A unary bitvector encoding where the map contains predicates such as u^.unaryBVMap^.at i holds iff the value represented by u is less than or equal to i.

The map stored in the representation should always have a single element, and the largest integer stored in the map should be associated with a predicate representing "true". This means that if the map contains only a single binding, then it represents a constant.

Returns the number of distinct values that this could be.

Create a unary bitvector term from a constant.

Create a unary bitvector term from a constant.

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

Evaluate a unary bitvector as an integer given an evaluation function.

Evaluate a unary bitvector given an evaluation function.

This function is used to convert a unary bitvector into some other representation such as a binary bitvector or vector of bits.

It is polymorphic over the result type r, and requires functions for manipulating values of type r to construct it.

This function instantiates the predicates in a unary predicate with new predicates.

The mapping f should be monotonic, that is for all predicates p and 'q, such that 'p |- q', f should satisfy the constraint that 'f p |- f q'.

Return potential values for abstract domain.

Add two bitvectors.

The number of integers in the result will be at most the product of the sizes of the individual bitvectors.

Negate a bitvector. The size of the result will be equal to the size of the input.

mux sym c x y returns value equal to if c then x else y. The number of entries in the return value is at most size x + size y.

Return predicate that holds if bitvectors are equal.

Return predicate that holds if first value is less than other.

Return predicate that holds if first value is less than other.

Perform a unsigned extension

Perform a signed extension

Perform a struncation.