A What4 symbolic bitvector where the size does not appear in the type

Return the signed value if this is a constant bitvector

Return the unsigned value if this is a constant bitvector

Convert an integer to an unsigned bitvector. The input value is reduced modulo 2^w.

Interpret the bit-vector as an unsigned integer

Interpret the bit-vector as a signed integer

Get the width of a bitvector

Create a bitvector with the given width and value

Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in little-endian ordering, meaning the least-significant bit is bit 0

Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0

Select a subsequence from a bitvector, with bits numbered in Big Endian order (most significant bit is 0). This fails if idx + n is >= w

Select a subsequence from a bitvector, with bits numbered in Little Endian order (least significant bit is 0). This fails if idx + n is >= w

Concatenate two bitvectors.

If-then-else applied to bitvectors.

convert a vector of booleans to a bitvector. The input are used in Big Endian order (most significant bit first)

convert a vector of booleans to a bitvector. The inputs are used in Little Endian order (least significant bit first)

Explode a bitvector into a vector of booleans in Big Endian order (most significant bit first)

Explode a bitvector into a vector of booleans in Little Endian order (least significant bit first)

Bitwise complement

Bitwise logical and.

Bitwise logical or.

Bitwise logical exclusive or.

2's complement negation.

Add two bitvectors.

Subtract one bitvector from another.

Multiply one bitvector by another.

Unsigned bitvector division.

The result is undefined when y is zero, but is otherwise equal to floor( x / y ).

Unsigned bitvector remainder.

The result is undefined when y is zero, but is otherwise equal to x - (bvUdiv x y) * y.

Signed bitvector division. The result is truncated to zero.

The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs.

NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.

Signed bitvector remainder.

The result of bvSrem x y is undefined when y is zero, but is otherwise equal to x - (bvSdiv x y) * y.

Return true if bitvectors are equal.

Signed less-than-or-equal.

Signed less-than.

Unsigned less-than-or-equal.

Unsigned less-than.

Signed greater-than-or-equal.

Signed greater-than.

Unsigned greater-than-or-equal.

Unsigned greater-than.

Zero-extend a value, adding the specified number of bits.

Sign-extend a value, adding the specified number of bits.