Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
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__

Detailed Description

Bit-vector expressions.

Definition at line 2939 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 2964 of file z3py.py.

02964 
02965     def __add__(self, other):
02966         """Create the Z3 expression `self + other`.
02967         
02968         >>> x = BitVec('x', 32)
02969         >>> y = BitVec('y', 32)
02970         >>> x + y
02971         x + y
02972         >>> (x + y).sort()
02973         BitVec(32)
02974         """
02975         a, b = _coerce_exprs(self, other)
02976         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 3056 of file z3py.py.

03056 
03057     def __and__(self, other):
03058         """Create the Z3 expression bitwise-and `self & other`.
03059         
03060         >>> x = BitVec('x', 32)
03061         >>> y = BitVec('y', 32)
03062         >>> x & y
03063         x & y
03064         >>> (x & y).sort()
03065         BitVec(32)
03066         """
03067         a, b = _coerce_exprs(self, other)
03068         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 3133 of file z3py.py.

03133 
03134     def __div__(self, other):
03135         """Create the Z3 expression (signed) division `self / other`.
03136 
03137         Use the function UDiv() for unsigned division.
03138 
03139         >>> x = BitVec('x', 32)
03140         >>> y = BitVec('y', 32)
03141         >>> x / y
03142         x/y
03143         >>> (x / y).sort()
03144         BitVec(32)
03145         >>> (x / y).sexpr()
03146         '(bvsdiv x y)'
03147         >>> UDiv(x, y).sexpr()
03148         '(bvudiv x y)'
03149         """
03150         a, b = _coerce_exprs(self, other)
03151         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 3263 of file z3py.py.

03263 
03264     def __ge__(self, other):
03265         """Create the Z3 expression (signed) `other >= self`.
03266         
03267         Use the function UGE() for unsigned greater than or equal to.
03268 
03269         >>> x, y = BitVecs('x y', 32)
03270         >>> x >= y
03271         x >= y
03272         >>> (x >= y).sexpr()
03273         '(bvsge x y)'
03274         >>> UGE(x, y).sexpr()
03275         '(bvuge x y)'
03276         """
03277         a, b = _coerce_exprs(self, other)
03278         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 3247 of file z3py.py.

03247 
03248     def __gt__(self, other):
03249         """Create the Z3 expression (signed) `other > self`.
03250         
03251         Use the function UGT() for unsigned greater than.
03252 
03253         >>> x, y = BitVecs('x y', 32)
03254         >>> x > y
03255         x > y
03256         >>> (x > y).sexpr()
03257         '(bvsgt x y)'
03258         >>> UGT(x, y).sexpr()
03259         '(bvugt x y)'
03260         """
03261         a, b = _coerce_exprs(self, other)
03262         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 3122 of file z3py.py.

03122 
03123     def __invert__(self):
03124         """Create the Z3 expression bitwise-not `~self`.
03125 
03126         >>> x = BitVec('x', 32)
03127         >>> ~x
03128         ~x
03129         >>> simplify(~(~x))
03130         x
03131         """
03132         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 3215 of file z3py.py.

03215 
03216     def __le__(self, other):
03217         """Create the Z3 expression (signed) `other <= self`.
03218         
03219         Use the function ULE() for unsigned less than or equal to.
03220 
03221         >>> x, y = BitVecs('x y', 32)
03222         >>> x <= y
03223         x <= y
03224         >>> (x <= y).sexpr()
03225         '(bvsle x y)'
03226         >>> ULE(x, y).sexpr()
03227         '(bvule x y)'
03228         """
03229         a, b = _coerce_exprs(self, other)
03230         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 3309 of file z3py.py.

03309 
03310     def __lshift__(self, other):
03311         """Create the Z3 expression left shift `self << other`
03312 
03313         >>> x, y = BitVecs('x y', 32)
03314         >>> x << y
03315         x << y
03316         >>> (x << y).sexpr()
03317         '(bvshl x y)'
03318         >>> simplify(BitVecVal(2, 3) << 1)
03319         4
03320         """
03321         a, b = _coerce_exprs(self, other)
03322         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 3231 of file z3py.py.

03231 
03232     def __lt__(self, other):
03233         """Create the Z3 expression (signed) `other < self`.
03234         
03235         Use the function ULT() for unsigned less than.
03236 
03237         >>> x, y = BitVecs('x y', 32)
03238         >>> x < y
03239         x < y
03240         >>> (x < y).sexpr()
03241         '(bvslt x y)'
03242         >>> ULT(x, y).sexpr()
03243         '(bvult x y)'
03244         """
03245         a, b = _coerce_exprs(self, other)
03246         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 3176 of file z3py.py.

