Z3: BitVecRef Class Reference

Inheritance diagram for BitVecRef:

Public Member Functions
def	sort

def	size

def	__add__

def	__radd__

def	__mul__

def	__rmul__

def	__sub__

def	__rsub__

def	__or__

def	__ror__

def	__and__

def	__rand__

def	__xor__

def	__rxor__

def	__pos__

def	__neg__

def	__invert__

def	__div__

def	__truediv__

def	__rdiv__

def	__rtruediv__

def	__mod__

def	__rmod__

def	__le__

def	__lt__

def	__gt__

def	__ge__

def	__rshift__

def	__lshift__

def	__rrshift__

def	__rlshift__

Public Member Functions inherited from ExprRef
def	as_ast

def	sort

def	sort_kind

def	__eq__

def	__ne__

def	decl

def	num_args

def	arg

def	children

Public Member Functions inherited from AstRef
def	__init__

def	__del__

def	__str__

def	__repr__

def	sexpr

def	as_ast

def	ctx_ref

def	eq

def	translate

def	hash

Public Member Functions inherited from Z3PPObject
def	use_pp

Additional Inherited Members
Data Fields inherited from AstRef
	ast

	ctx

Detailed Description

Bit-vector expressions.

Definition at line 2831 of file z3py.py.

Member Function Documentation

def __add__	(	self,
		other
	)

Create the Z3 expression `self + other`.

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

