Generated bit-vector constructors, sort-erased #

bvNot [Ω] (bv : Term) : View.BitVec
Bitwise negation.
bvAnd [Ω] (lft rgt : Term) : View.BitVec
Bitwise conjunction.
bvOr [Ω] (lft rgt : Term) : View.BitVec
Bitwise disjunction.
bvXor [Ω] (lft rgt : Term) : View.BitVec
Bitwise exclusive disjunction.
bvNand [Ω] (lft rgt : Term) : View.BitVec
Bitwise negated conjunction.
bvNor [Ω] (lft rgt : Term) : View.BitVec
Bitwise negated disjunction.
bvXnor [Ω] (lft rgt : Term) : View.BitVec
Bitwise negated exclusive disjunction.
bvNeg [Ω] (bv : Term) : View.BitVec
Two's-complement negation.
bvAdd [Ω] (lft rgt : Term) : View.BitVec
Addition modulo 2 ^ n.
bvSub [Ω] (lft rgt : Term) : View.BitVec
Subtraction modulo 2 ^ n.
bvMul [Ω] (lft rgt : Term) : View.BitVec
Multiplication modulo 2 ^ n.
bvUdiv [Ω] (lft rgt : Term) : View.BitVec
Unsigned division, truncating towards zero; all ones on a zero divisor.
bvUrem [Ω] (lft rgt : Term) : View.BitVec
Unsigned remainder; the dividend on a zero divisor.
bvSdiv [Ω] (lft rgt : Term) : View.BitVec
Signed division, truncating towards zero.
On a zero divisor: -1 for a non-negative dividend, 1 for a negative one.
bvSrem [Ω] (lft rgt : Term) : View.BitVec
Signed remainder, sign following the dividend; the dividend on a zero divisor.
bvSmod [Ω] (lft rgt : Term) : View.BitVec
Signed remainder, sign following the divisor; the dividend on a zero divisor.
bvShl [Ω] (lft rgt : Term) : View.BitVec
Logical left shift of lft by rgt bits.
bvLshr [Ω] (lft rgt : Term) : View.BitVec
Logical right shift of lft by rgt bits.
bvAshr [Ω] (lft rgt : Term) : View.BitVec
Arithmetic right shift of lft by rgt bits.
bvUlt [Ω] (lft rgt : Term) : View.BitVec
Unsigned less-than.
bvUle [Ω] (lft rgt : Term) : View.BitVec
Unsigned less-than-or-equal-to.
bvUgt [Ω] (lft rgt : Term) : View.BitVec
Unsigned greater-than.
bvUge [Ω] (lft rgt : Term) : View.BitVec
Unsigned greater-than-or-equal-to.
bvSlt [Ω] (lft rgt : Term) : View.BitVec
Signed less-than.
bvSle [Ω] (lft rgt : Term) : View.BitVec
Signed less-than-or-equal-to.
bvSgt [Ω] (lft rgt : Term) : View.BitVec
Signed greater-than.
bvSge [Ω] (lft rgt : Term) : View.BitVec
Signed greater-than-or-equal-to.
bvConcat [Ω] (lft rgt : Term) : View.BitVec
Concatenation, lft giving the most significant bits.
bvComp [Ω] (lft rgt : Term) : View.BitVec
Bit-level comparison, 1 when both arguments are equal and 0 otherwise.
bvRedand [Ω] (bv : Term) : View.BitVec
Conjunction of all the bits, as a one-bit bit-vector.
bvRedor [Ω] (bv : Term) : View.BitVec
Disjunction of all the bits, as a one-bit bit-vector.
bvIte [Ω] (cnd thn els : Term) : View.BitVec
Bit-vector conditional, selecting on a one-bit condition.
bvUbvToInt [Ω] (bv : Term) : View.BitVec
Conversion to an integer, reading the bit-vector as unsigned.
bvSbvToInt [Ω] (bv : Term) : View.BitVec
Conversion to an integer, reading the bit-vector as signed.
bvNego [Ω] (bv : Term) : View.BitVec
Whether two's-complement negation overflows.
bvUaddo [Ω] (lft rgt : Term) : View.BitVec
Whether unsigned addition overflows.
bvSaddo [Ω] (lft rgt : Term) : View.BitVec
Whether signed addition overflows.
bvUsubo [Ω] (lft rgt : Term) : View.BitVec
Whether unsigned subtraction overflows.
bvSsubo [Ω] (lft rgt : Term) : View.BitVec
Whether signed subtraction overflows.
bvUmulo [Ω] (lft rgt : Term) : View.BitVec
Whether unsigned multiplication overflows.
bvSmulo [Ω] (lft rgt : Term) : View.BitVec
Whether signed multiplication overflows.
bvSdivo [Ω] (lft rgt : Term) : View.BitVec
Whether signed division overflows.
bvUltbv [Ω] (lft rgt : Term) : View.BitVec
Unsigned less-than, as a one-bit bit-vector.
bvSltbv [Ω] (lft rgt : Term) : View.BitVec
Signed less-than, as a one-bit bit-vector.
bvExtract [Ω] (hi lo : Nat) (bv : Term) : View.BitVec
Bits hi down to lo of bv, bit 0 being the least significant; needs lo ≤ hi < n.
bvRepeat [Ω] (count : Nat) (bv : Term) : View.BitVec
The given number of copies of a bit-vector, concatenated.
bvZeroExtend [Ω] (extra : Nat) (bv : Term) : View.BitVec
Extension with the given number of zeroes.
bvSignExtend [Ω] (extra : Nat) (bv : Term) : View.BitVec
Extension with the given number of copies of the sign bit.
bvRotateLeft [Ω] (count : Nat) (bv : Term) : View.BitVec
Rotation to the left by the given number of bits.
bvRotateRight [Ω] (count : Nat) (bv : Term) : View.BitVec
Rotation to the right by the given number of bits.
intToBv [Ω] (size : Nat) (arg : Term) : View.BitVec
Conversion of an integer to a bit-vector of the given size, modulo 2 ^ size.