Z3
Loading...
Searching...
No Matches
AlgebraicNumRef Class Reference
Inheritance diagram for AlgebraicNumRef:

Public Member Functions

 approx (self, precision=10)
 as_decimal (self, prec)
 poly (self)
 index (self)
Public Member Functions inherited from ArithRef
 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)
Public Member Functions inherited from ExprRef
 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)
Public Member Functions inherited from AstRef
 __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)
Public Member Functions inherited from Z3PPObject
 use_pp (self)

Additional Inherited Members

Data Fields inherited from AstRef
 ast = ast
 ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)

Detailed Description

Algebraic irrational values.

Definition at line 3176 of file z3py.py.

Member Function Documentation

◆ approx()

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.

3179 def approx(self, precision=10):
3180 """Return a Z3 rational number that approximates the algebraic number `self`.
3181 The result `r` is such that |r - self| <= 1/10^precision
3182
3183 >>> x = simplify(Sqrt(2))
3184 >>> x.approx(20)
3185 6838717160008073720548335/4835703278458516698824704
3186 >>> x.approx(5)
3187 2965821/2097152
3188 """
3189 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
3190
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...

◆ as_decimal()

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.

3191 def as_decimal(self, prec):
3192 """Return a string representation of the algebraic number `self` in decimal notation
3193 using `prec` decimal places.
3194
3195 >>> x = simplify(Sqrt(2))
3196 >>> x.as_decimal(10)
3197 '1.4142135623?'
3198 >>> x.as_decimal(20)
3199 '1.41421356237309504880?'
3200 """
3201 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3202
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.

◆ index()

index ( self)

Definition at line 3206 of file z3py.py.

3206 def index(self):
3207 return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())
3208
3209
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.

◆ poly()

poly ( self)

Definition at line 3203 of file z3py.py.

3203 def poly(self):
3204 return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx)
3205
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.