Documentation

Bitvector equality.

Unsigned less-than-or-equal.

Unsigned less-than.

Signed less-than-or-equal.

Signed less-than.

Two's complement bitvector negation.

Two's complement bitvector addition.

Two's complement bitvector subtraction.

Two's complement bitvector multiplication.

Unsigned bitvector division.

Unsigned bitvector remainder.

Signed bitvector division.

Signed bitvector remainder.

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 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.

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

Bitwise logical left shift. Shifts the bits in the first bit-vector by the unsigned, arithmetic value in the second bit-vector filling in with false bits.

Arithmetic logical right shift. Shifts the bits in the first bit-vector by the unsigned, arithmetic value in the second bit-vector filling in with bits matching the first bit (which is treated as a sign bit).

Bitwise logical right shift. Shifts the bits in the first bit-vector by the unsigned, arithmetic value in the second bit-vector filling in with false bits.

Bitwise right rotation. Rotates the bits in the first bit-vector by the unsigned, arithmetic value in the second bit-vector.

Bitwise left rotation. Rotates the bits in the first bit-vector by the unsigned, arithmetic value in the second bit-vector.

Constant integer literals.