03176 
03177     def __mod__(self, other):
03178         """Create the Z3 expression (signed) mod `self % other`.
03179 
03180         Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03181 
03182         >>> x = BitVec('x', 32)
03183         >>> y = BitVec('y', 32)
03184         >>> x % y
03185         x%y
03186         >>> (x % y).sort()
03187         BitVec(32)
03188         >>> (x % y).sexpr()
03189         '(bvsmod x y)'
03190         >>> URem(x, y).sexpr()
03191         '(bvurem x y)'
03192         >>> SRem(x, y).sexpr()
03193         '(bvsrem x y)'
03194         """
03195         a, b = _coerce_exprs(self, other)
03196         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 2987 of file z3py.py.

02987 
02988     def __mul__(self, other):
02989         """Create the Z3 expression `self * other`.
02990         
02991         >>> x = BitVec('x', 32)
02992         >>> y = BitVec('y', 32)
02993         >>> x * y
02994         x*y
02995         >>> (x * y).sort()
02996         BitVec(32)
02997         """
02998         a, b = _coerce_exprs(self, other)
02999         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 3111 of file z3py.py.

03111 
03112     def __neg__(self):
03113         """Return an expression representing `-self`.
03114 
03115         >>> x = BitVec('x', 32)
03116         >>> -x
03117         -x
03118         >>> simplify(-(-x))
03119         x
03120         """
03121         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 3033 of file z3py.py.

03033 
03034     def __or__(self, other):
03035         """Create the Z3 expression bitwise-or `self | other`.
03036         
03037         >>> x = BitVec('x', 32)
03038         >>> y = BitVec('y', 32)
03039         >>> x | y
03040         x | y
03041         >>> (x | y).sort()
03042         BitVec(32)
03043         """
03044         a, b = _coerce_exprs(self, other)
03045         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 3102 of file z3py.py.

03102 
03103     def __pos__(self):
03104         """Return `self`.
03105 
03106         >>> x = BitVec('x', 32)
03107         >>> +x
03108         x
03109         """
03110         return self

def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 2977 of file z3py.py.

02977 
02978     def __radd__(self, other):
02979         """Create the Z3 expression `other + self`.
02980         
02981         >>> x = BitVec('x', 32)
02982         >>> 10 + x
02983         10 + x
02984         """
02985         a, b = _coerce_exprs(self, other)
02986         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 3069 of file z3py.py.

03069 
03070     def __rand__(self, other):
03071         """Create the Z3 expression bitwise-or `other & self`.
03072         
03073         >>> x = BitVec('x', 32)
03074         >>> 10 & x
03075         10 & x
03076         """
03077         a, b = _coerce_exprs(self, other)
03078         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 3156 of file z3py.py.

03156 
03157     def __rdiv__(self, other):
03158         """Create the Z3 expression (signed) division `other / self`.
03159 
03160         Use the function UDiv() for unsigned division.
03161 
03162         >>> x = BitVec('x', 32)
03163         >>> 10 / x
03164         10/x
03165         >>> (10 / x).sexpr()
03166         '(bvsdiv #x0000000a x)'
03167         >>> UDiv(10, x).sexpr()
03168         '(bvudiv #x0000000a x)'
03169         """
03170         a, b = _coerce_exprs(self, other)
03171         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 3337 of file z3py.py.

03337 
03338     def __rlshift__(self, other):
03339         """Create the Z3 expression left shift `other << self`.
03340 
03341         Use the function LShR() for the right logical shift
03342 
03343         >>> x = BitVec('x', 32)
03344         >>> 10 << x
03345         10 << x
03346         >>> (10 << x).sexpr()
03347         '(bvshl #x0000000a x)'
03348         """
03349         a, b = _coerce_exprs(self, other)
03350         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 3197 of file z3py.py.

03197 
03198     def __rmod__(self, other):
03199         """Create the Z3 expression (signed) mod `other % self`.
03200 
03201         Use the function URem() for unsigned remainder, and SRem() for signed remainder.
03202 
03203         >>> x = BitVec('x', 32)
03204         >>> 10 % x
03205         10%x
03206         >>> (10 % x).sexpr()
03207         '(bvsmod #x0000000a x)'
03208         >>> URem(10, x).sexpr()
03209         '(bvurem #x0000000a x)'
03210         >>> SRem(10, x).sexpr()
03211         '(bvsrem #x0000000a x)'
03212         """
03213         a, b = _coerce_exprs(self, other)
03214         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 3000 of file z3py.py.

03000 
03001     def __rmul__(self, other):
03002         """Create the Z3 expression `other * self`.
03003         
03004         >>> x = BitVec('x', 32)
03005         >>> 10 * x
03006         10*x
03007         """
03008         a, b = _coerce_exprs(self, other)
03009         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 3046 of file z3py.py.

