Public Member Functions | |
sign (self) | |
sign_as_bv (self) | |
significand (self) | |
significand_as_long (self) | |
significand_as_bv (self) | |
exponent (self, biased=True) | |
exponent_as_long (self, biased=True) | |
exponent_as_bv (self, biased=True) | |
isNaN (self) | |
isInf (self) | |
isZero (self) | |
isNormal (self) | |
isSubnormal (self) | |
isPositive (self) | |
isNegative (self) | |
as_string (self) | |
py_value (self) | |
![]() | |
sort (self) | |
ebits (self) | |
sbits (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) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
The sign of the numeral. >>> x = FPVal(+1.0, FPSort(8, 24)) >>> x.sign() False >>> x = FPVal(-1.0, FPSort(8, 24)) >>> x.sign() True
as_string | ( | self | ) |
Return a Z3 floating point expression as a Python string.
Reimplemented from FPRef.
Definition at line 10102 of file z3py.py.
exponent | ( | self, | |
biased = True ) |
exponent_as_bv | ( | self, | |
biased = True ) |
Definition at line 10056 of file z3py.py.
exponent_as_long | ( | self, | |
biased = True ) |
Definition at line 10045 of file z3py.py.
isInf | ( | self | ) |
isNaN | ( | self | ) |
isNegative | ( | self | ) |
isNormal | ( | self | ) |
isPositive | ( | self | ) |
isSubnormal | ( | self | ) |
isZero | ( | self | ) |
py_value | ( | self | ) |
Return a Python value that is equivalent to `self`.
Reimplemented from AstRef.
Definition at line 10106 of file z3py.py.
sign | ( | self | ) |
Definition at line 9982 of file z3py.py.
sign_as_bv | ( | self | ) |
significand | ( | self | ) |
significand_as_bv | ( | self | ) |
Definition at line 10025 of file z3py.py.
significand_as_long | ( | self | ) |
Definition at line 10014 of file z3py.py.