Detailed Description
Definition at line 2939 of file z3py.py.
Member Function Documentation
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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()
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)