Public Member Functions | |
approx (self, precision=10) | |
as_decimal (self, prec) | |
poly (self) | |
index (self) | |
![]() | |
sort (self) | |
is_int (self) | |
is_real (self) | |
__add__ (self, other) | |
__radd__ (self, other) | |
__mul__ (self, other) | |
__rmul__ (self, other) | |
__sub__ (self, other) | |
__rsub__ (self, other) | |
__pow__ (self, other) | |
__rpow__ (self, other) | |
__div__ (self, other) | |
__truediv__ (self, other) | |
__rdiv__ (self, other) | |
__rtruediv__ (self, other) | |
__mod__ (self, other) | |
__rmod__ (self, other) | |
__neg__ (self) | |
__pos__ (self) | |
__le__ (self, other) | |
__lt__ (self, other) | |
__gt__ (self, other) | |
__ge__ (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) | |
approx | ( | self, | |
precision = 10 ) |
Return a Z3 rational number that approximates the algebraic number `self`. The result `r` is such that |r - self| <= 1/10^precision >>> x = simplify(Sqrt(2)) >>> x.approx(20) 6838717160008073720548335/4835703278458516698824704 >>> x.approx(5) 2965821/2097152
Definition at line 3179 of file z3py.py.
as_decimal | ( | self, | |
prec ) |
Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places. >>> x = simplify(Sqrt(2)) >>> x.as_decimal(10) '1.4142135623?' >>> x.as_decimal(20) '1.41421356237309504880?'
Definition at line 3191 of file z3py.py.
index | ( | self | ) |