Bit-Vectors

Basic Bit-Vector Term Builders

cvc5.pythonic.BitVec(name, bv, ctx=None)

Return a bit-vector constant named name. bv may be the number of bits of a bit-vector sort. If ctx=None, then the global context is used.

>>> x  = BitVec('x', 16)
>>> is_bv(x)
True
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> word = BitVecSort(16)
>>> x2 = BitVec('x', word)
>>> eq(x, x2)
True

cvc5.pythonic.BitVecVal(val, bv, ctx=None)

Return a bit-vector value with the given number of bits. If ctx=None, then the global context is used. The second argument can be a number of bits (integer) or a bit-vector sort.

>>> v = BitVecVal(10, 32)
>>> v
10
>>> print("0x%.8x" % v.as_long())
0x0000000a
>>> s = BitVecSort(3)
>>> u = BitVecVal(10, s)
>>> u
2

cvc5.pythonic.BitVecSort(sz, ctx=None)

Return an SMT bit-vector sort of the given size. If ctx=None, then the global context is used.

>>> Byte = BitVecSort(8)
>>> Word = BitVecSort(16)
>>> Byte
BitVec(8)
>>> x = Const('x', Byte)
>>> eq(x, BitVec('x', 8))
True

cvc5.pythonic.BitVecs(names, bv, ctx=None)

Return a tuple of bit-vector constants of size bv.

>>> x, y, z = BitVecs('x y z', 16)
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> Sum(x, y, z)
x + y + z
>>> Product(x, y, z)
x*y*z

Bit-Vector Overloads

See the following operator overloads for building bit-vector terms. Each kind of term can also be built with a builder function below.

• arithmetic

  addition (+)

  cvc5.pythonic.BitVecRef.__add__()

  subtraction (-)

  cvc5.pythonic.BitVecRef.__sub__()

  multiplication (*)

  cvc5.pythonic.BitVecRef.__mul__()

  division (/)

  cvc5.pythonic.BitVecRef.__div__()

• bit-wise

  or (|)

  cvc5.pythonic.BitVecRef.__or__()

  and (&)

  cvc5.pythonic.BitVecRef.__and__()

  xor (^)

  cvc5.pythonic.BitVecRef.__xor__()

  bit complement (~)

  cvc5.pythonic.BitVecRef.__invert__()

  negation (-)

  cvc5.pythonic.BitVecRef.__neg__()

  left shift (<<)

  cvc5.pythonic.BitVecRef.__lshift__()

  right shift (>>)

  cvc5.pythonic.BitVecRef.__rshift__()

• comparisons

  signed greater than (>)

  cvc5.pythonic.BitVecRef.__gt__()

  signed less than (<)

  cvc5.pythonic.BitVecRef.__lt__()

  signed greater than or equal to (>=)

  cvc5.pythonic.BitVecRef.__ge__()

  signed less than or equal to (<=)

  cvc5.pythonic.BitVecRef.__le__()

  equal (==)

  cvc5.pythonic.ExprRef.__eq__()

  not equal (!=)

  cvc5.pythonic.ExprRef.__ne__()

Bit-Vector Term Builders

cvc5.pythonic.BV2Int(a, is_signed=False)

Return the SMT expression BV2Int(a).

>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=False)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=True)
x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
>>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2]

cvc5.pythonic.Int2BV(a, num_bits)

Return the SMT expression Int2BV(a, num_bits). It is a bit-vector of width num_bits and represents the modulo of a by 2^num_bits

>>> x = Int('x')
>>> bv_x = Int2BV(x, 2)
>>> bv_x_plus_4 = Int2BV(x + 4, 2)
>>> solve([bv_x != bv_x_plus_4])
no solution

cvc5.pythonic.Concat(*args)

Create an SMT bit-vector, string, sequence or regular expression concatenation expression.

