Bit-vectors, typed #
A result's width is computed from its arguments' and indices: bvConcat is
Term (BitVec n) → Term (BitVec m) → Env (Term (BitVec (n + m))), matching BitVec.append.
Conversion to an integer, reading the bit-vector as unsigned.
Equations
Instances For
Rotation to the right by the given number of bits.
Equations
- Cvc.Typed.Term.bvRotateRight count bv = Cvc.Untyped.Term.bvRotateRight count bv
Instances For
Conversion of an integer to a bit-vector of the given size, modulo 2 ^ size.
Equations
- Cvc.Typed.Term.intToBv size arg = Cvc.Untyped.Term.intToBv size arg
Instances For
Extension with the given number of zeroes.
Equations
- Cvc.Typed.Term.bvZeroExtend extra bv = Cvc.Untyped.Term.bvZeroExtend extra bv
Instances For
Bits hi down to lo of bv, bit 0 being the least significant; needs lo ≤ hi < n.
Equations
- Cvc.Typed.Term.bvExtract hi lo bv = Cvc.Untyped.Term.bvExtract hi lo bv
Instances For
Rotation to the left by the given number of bits.
Equations
- Cvc.Typed.Term.bvRotateLeft count bv = Cvc.Untyped.Term.bvRotateLeft count bv
Instances For
Extension with the given number of copies of the sign bit.
Equations
- Cvc.Typed.Term.bvSignExtend extra bv = Cvc.Untyped.Term.bvSignExtend extra bv
Instances For
Conversion to an integer, reading the bit-vector as signed.
Equations
Instances For
A bit-vector literal of the given size, keeping the low size bits of value.
Equations
- Cvc.Typed.Term.mkBitVec size value = Cvc.Untyped.Term.mkBitVec size value
Instances For
A bit-vector literal of the given size, read in base, which must be 2, 10 or 16.
Equations
- Cvc.Typed.Term.mkBitVecOfString size repr base = Cvc.Untyped.Term.mkBitVecOfString size repr base
Instances For
The given number of copies of a bit-vector, concatenated.
Equations
- Cvc.Typed.Term.bvRepeat count bv = Cvc.Untyped.Term.bvRepeat count bv
Instances For
BitVec's operators with a result of sort BitVec.
- bvNot
[Ω]
{w : Nat}
(bv : Term (BitVec w))
: OnBitVec w
Bitwise negation.
- bvAnd
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise conjunction.
- bvOr
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise disjunction.
- bvXor
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise exclusive disjunction.
- bvNand
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise negated conjunction.
- bvNor
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise negated disjunction.
- bvXnor
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Bitwise negated exclusive disjunction.
- bvNeg
[Ω]
{w : Nat}
(bv : Term (BitVec w))
: OnBitVec w
Two's-complement negation.
- bvAdd
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Addition modulo
2 ^ n. - bvSub
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Subtraction modulo
2 ^ n. - bvMul
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Multiplication modulo
2 ^ n. - bvUdiv
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Unsigned division, truncating towards zero; all ones on a zero divisor.
- bvUrem
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Unsigned remainder; the dividend on a zero divisor.
- bvSdiv
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Signed division, truncating towards zero.
On a zero divisor:
-1for a non-negative dividend,1for a negative one. - bvSrem
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Signed remainder, sign following the dividend; the dividend on a zero divisor.
- bvSmod
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Signed remainder, sign following the divisor; the dividend on a zero divisor.
- bvShl
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Logical left shift of
lftbyrgtbits. - bvLshr
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Logical right shift of
lftbyrgtbits. - bvAshr
[Ω]
{w : Nat}
(lft rgt : Term (BitVec w))
: OnBitVec w
Arithmetic right shift of
lftbyrgtbits. - bvConcat
[Ω]
{w : Nat}
(n m : Nat)
{h0 : n + m = w}
(lft : Term (BitVec n))
(rgt : Term (BitVec m))
: OnBitVec w
Concatenation,
lftgiving the most significant bits. - bvComp
[Ω]
{w : Nat}
(n : Nat)
{h0 : 1 = w}
(lft rgt : Term (BitVec n))
: OnBitVec w
Bit-level comparison,
1when both arguments are equal and0otherwise. - bvRedand
[Ω]
{w : Nat}
(n : Nat)
{h0 : 1 = w}
(bv : Term (BitVec n))
: OnBitVec w
Conjunction of all the bits, as a one-bit bit-vector.
- bvRedor
[Ω]
{w : Nat}
(n : Nat)
{h0 : 1 = w}
(bv : Term (BitVec n))
: OnBitVec w
Disjunction of all the bits, as a one-bit bit-vector.
- bvIte
[Ω]
{w : Nat}
(cnd : Term (BitVec 1))
(thn els : Term (BitVec w))
: OnBitVec w
Bit-vector conditional, selecting on a one-bit condition.
- bvUltbv
[Ω]
{w : Nat}
(n : Nat)
{h0 : 1 = w}
(lft rgt : Term (BitVec n))
: OnBitVec w
Unsigned less-than, as a one-bit bit-vector.
- bvSltbv
[Ω]
{w : Nat}
(n : Nat)
{h0 : 1 = w}
(lft rgt : Term (BitVec n))
: OnBitVec w
Signed less-than, as a one-bit bit-vector.
- bvExtract
[Ω]
{w : Nat}
(hi lo n : Nat)
{h0 : hi - lo + 1 = w}
(bv : Term (BitVec n))
: OnBitVec w
Bits
hidown toloofbv, bit 0 being the least significant; needslo ≤ hi < n. - bvRepeat
[Ω]
{w : Nat}
(count n : Nat)
{h0 : n * count = w}
(bv : Term (BitVec n))
: OnBitVec w
The given number of copies of a bit-vector, concatenated.
- bvZeroExtend
[Ω]
{w : Nat}
(extra n : Nat)
{h0 : n + extra = w}
(bv : Term (BitVec n))
: OnBitVec w
Extension with the given number of zeroes.
- bvSignExtend
[Ω]
{w : Nat}
(extra n : Nat)
{h0 : n + extra = w}
(bv : Term (BitVec n))
: OnBitVec w
Extension with the given number of copies of the sign bit.
- bvRotateLeft
[Ω]
{w : Nat}
(count : Nat)
(bv : Term (BitVec w))
: OnBitVec w
Rotation to the left by the given number of bits.
- bvRotateRight
[Ω]
{w : Nat}
(count : Nat)
(bv : Term (BitVec w))
: OnBitVec w
Rotation to the right by the given number of bits.
- intToBv
[Ω]
{w : Nat}
(size : Nat)
{h0 : size = w}
(arg : Term Int)
: OnBitVec w
Conversion of an integer to a bit-vector of the given size, modulo
2 ^ size.
Instances For
BitVec's operators, taken apart one level, indexed by the sort each produces.
- bitVec
[Ω]
(w : Nat)
: OnBitVec w → View.BitVec (Typ.bitVec w)
An operator with a result of sort
BitVec. - bool
[Ω]
: OnBool → View.BitVec Typ.bool
An operator with a result of sort
Bool. - int
[Ω]
: OnInt → View.BitVec Typ.int
An operator with a result of sort
Int.
Instances For
Takes a term apart one level, at its sort, if BitVec owns its operator and the term's sort fits it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
BitVec's operators with a result of sort Bool.
- bvUlt
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Unsigned less-than.
- bvUle
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Unsigned less-than-or-equal-to.
- bvUgt
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Unsigned greater-than.
- bvUge
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Unsigned greater-than-or-equal-to.
- bvSlt
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Signed less-than.
- bvSle
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Signed less-than-or-equal-to.
- bvSgt
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Signed greater-than.
- bvSge
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Signed greater-than-or-equal-to.
- bvNego
[Ω]
(n : Nat)
(bv : Term (BitVec n))
: OnBool
Whether two's-complement negation overflows.
- bvUaddo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether unsigned addition overflows.
- bvSaddo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether signed addition overflows.
- bvUsubo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether unsigned subtraction overflows.
- bvSsubo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether signed subtraction overflows.
- bvUmulo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether unsigned multiplication overflows.
- bvSmulo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether signed multiplication overflows.
- bvSdivo
[Ω]
(n : Nat)
(lft rgt : Term (BitVec n))
: OnBool
Whether signed division overflows.
Instances For
Values #
Determine if this term is a bit-vector value.
Equations
- term.isBitVecValue = Cvc.Untyped.Term.isBitVecValue term
Instances For
The bit-vector a constant term denotes, failing unless it has the expected size.
Equations
- term.getBitVecValue = Cvc.Untyped.Term.getBitVecValue term
Instances For
Equations
- One or more equations did not get rendered due to their size.