Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
AlgebraicNumRef Class Reference
+ Inheritance diagram for AlgebraicNumRef:

Public Member Functions

def approx
 
def as_decimal
 
- Public Member Functions inherited from ArithRef
def sort
 
def is_int
 
def is_real
 
def __add__
 
def __radd__
 
def __mul__
 
def __rmul__
 
def __sub__
 
def __rsub__
 
def __pow__
 
def __rpow__
 
def __div__
 
def __truediv__
 
def __rdiv__
 
def __rtruediv__
 
def __mod__
 
def __rmod__
 
def __neg__
 
def __pos__
 
def __le__
 
def __lt__
 
def __gt__
 
def __ge__
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Algebraic irrational values.

Definition at line 2853 of file z3py.py.

Member Function Documentation

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

2857  def approx(self, precision=10):
2858  """Return a Z3 rational number that approximates the algebraic number `self`.
2859  The result `r` is such that |r - self| <= 1/10^precision
2860 
2861  >>> x = simplify(Sqrt(2))
2862  >>> x.approx(20)
2863  6838717160008073720548335/4835703278458516698824704
2864  >>> x.approx(5)
2865  2965821/2097152
2866  """
return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
def as_ast
Definition: z3py.py:344
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...
def ctx_ref
Definition: z3py.py:352
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 2867 of file z3py.py.

2868  def as_decimal(self, prec):
2869  """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
2870 
2871  >>> x = simplify(Sqrt(2))
2872  >>> x.as_decimal(10)
2873  '1.4142135623?'
2874  >>> x.as_decimal(20)
2875  '1.41421356237309504880?'
2876  """
2877  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
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...
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352