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.

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