Public Member Functions | |
sort (self) | |
ebits (self) | |
sbits (self) | |
as_string (self) | |
__le__ (self, other) | |
__lt__ (self, other) | |
__ge__ (self, other) | |
__gt__ (self, other) | |
__add__ (self, other) | |
__radd__ (self, other) | |
__sub__ (self, other) | |
__rsub__ (self, other) | |
__mul__ (self, other) | |
__rmul__ (self, other) | |
__pos__ (self) | |
__neg__ (self) | |
__div__ (self, other) | |
__rdiv__ (self, other) | |
__truediv__ (self, other) | |
__rtruediv__ (self, other) | |
__mod__ (self, other) | |
__rmod__ (self, other) | |
![]() | |
as_ast (self) | |
get_id (self) | |
sort_kind (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__ne__ (self, other) | |
params (self) | |
decl (self) | |
kind (self) | |
num_args (self) | |
arg (self, idx) | |
children (self) | |
from_string (self, s) | |
serialize (self) | |
![]() | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
py_value (self) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
__add__ | ( | self, | |
other ) |
Create the Z3 expression `self + other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x + y x + y >>> (x + y).sort() FPSort(8, 24)
Definition at line 9752 of file z3py.py.
__div__ | ( | self, | |
other ) |
Create the Z3 expression `self / other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x / y x / y >>> (x / y).sort() FPSort(8, 24) >>> 10 / y 1.25*(2**3) / y
Definition at line 9839 of file z3py.py.
__ge__ | ( | self, | |
other ) |
__gt__ | ( | self, | |
other ) |
__le__ | ( | self, | |
other ) |
__lt__ | ( | self, | |
other ) |
__mod__ | ( | self, | |
other ) |
__mul__ | ( | self, | |
other ) |
Create the Z3 expression `self * other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x * y x * y >>> (x * y).sort() FPSort(8, 24) >>> 10 * y 1.25*(2**3) * y
Definition at line 9798 of file z3py.py.
__neg__ | ( | self | ) |
__pos__ | ( | self | ) |
__radd__ | ( | self, | |
other ) |
Create the Z3 expression `other + self`. >>> x = FP('x', FPSort(8, 24)) >>> 10 + x 1.25*(2**3) + x
Definition at line 9765 of file z3py.py.
__rdiv__ | ( | self, | |
other ) |
Create the Z3 expression `other / self`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x / y x / y >>> x / 10 x / 1.25*(2**3)
Definition at line 9854 of file z3py.py.
__rmod__ | ( | self, | |
other ) |
__rmul__ | ( | self, | |
other ) |
Create the Z3 expression `other * self`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x * y x * y >>> x * 10 x * 1.25*(2**3)
Definition at line 9813 of file z3py.py.
__rsub__ | ( | self, | |
other ) |
Create the Z3 expression `other - self`. >>> x = FP('x', FPSort(8, 24)) >>> 10 - x 1.25*(2**3) - x
Definition at line 9788 of file z3py.py.
__rtruediv__ | ( | self, | |
other ) |
__sub__ | ( | self, | |
other ) |
Create the Z3 expression `self - other`. >>> x = FP('x', FPSort(8, 24)) >>> y = FP('y', FPSort(8, 24)) >>> x - y x - y >>> (x - y).sort() FPSort(8, 24)
Definition at line 9775 of file z3py.py.
__truediv__ | ( | self, | |
other ) |
as_string | ( | self | ) |
Return a Z3 floating point expression as a Python string.
Reimplemented in FPNumRef.
Definition at line 9736 of file z3py.py.
ebits | ( | self | ) |
Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. >>> b = FPSort(8, 24) >>> b.ebits() 8
Definition at line 9720 of file z3py.py.
sbits | ( | self | ) |
Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`. >>> b = FPSort(8, 24) >>> b.sbits() 24
Definition at line 9728 of file z3py.py.
sort | ( | self | ) |
Return the sort of the floating-point expression `self`. >>> x = FP('1.0', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sort() == FPSort(8, 24) True
Reimplemented from ExprRef.
Definition at line 9709 of file z3py.py.