Definition at line 2856 of file z3py.py.

 
     def __add__(self, other):
         """Create the Z3 expression `self + other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x + y
         x + y
         >>> (x + y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __and__	(	self,
		other
	)

Create the Z3 expression bitwise-and `self & other`.

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

Definition at line 2948 of file z3py.py.

 
     def __and__(self, other):
         """Create the Z3 expression bitwise-and `self & other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x & y
         x & y
         >>> (x & y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvand(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __div__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3025 of file z3py.py.

 
     def __div__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __ge__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3155 of file z3py.py.

 
     def __ge__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_bvsge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __gt__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3139 of file z3py.py.

 
     def __gt__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_bvsgt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __invert__ ( self )

Create the Z3 expression bitwise-not `~self`.

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

Definition at line 3014 of file z3py.py.

 
     def __invert__(self):
         """Create the Z3 expression bitwise-not `~self`.
 
         >>> x = BitVec('x', 32)
         >>> ~x
         ~x
         >>> simplify(~(~x))
         x
         """
         return BitVecRef(Z3_mk_bvnot(self.ctx_ref(), self.as_ast()), self.ctx)

def __le__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3107 of file z3py.py.

 
     def __le__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_bvsle(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __lshift__	(	self,
		other
	)

Create the Z3 expression left shift `self << other`

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

Definition at line 3201 of file z3py.py.

 
     def __lshift__(self, other):
         """Create the Z3 expression left shift `self << other`
 
         >>> x, y = BitVecs('x y', 32)
         >>> x << y
         x << y
         >>> (x << y).sexpr()
         '(bvshl x y)'
         >>> simplify(BitVecVal(2, 3) << 1)
         4
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __lt__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3123 of file z3py.py.

 
     def __lt__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BoolRef(Z3_mk_bvslt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __mod__	(	self,
		other
	)

Create the Z3 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)'

Definition at line 3068 of file z3py.py.

 
     def __mod__(self, other):
         """Create the Z3 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)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __mul__	(	self,
		other
	)

Create the Z3 expression `self * other`.

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

Definition at line 2879 of file z3py.py.

 
     def __mul__(self, other):
         """Create the Z3 expression `self * other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x * y
         x*y
         >>> (x * y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __neg__ ( self )

Return an expression representing `-self`.

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

Definition at line 3003 of file z3py.py.

 
     def __neg__(self):
         """Return an expression representing `-self`.
 
         >>> x = BitVec('x', 32)
         >>> -x
         -x
         >>> simplify(-(-x))
         x
         """
         return BitVecRef(Z3_mk_bvneg(self.ctx_ref(), self.as_ast()), self.ctx)

def __or__	(	self,
		other
	)

Create the Z3 expression bitwise-or `self | other`.

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

Definition at line 2925 of file z3py.py.

 
     def __or__(self, other):
         """Create the Z3 expression bitwise-or `self | other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x | y
         x | y
         >>> (x | y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __pos__ ( self )

Return `self`.

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

Definition at line 2994 of file z3py.py.

 
     def __pos__(self):
         """Return `self`.
 
         >>> x = BitVec('x', 32)
         >>> +x
         x
         """
         return self

def __radd__	(	self,
		other
	)

Create the Z3 expression `other + self`.

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

Definition at line 2869 of file z3py.py.

 
     def __radd__(self, other):
         """Create the Z3 expression `other + self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 + x
         10 + x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvadd(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rand__	(	self,
		other
	)

Create the Z3 expression bitwise-or `other & self`.

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

Definition at line 2961 of file z3py.py.

 
     def __rand__(self, other):
         """Create the Z3 expression bitwise-or `other & self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 & x
         10 & x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvand(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rdiv__	(	self,
		other
	)

Create the Z3 expression (signed) division `other / self`.

Use the function UDiv() for unsigned division.

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

Definition at line 3048 of file z3py.py.

 
     def __rdiv__(self, other):
         """Create the Z3 expression (signed) division `other / self`.
 
         Use the function UDiv() for unsigned division.
 
         >>> x = BitVec('x', 32)
         >>> 10 / x
         10/x
         >>> (10 / x).sexpr()
         '(bvsdiv #x0000000a x)'
         >>> UDiv(10, x).sexpr()
         '(bvudiv #x0000000a x)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsdiv(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rlshift__	(	self,
		other
	)

Create the Z3 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 #x0000000a x)'

Definition at line 3229 of file z3py.py.

 
     def __rlshift__(self, other):
         """Create the Z3 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 #x0000000a x)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rmod__	(	self,
		other
	)

Create the Z3 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 #x0000000a x)'
>>> URem(10, x).sexpr()
'(bvurem #x0000000a x)'
>>> SRem(10, x).sexpr()
'(bvsrem #x0000000a x)'

Definition at line 3089 of file z3py.py.

 
     def __rmod__(self, other):
         """Create the Z3 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 #x0000000a x)'
         >>> URem(10, x).sexpr()
         '(bvurem #x0000000a x)'
         >>> SRem(10, x).sexpr()
         '(bvsrem #x0000000a x)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsmod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rmul__	(	self,
		other
	)

Create the Z3 expression `other * self`.

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

Definition at line 2892 of file z3py.py.

 
     def __rmul__(self, other):
         """Create the Z3 expression `other * self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 * x
         10*x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvmul(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __ror__	(	self,
		other
	)

Create the Z3 expression bitwise-or `other | self`.

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

Definition at line 2938 of file z3py.py.

 
     def __ror__(self, other):
         """Create the Z3 expression bitwise-or `other | self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 | x
         10 | x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rrshift__	(	self,
		other
	)

Create the Z3 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 #x0000000a x)'

Definition at line 3215 of file z3py.py.

 
     def __rrshift__(self, other):
         """Create the Z3 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 #x0000000a x)'
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rshift__	(	self,
		other
	)

Create the Z3 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()
-4L
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L
>>> 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

Definition at line 3171 of file z3py.py.

 
     def __rshift__(self, other):
         """Create the Z3 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()
         -4L
         >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
         -2L
         >>> 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
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvashr(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __rsub__	(	self,
		other
	)

Create the Z3 expression `other - self`.

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

Definition at line 2915 of file z3py.py.

 
     def __rsub__(self, other):
         """Create the Z3 expression `other - self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 - x
         10 - x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __rtruediv__	(	self,
		other
	)

Create the Z3 expression (signed) division `other / self`.

Definition at line 3064 of file z3py.py.

 
     def __rtruediv__(self, other):
         """Create the Z3 expression (signed) division `other / self`."""
         self.__rdiv__(other)

def __rxor__	(	self,
		other
	)

Create the Z3 expression bitwise-xor `other ^ self`.

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

Definition at line 2984 of file z3py.py.

 
     def __rxor__(self, other):
         """Create the Z3 expression bitwise-xor `other ^ self`.
         
         >>> x = BitVec('x', 32)
         >>> 10 ^ x
         10 ^ x
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

def __sub__	(	self,
		other
	)

Create the Z3 expression `self - other`.

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

Definition at line 2902 of file z3py.py.

 
     def __sub__(self, other):
         """Create the Z3 expression `self - other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x - y
         x - y
         >>> (x - y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvsub(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __truediv__	(	self,
		other
	)

Create the Z3 expression (signed) division `self / other`.

Definition at line 3044 of file z3py.py.

 
     def __truediv__(self, other):
         """Create the Z3 expression (signed) division `self / other`."""
         self.__div__(other)

def __xor__	(	self,
		other
	)

Create the Z3 expression bitwise-xor `self ^ other`.

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

Definition at line 2971 of file z3py.py.

 
     def __xor__(self, other):
         """Create the Z3 expression bitwise-xor `self ^ other`.
         
         >>> x = BitVec('x', 32)
         >>> y = BitVec('y', 32)
         >>> x ^ y
         x ^ y
         >>> (x ^ y).sort()
         BitVec(32)
         """
         a, b = _coerce_exprs(self, other)
         return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def size ( self )

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

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

Definition at line 2845 of file z3py.py.

 
     def size(self):
         """Return the number of bits of the bit-vector expression `self`.
         
         >>> x = BitVec('x', 32)
         >>> (x + 1).size()
         32
         >>> Concat(x, x).size()
         64
         """
         return self.sort().size()

def sort ( self )

Return the sort of the bit-vector expression `self`.

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

Definition at line 2834 of file z3py.py.

Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__or__(), BitVecRef.__sub__(), and BitVecRef.__xor__().

 
     def sort(self):
         """Return the sort of the bit-vector expression `self`.
 
         >>> x = BitVec('x', 32)
         >>> x.sort()
         BitVec(32)
         >>> x.sort() == BitVecSort(32)
         True
         """
         return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)

Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation