Public Member Functions | |
ebits (self) | |
sbits (self) | |
cast (self, val) | |
![]() | |
as_ast (self) | |
get_id (self) | |
kind (self) | |
subsort (self, other) | |
name (self) | |
__eq__ (self, other) | |
__ne__ (self, other) | |
__hash__ (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) | |
cast | ( | self, | |
val ) |
Try to cast `val` as a floating-point expression. >>> b = FPSort(8, 24) >>> b.cast(1.0) 1 >>> b.cast(1.0).sexpr() '(fp #b0 #x7f #b00000000000000000000000)'
Reimplemented from SortRef.
Definition at line 9618 of file z3py.py.
ebits | ( | self | ) |
Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`. >>> b = FPSort(8, 24) >>> b.ebits() 8
Definition at line 9602 of file z3py.py.
sbits | ( | self | ) |
Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`. >>> b = FPSort(8, 24) >>> b.sbits() 24
Definition at line 9610 of file z3py.py.