A BitVector consists of a sequence of symbolic bits and can be used for symbolic machine-word arithmetic. Bits are stored in most-significant-bit first order.

Empty bitvector

Number of bits in a bit vector

Project the individual bits of a BitVector. x at 0 is the most significant bit. It is an error to request an out-of-bounds bit.

Select bits from a bitvector, starting from the least significant bit. x ! 0 is the least significant bit. It is an error to request an out-of-bounds bit.

Append two bitvectors, with the most significant bitvector given first.

Concatenate a list of bitvectors, with the most significant bitvector at the head of the list.

Project out the n most significant bits from a bitvector.

Drop the n most significant bits from a bitvector.

Extract n bits starting at index i. The vector must contain at least i+n elements

Extract n bits starting at index i, counting from the end of the vector instead of the beginning. The vector must contain at least i+n elements.

Combine two bitvectors with a bitwise function

Combine two bitvectors with a bitwise monadic combiner action.

Retrieve the most significant bit of a bitvector.

Retrieve the least significant bit of a bitvector.

Test syntactic equalify of two bitvectors using the === operation

Display a bitvector as a string of bits with most significant bits first. Concrete literals are displayed as '0' or '1', whereas symbolic literals are displayed as x.

Generate a bitvector of length n, using monadic function f to generate the bit literals. The indexes to f are given in MSB-first order, i.e., f 0 is the most significant bit.

Generate a bitvector of length n, using function f to specify the bit literals. The indexes to f are given in MSB-first order, i.e., f 0 is the most significant bit.

Generate a bitvector of length n, using monadic function f to generate the bit literals. The indexes to f are given in LSB-first order, i.e., f 0 is the least significant bit.

Generate a bitvector of length n, using function f to specify the bit literals. The indexes to f are given in LSB-first order, i.e., f 0 is the least significant bit.

Generate a bit vector of length n where every bit value is literal l.

Generate a bit vector of length n where every bit value is generated in turn by m.

Generate a bitvector from an integer value, using 2's complement representation.

Convert a list to a bitvector, assuming big-endian bit order.

muxInteger mergeFn maxValue lv valueFn returns a circuit whose result is valueFn v when lv has value v.

Generate a one-element bitvector containing the given literal

Build a short-cut AND circuit. If the left argument evaluates to the constant false, the right argument will not be evaluated.

Build a short-cut OR circuit. If the left argument evaluates to the constant true, the right argument will not be evaluated.

Construct a lazy xor. If both arguments are constants, the output will also be a constant.

Construct a lazy equality test. If both arguments are constants, the output will also be a constant.

Lazy negation of a circuit.

If-then-else combinator for bitvectors.

If-then-else combinator for bitvector computations with optimistic shortcutting. If the test bit is concrete, we can avoid generating either the if or the else circuit.

Interpret a bitvector as an unsigned integer. Return Nothing if the bitvector is not concrete.

Interpret a bitvector as a signed integer. Return Nothing if the bitvector is not concrete.

Convert a bitvector to a list, most significant bit first.

Compute the 2's complement negation of a bitvector

Add two bitvectors with the same size. Discard carry bit.

Add two bitvectors with the same size with carry.

Subtract one bitvector from another with the same size. Discard carry bit.

Subtract one bitvector from another with the same size with carry.

Add a constant value to a bitvector

Add a constant value to a bitvector

Multiply two bitvectors with the same size, with result of the same size as the arguments. Overflow is silently discarded.

Unsigned multiply two bitvectors with size m and size n, resulting in a vector of size m+n.

Signed multiply two bitvectors with size m and size n, resulting in a vector of size m+n.

Compute the signed quotient of two signed bitvectors with the same size.

Compute the signed division remainder of two signed bitvectors with the same size.

Compute the unsigned quotient of two unsigned bitvectors with the same size.

Compute the unsigned division remainder of two unsigned bitvectors with the same size.

Shift left. The least significant bit becomes 0.

Signed right shift. The most significant bit is copied.

Unsigned right shift. The most significant bit becomes 0.

Rotate left.

Rotate right.

Test equality of two bitvectors with the same size.

Test if a bitvector is equal to zero

Test if a bitvector is distinct from zero

Signed less-than-or-equal on bitvector with the same size.

Signed less-than on bitvector with the same size.

Unsigned less-than-or-equal on bitvector with the same size.

Unsigned less-than on bitvector with the same size.

Return absolute value of signed bitvector.

sext v n sign extends v to be a vector with length n. This function requires that n >= length v and length v > 0.

zext g v n zero extends v to be a vector with length n. This function requires that n >= length v.

Truncate the given bit vector to the specified length

Truncate or zero-extend a bitvector to have the specified number of bits

Truncate or sign-extend a bitvector to have the specified number of bits

Priority encoder. Given a bitvector, calculate the bit position of the most-significant 1 bit, with position 0 corresponding to the least-significant-bit. Return the "valid" bit, which is set iff at least one bit in the input is set; and the calcuated bit position. If no bits are set in the input (i.e. if the valid bit is false), the calculated bit position is zero. The indicated bitwidth must be large enough to hold the answer; in particular, we must have (length bv <= 2^w).

Compute the rounded-down base2 logarithm of the input bitvector. For x > 0, this uniquely satisfies 2^(logBase2_down(x)) <= x < 2^(logBase2_down(x)+1). For x = 0, we set logBase2(x) = -1. The output bitvector has the same width as the input bitvector.

Compute the rounded-up base2 logarithm of the input bitvector. For x > 1, this uniquely satisfies 2^(logBase2_up(x) - 1) < x <= 2^(logBase2_up(x)). For x = 1, logBase2_up 1 = 0. For x = 0, we get logBase2_up 0 = bitvector length; this just happens to work out from the defining fomula `logBase2_up x = logBase2_down (x-1) + 1` when interpreted in 2's complement. The output bitvector has the same width as the input bitvector.

Count the number of leading zeros in the input vector; that is, the number of more-significant digits set to 0 above the most significant digit that is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as leading zeros). The output bitvector has the same width as the input bitvector.

Count the number of trailing zeros in the input vector; that is, the number of less-significant digits set to 0 below the least significant digit which is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as trailing zeros). The output bitvector has the same width as the input bitvector.

Polynomial multiplication. Note that the algorithm works the same no matter which endianness convention is used. Result length is max 0 (m+n-1), where m and n are the lengths of the inputs.

Polynomial division. Return value has length equal to the first argument.

Polynomial mod with symbolic modulus. Return value has length one less than the length of the modulus. This implementation is optimized for the (common) case where the modulus is concrete.