|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
|
Z3
|
|
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 | get_id |
| 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 | get_id |
| 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 | |
| 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 2989 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)
Definition at line 3081 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)'
Definition at line 3158 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)'
Definition at line 3288 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)'
Definition at line 3272 of file z3py.py.
| def __invert__ | ( | self | ) |
Create the Z3 expression bitwise-not `~self`.
>>> x = BitVec('x', 32)
>>> ~x
~x
>>> simplify(~(~x))
x
Definition at line 3147 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)'
Definition at line 3240 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
Definition at line 3334 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)'
Definition at line 3256 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)'
Definition at line 3201 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)
Definition at line 3012 of file z3py.py.
| def __neg__ | ( | self | ) |
Return an expression representing `-self`.
>>> x = BitVec('x', 32)
>>> -x
-x
>>> simplify(-(-x))
x
Definition at line 3136 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)
Definition at line 3058 of file z3py.py.
| def __pos__ | ( | self | ) |
| def __radd__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression `other + self`.
>>> x = BitVec('x', 32)
>>> 10 + x
10 + x
Definition at line 3002 of file z3py.py.
| def __rand__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression bitwise-or `other & self`.
>>> x = BitVec('x', 32)
>>> 10 & x
10 & x
Definition at line 3094 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)'
Definition at line 3181 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)'
Definition at line 3362 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)'
Definition at line 3222 of file z3py.py.
| def __rmul__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression `other * self`.
>>> x = BitVec('x', 32)
>>> 10 * x
10*x
Definition at line 3025 of file z3py.py.
| def __ror__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression bitwise-or `other | self`.
>>> x = BitVec('x', 32)
>>> 10 | x
10 | x
Definition at line 3071 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)'
Definition at line 3348 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()
-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 3304 of file z3py.py.
| def __rsub__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression `other - self`.
>>> x = BitVec('x', 32)
>>> 10 - x
10 - x
Definition at line 3048 of file z3py.py.
| def __rtruediv__ | ( | self, | |
| other | |||
| ) |
| def __rxor__ | ( | self, | |
| other | |||
| ) |
Create the Z3 expression bitwise-xor `other ^ self`.
>>> x = BitVec('x', 32)
>>> 10 ^ x
10 ^ x
Definition at line 3117 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)
Definition at line 3035 of file z3py.py.
| def __truediv__ | ( | self, | |
| 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 3104 of file z3py.py.
| def size | ( | self | ) |
| 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 2967 of file z3py.py.
Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__or__(), BitVecRef.__sub__(), and BitVecRef.__xor__().
1.8.5