03046 
03047     def __ror__(self, other):
03048         """Create the Z3 expression bitwise-or `other | self`.
03049         
03050         >>> x = BitVec('x', 32)
03051         >>> 10 | x
03052         10 | x
03053         """
03054         a, b = _coerce_exprs(self, other)
03055         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 3323 of file z3py.py.

03323 
03324     def __rrshift__(self, other):
03325         """Create the Z3 expression (arithmetical) right shift `other` >> `self`.
03326 
03327         Use the function LShR() for the right logical shift
03328 
03329         >>> x = BitVec('x', 32)
03330         >>> 10 >> x
03331         10 >> x
03332         >>> (10 >> x).sexpr()
03333         '(bvashr #x0000000a x)'
03334         """
03335         a, b = _coerce_exprs(self, other)
03336         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()
-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

Definition at line 3279 of file z3py.py.

03279 
03280     def __rshift__(self, other):
03281         """Create the Z3 expression (arithmetical) right shift `self >> other`
03282 
03283         Use the function LShR() for the right logical shift
03284 
03285         >>> x, y = BitVecs('x y', 32)
03286         >>> x >> y
03287         x >> y
03288         >>> (x >> y).sexpr()
03289         '(bvashr x y)'
03290         >>> LShR(x, y).sexpr()
03291         '(bvlshr x y)'
03292         >>> BitVecVal(4, 3)
03293         4
03294         >>> BitVecVal(4, 3).as_signed_long()
03295         -4
03296         >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
03297         -2
03298         >>> simplify(BitVecVal(4, 3) >> 1)
03299         6
03300         >>> simplify(LShR(BitVecVal(4, 3), 1))
03301         2
03302         >>> simplify(BitVecVal(2, 3) >> 1)
03303         1
03304         >>> simplify(LShR(BitVecVal(2, 3), 1))
03305         1
03306         """
03307         a, b = _coerce_exprs(self, other)
03308         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 3023 of file z3py.py.

03023 
03024     def __rsub__(self, other):
03025         """Create the Z3 expression `other - self`.
03026         
03027         >>> x = BitVec('x', 32)
03028         >>> 10 - x
03029         10 - x
03030         """
03031         a, b = _coerce_exprs(self, other)
03032         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 3172 of file z3py.py.

03172 
03173     def __rtruediv__(self, other):
03174         """Create the Z3 expression (signed) division `other / self`."""
03175         return 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 3092 of file z3py.py.

03092 
03093     def __rxor__(self, other):
03094         """Create the Z3 expression bitwise-xor `other ^ self`.
03095         
03096         >>> x = BitVec('x', 32)
03097         >>> 10 ^ x
03098         10 ^ x
03099         """
03100         a, b = _coerce_exprs(self, other)
03101         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 3010 of file z3py.py.

03010 
03011     def __sub__(self, other):
03012         """Create the Z3 expression `self - other`.
03013         
03014         >>> x = BitVec('x', 32)
03015         >>> y = BitVec('y', 32)
03016         >>> x - y
03017         x - y
03018         >>> (x - y).sort()
03019         BitVec(32)
03020         """
03021         a, b = _coerce_exprs(self, other)
03022         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 3152 of file z3py.py.

03152 
03153     def __truediv__(self, other):
03154         """Create the Z3 expression (signed) division `self / other`."""
03155         return 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 3079 of file z3py.py.

03079 
03080     def __xor__(self, other):
03081         """Create the Z3 expression bitwise-xor `self ^ other`.
03082         
03083         >>> x = BitVec('x', 32)
03084         >>> y = BitVec('y', 32)
03085         >>> x ^ y
03086         x ^ y
03087         >>> (x ^ y).sort()
03088         BitVec(32)
03089         """
03090         a, b = _coerce_exprs(self, other)
03091         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 2953 of file z3py.py.

02953 
02954     def size(self):
02955         """Return the number of bits of the bit-vector expression `self`.
02956         
02957         >>> x = BitVec('x', 32)
02958         >>> (x + 1).size()
02959         32
02960         >>> Concat(x, x).size()
02961         64
02962         """
02963         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

Reimplemented from ExprRef.

Definition at line 2942 of file z3py.py.

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

02942 
02943     def sort(self):
02944         """Return the sort of the bit-vector expression `self`.
02945 
02946         >>> x = BitVec('x', 32)
02947         >>> x.sort()
02948         BitVec(32)
02949         >>> x.sort() == BitVecSort(32)
02950         True
02951         """
02952         return BitVecSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines