range package:what4

range w l u returns domain containing all bitvectors formed from the w low order bits of some i in [l,u]. Note that per testBit, the least significant bit has index 0.

range w l u returns domain containing all bitvectors formed from the w low order bits of some i in [l,u]. Note that per testBit, the least significant bit has index 0.

Construct a domain from bitwise lower and upper bounds

Return maybe Boolean if range is equal, is not equal, or indeterminant.

Return upper bound of range.

Return lower bound of range.

Multiply a range by a scalar value

Option style for integer-valued options with upper and lower bounds

Option style for real-valued options with upper and lower bounds

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.

unsignedRanges v returns a set of predicates and ranges where we know that for each entry (p,l,h) and each value i : l <= i & i <= h: p iff. v <= i

The number is between the given lower and upper bounds.

This exception is thrown if the user requests to make a bounded variable, but gives incoherent or out-of-range bounds.

The number is less than or equal to the given upper bound.

The number is greater than or equal to the given lower bound.

Indicates that range denotes a single value

The number is unconstrained.

Describes a range of values in a totally ordered set.

Check whether the lhs array and rhs array are equal at a range of indices. arrayRangeEq sym lhs_arr lhs_idx rhs_arr rhs_idx len checks whether the elements of lhs_arr at indices [lhs_idx .. (lhs_idx + len - 1)] and the elements of rhs_arr at indices [rhs_idx .. (rhs_idx + len - 1)] are equal. The result is undefined if either lhs_idx + len or rhs_idx + len wraps around.

This function is used for selecting a value from among potential values in a range. muxRange p ite f l h returns an expression denoting the value obtained from the value f i where i is the smallest value in the range [l..h] such that p i is true. If p i is true for no such value, then this returns the value f h.