>>> v = BitVecVal(1, 4)
>>> Concat(v, v+1, v)
Concat(1, 1 + 1, 1)
>>> evaluate(Concat(v, v+1, v))
289
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121

cvc5.pythonic.Extract(high, low, a)

Create an SMT bit-vector extraction expression, or create a string extraction expression.

>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)

cvc5.pythonic.ULE(a, b)

Create the SMT expression (unsigned) other <= self.

Use the operator <= for signed less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

cvc5.pythonic.ULT(a, b)

Create the SMT expression (unsigned) other < self.

Use the operator < for signed less than.

>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

cvc5.pythonic.UGE(a, b)

Create the SMT expression (unsigned) other >= self.

Use the operator >= for signed greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

cvc5.pythonic.UGT(a, b)

Create the SMT expression (unsigned) other > self.

Use the operator > for signed greater than.

>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

cvc5.pythonic.SLE(a, b)

Create the SMT expression (signed) other <= self.

See also the __le__ overload (<= operator) for BitVecRef

>>> x, y = BitVecs('x y', 32)
>>> SLE(x, y).sexpr()
'(bvsle x y)'

cvc5.pythonic.SLT(a, b)

Create the SMT expression (signed) other < self.

See also the __lt__ overload (< operator) for BitVecRef

>>> x, y = BitVecs('x y', 32)
>>> SLT(x, y).sexpr()
'(bvslt x y)'

cvc5.pythonic.SGE(a, b)

Create the SMT expression (signed) other >= self.

See also the __ge__ overload (>= operator) for BitVecRef

>>> x, y = BitVecs('x y', 32)
>>> SGE(x, y).sexpr()
'(bvsge x y)'

cvc5.pythonic.SGT(a, b)

Create the SMT expression (signed) other > self.

See also the __gt__ overload (> operator) for BitVecRef

>>> x, y = BitVecs('x y', 32)
>>> SGT(x, y).sexpr()
'(bvsgt x y)'

cvc5.pythonic.UDiv(a, b)

Create the SMT expression (unsigned) division self / other.

