Z3
Public Member Functions
AlgebraicNumRef Class Reference
+ Inheritance diagram for AlgebraicNumRef:

Public Member Functions

def approx (self, precision=10)
 
def as_decimal (self, prec)
 
def poly (self)
 
def index (self)
 
- Public Member Functions inherited from ArithRef
def sort (self)
 
def is_int (self)
 
def is_real (self)
 
def __add__ (self, other)
 
def __radd__ (self, other)
 
def __mul__ (self, other)
 
def __rmul__ (self, other)
 
def __sub__ (self, other)
 
def __rsub__ (self, other)
 
def __pow__ (self, other)
 
def __rpow__ (self, other)
 
def __div__ (self, other)
 
def __truediv__ (self, other)
 
def __rdiv__ (self, other)
 
def __rtruediv__ (self, other)
 
def __mod__ (self, other)
 
def __rmod__ (self, other)
 
def __neg__ (self)
 
def __pos__ (self)
 
def __le__ (self, other)
 
def __lt__ (self, other)
 
def __gt__ (self, other)
 
def __ge__ (self, other)
 
- Public Member Functions inherited from ExprRef
def as_ast (self)
 
def get_id (self)
 
def sort_kind (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __ne__ (self, other)
 
def params (self)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __deepcopy__ (self, memo={})
 
def __str__ (self)
 
def __repr__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def __copy__ (self)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Algebraic irrational values.

Definition at line 2899 of file z3py.py.

Member Function Documentation

◆ approx()

def 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 2902 of file z3py.py.

2902  def approx(self, precision=10):
2903  """Return a Z3 rational number that approximates the algebraic number `self`.
2904  The result `r` is such that |r - self| <= 1/10^precision
2905 
2906  >>> x = simplify(Sqrt(2))
2907  >>> x.approx(20)
2908  6838717160008073720548335/4835703278458516698824704
2909  >>> x.approx(5)
2910  2965821/2097152
2911  """
2912  return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)

◆ as_decimal()

def 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 2913 of file z3py.py.

2913  def as_decimal(self, prec):
2914  """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
2915 
2916  >>> x = simplify(Sqrt(2))
2917  >>> x.as_decimal(10)
2918  '1.4142135623?'
2919  >>> x.as_decimal(20)
2920  '1.41421356237309504880?'
2921  """
2922  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2923 

◆ index()

def index (   self)

Definition at line 2927 of file z3py.py.

2927  def index(self):
2928  return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())
2929 

◆ poly()

def poly (   self)

Definition at line 2924 of file z3py.py.

2924  def poly(self):
2925  return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx)
2926 
Z3_algebraic_get_i
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
Z3_get_algebraic_number_upper
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...
Z3_algebraic_get_poly
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_get_numeral_decimal_string
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.