Use the operator / for signed division.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> UDiv(x, y)
UDiv(x, y)
>>> UDiv(x, y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'

cvc5.pythonic.URem(a, b)

Create the SMT expression (unsigned) remainder self % other.

Use the operator % for signed modulus, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'

cvc5.pythonic.SDiv(a, b)

Create an SMT signed division expression.

See also the __div__ overload (/ operator) for BitVecRef.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SDiv(x, y)
x/y

cvc5.pythonic.SMod(a, b)

Create an SMT expression for the signed modulus self % other.

See also the __mod__ overload (% operator) for BitVecRef.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SMod(x, y)
x%y

cvc5.pythonic.SRem(a, b)

Create the SMT expression signed remainder.

Use the operator % for signed modulus, and URem() for unsigned remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

cvc5.pythonic.LShR(a, b)

Create the SMT expression logical right shift.

Use the operator >> for the arithmetical right shift.

>>> x, y = BitVecs('x y', 32)
>>> LShR(x, y)
LShR(x, y)
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
2
>>> simplify(BitVecVal(2, 3) >> 1)
1
>>> simplify(LShR(BitVecVal(2, 3), 1))
1

cvc5.pythonic.RotateLeft(a, b)

Return an expression representing a rotated to the left b times.

>>> a, b = BitVecs('a b', 16)
>>> RotateLeft(a, 10)
RotateLeft(a, 10)
>>> simplify(RotateLeft(a, 0))
a
>>> simplify(RotateLeft(a, 16))
a

cvc5.pythonic.RotateRight(a, b)

Return an expression representing a rotated to the right b times.

>>> a, b = BitVecs('a b', 16)
>>> RotateRight(a, 10)
RotateRight(a, 10)
>>> simplify(RotateRight(a, 0))
a
>>> simplify(RotateRight(a, 16))
a

cvc5.pythonic.SignExt(n, a)

Return a bit-vector expression with n extra sign-bits.

>>> x = BitVec('x', 16)
>>> n = SignExt(8, x)
>>> n.size()
24
>>> n
SignExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(SignExt(6, v0))
>>> v
254
>>> v.size()
8
>>> print("%.x" % v.as_long())
fe

cvc5.pythonic.ZeroExt(n, a)

Return a bit-vector expression with n extra zero-bits.

>>> x = BitVec('x', 16)
>>> n = ZeroExt(8, x)
>>> n.size()
24
>>> n
ZeroExt(8, x)
>>> n.sort()
BitVec(24)
>>> v0 = BitVecVal(2, 2)
>>> v0
2
>>> v0.size()
2
>>> v  = simplify(ZeroExt(6, v0))
>>> v
2
>>> v.size()
8

cvc5.pythonic.RepeatBitVec(n, a)

Return an expression representing n copies of a.

>>> x = BitVec('x', 8)
>>> n = RepeatBitVec(4, x)
>>> n
RepeatBitVec(4, x)
>>> n.size()
32
>>> v0 = BitVecVal(10, 4)
>>> print("%.x" % v0.as_long())
a
>>> v = simplify(RepeatBitVec(4, v0))
>>> v.size()
16
>>> print("%.x" % v.as_long())
aaaa

cvc5.pythonic.BVRedAnd(a)

Return the reduction-and expression of a.

>>> x = BitVec('x', 4)
>>> solve([BVRedAnd(x), BVRedOr(~x)])
no solution

cvc5.pythonic.BVRedOr(a)

Return the reduction-or expression of a.

>>> x = BitVec('x', 4)
>>> solve([BVRedAnd(x), BVRedOr(~x)])
no solution

cvc5.pythonic.BVAdd(*args)

Create a sum of bit-vectors.

See also the __add__ overload (+ operator) for BitVecRef.

>>> x, y, z = BitVecs('x y z', 32)
>>> BVAdd(x, y, z)
x + y + z

cvc5.pythonic.BVMult(*args)

Create a product of bit-vectors.

See also the __mul__ overload (* operator) for BitVecRef.

>>> x, y, z = BitVecs('x y z', 32)
>>> BVMult(x, y, z)
x*y*z

cvc5.pythonic.BVSub(a, b)

Create a difference of bit-vectors.

See also the __sub__ overload (- operator) for BitVecRef.

>>> x, y = BitVecs('x y', 32)
>>> BVSub(x, y)
x - y

cvc5.pythonic.BVOr(*args)

Create a bit-wise disjunction of bit-vectors.

See also the __or__ overload (| operator) for BitVecRef.

>>> x, y, z = BitVecs('x y z', 32)
>>> BVOr(x, y, z)
x | y | z

cvc5.pythonic.BVAnd(*args)

Create a bit-wise conjunction of bit-vectors.

See also the __and__ overload (& operator) for BitVecRef.

>>> x, y, z = BitVecs('x y z', 32)
>>> BVAnd(x, y, z)
x & y & z

cvc5.pythonic.BVXor(*args)

Create a bit-wise exclusive disjunction of bit-vectors.

See also the __xor__ overload (^ operator) for BitVecRef.

>>> x, y, z = BitVecs('x y z', 32)
>>> BVXor(x, y, z)
x ^ y ^ z

cvc5.pythonic.BVNeg(a)

Create a negation (two’s complement) of a bit-vector

See also the __neg__ overload (unary - operator) for BitVecRef.

>>> x = BitVec('x', 32)
>>> BVNeg(x)
-x

cvc5.pythonic.BVNot(a)

Create a bitwise not of a bit-vector

See also the __invert__ overload (unary ~ operator) for BitVecRef.

>>> x = BitVec('x', 32)
>>> BVNot(x)
~x

Testers

cvc5.pythonic.is_bv_sort(s)

Return True if s is an SMT bit-vector sort.

>>> is_bv_sort(BitVecSort(32))
True
>>> is_bv_sort(IntSort())
False

cvc5.pythonic.is_bv(a)

Return True if a is an SMT bit-vector expression.

>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False

cvc5.pythonic.is_bv_value(a)

Return True if a is an SMT bit-vector numeral value.

>>> b = BitVec('b', 32)
>>> is_bv_value(b)
False
>>> b = BitVecVal(10, 32)
>>> b
10
>>> is_bv_value(b)
True

Classes (with overloads)

class cvc5.pythonic.BitVecSortRef(ast, ctx=None)

Bit-vector sort.

cast(val)

Try to cast val as a Bit-Vector.

>>> b = BitVecSort(32)
>>> b.cast(10)
10
>>> b.cast(10).sexpr()
'#b00000000000000000000000000001010'

size()

Return the size (number of bits) of the bit-vector sort self.

>>> b = BitVecSort(32)
>>> b.size()
32

subsort(other)

Return True if self is a subsort of other.

>>> IntSort().subsort(RealSort())
True
>>> BoolSort().subsort(RealSort())
True
>>> SetSort(BitVecSort(2)).subsort(SetSort(IntSort()))
False

class cvc5.pythonic.BitVecRef(ast, ctx=None, reverse_children=False)

Bit-vector expressions.

__add__(other)

Create the SMT expression self + other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x + y
x + y
>>> (x + y).sort()
BitVec(32)

__and__(other)

Create the SMT expression bitwise-and self & other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x & y
x & y
>>> (x & y).sort()
BitVec(32)

__div__(other)

Create the SMT expression (signed) division self / other.

Use the function UDiv() for unsigned division.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x / y
x/y
>>> (x / y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'

__ge__(other)

Create the SMT expression (signed) other >= self.

Use the function UGE() for unsigned greater than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> x >= y
x >= y
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'

__gt__(other)

Create the SMT expression (signed) other > self.

Use the function UGT() for unsigned greater than.

>>> x, y = BitVecs('x y', 32)
>>> x > y
x > y
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'

__invert__()

Create the SMT expression bitwise-not ~self.

>>> x = BitVec('x', 32)
>>> ~x
~x
>>> solve([~(~x) != x])
no solution

__le__(other)

Create the SMT expression (signed) other <= self.

Use the function ULE() for unsigned less than or equal to.

>>> x, y = BitVecs('x y', 32)
>>> x <= y
x <= y
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'

__lshift__(other)

Create the SMT expression left shift self << other

>>> x, y = BitVecs('x y', 32)
>>> x << y
x << y
>>> (x << y).sexpr()
'(bvshl x y)'
>>> evaluate(BitVecVal(2, 3) << 1)
4

__lt__(other)

Create the SMT expression (signed) other < self.

Use the function ULT() for unsigned less than.

>>> x, y = BitVecs('x y', 32)
>>> x < y
x < y
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'

__mod__(other)

Create the SMT expression (signed) mod self % other.

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x % y
x%y
>>> (x % y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'

__mul__(other)

Create the SMT expression self * other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x * y
x*y
>>> (x * y).sort()
BitVec(32)

__neg__()

Return an expression representing -self.

>>> x = BitVec('x', 32)
>>> -x
-x
>>> solve([-(-x) != x])
no solution

__or__(other)

Create the SMT expression bitwise-or self | other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x | y
x | y
>>> (x | y).sort()
BitVec(32)

__pos__()

Return self.

>>> x = BitVec('x', 32)
>>> +x
x

__radd__(other)

Create the SMT expression other + self.

>>> x = BitVec('x', 32)
>>> 10 + x
10 + x

__rand__(other)

Create the SMT expression bitwise-or other & self.

>>> x = BitVec('x', 32)
>>> 10 & x
10 & x

__rdiv__(other)

Create the SMT expression (signed) division other / self.

Use the function UDiv() for unsigned division.

>>> x = BitVec('x', 32)
>>> 10 / x
10/x
>>> (10 / x).sexpr()
'(bvsdiv #b00000000000000000000000000001010 x)'
>>> UDiv(10, x).sexpr()
'(bvudiv #b00000000000000000000000000001010 x)'

__rlshift__(other)

Create the SMT expression left shift other << self.

Use the function LShR() for the right logical shift

>>> x = BitVec('x', 32)
>>> 10 << x
10 << x
>>> (10 << x).sexpr()
'(bvshl #b00000000000000000000000000001010 x)'

__rmod__(other)

Create the SMT expression (signed) mod other % self.

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

>>> x = BitVec('x', 32)
>>> 10 % x
10%x
>>> (10 % x).sexpr()
'(bvsmod #b00000000000000000000000000001010 x)'
>>> URem(10, x).sexpr()
'(bvurem #b00000000000000000000000000001010 x)'
>>> SRem(10, x).sexpr()
'(bvsrem #b00000000000000000000000000001010 x)'

__rmul__(other)

Create the SMT expression other * self.

>>> x = BitVec('x', 32)
>>> 10 * x
10*x

__ror__(other)

Create the SMT expression bitwise-or other | self.

>>> x = BitVec('x', 32)
>>> 10 | x
10 | x

__rrshift__(other)

Create the SMT expression (arithmetical) right shift other >> self.

Use the function LShR() for the right logical shift

>>> x = BitVec('x', 32)
>>> 10 >> x
10 >> x
>>> (10 >> x).sexpr()
'(bvashr #b00000000000000000000000000001010 x)'

__rshift__(other)

Create the SMT expression (arithmetical) right shift self >> other

Use the function LShR() for the right logical shift

>>> x, y = BitVecs('x y', 32)
>>> x >> y
x >> y
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> evaluate(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> evaluate(BitVecVal(4, 3) >> 1)
6
>>> evaluate(LShR(BitVecVal(4, 3), 1))
2
>>> evaluate(BitVecVal(2, 3) >> 1)
1
>>> evaluate(LShR(BitVecVal(2, 3), 1))
1

__rsub__(other)

Create the SMT expression other - self.

>>> x = BitVec('x', 32)
>>> 10 - x
10 - x

__rtruediv__(other)

Create the SMT expression (signed) division other / self.

__rxor__(other)

Create the SMT expression bitwise-xor other ^ self.

>>> x = BitVec('x', 32)
>>> 10 ^ x
10 ^ x

__sub__(other)

Create the SMT expression self - other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x - y
x - y
>>> (x - y).sort()
BitVec(32)

__truediv__(other)

Create the SMT expression (signed) division self / other.

__xor__(other)

Create the SMT expression bitwise-xor self ^ other.

>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> x ^ y
x ^ y
>>> (x ^ y).sort()
BitVec(32)

size()

Return the number of bits of the bit-vector expression self.

>>> x = BitVec('x', 32)
>>> (x + 1).size()
32
>>> Concat(x, x).size()
64

sort()

Return the sort of the bit-vector expression self.

>>> x = BitVec('x', 32)
>>> x.sort()
BitVec(32)
>>> x.sort() == BitVecSort(32)
True

class cvc5.pythonic.BitVecNumRef(ast, ctx=None, reverse_children=False)

Bit-vector values.

as_long()

Return an SMT bit-vector numeral as a Python long (bignum) numeral.

>>> v = BitVecVal(0xbadc0de, 32)
>>> v
195936478
>>> print("0x%.8x" % v.as_long())
0x0badc0de

as_signed_long()

Return an SMT bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.

>>> BitVecVal(4, 3).as_signed_long()
-4
>>> BitVecVal(7, 3).as_signed_long()
-1
>>> BitVecVal(3, 3).as_signed_long()
3
>>> BitVecVal(2**32 - 1, 32).as_signed_long()
-1
>>> BitVecVal(2**64 - 1, 64).as_signed_long()
-1