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

Public Member Functions

def approx
def as_decimal

Detailed Description

Algebraic irrational values.

Definition at line 2579 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 2582 of file z3py.py.

02582 
02583     def approx(self, precision=10):
02584         """Return a Z3 rational number that approximates the algebraic number `self`. 
02585         The result `r` is such that |r - self| <= 1/10^precision 
02586         
02587         >>> x = simplify(Sqrt(2))
02588         >>> x.approx(20)
02589         6838717160008073720548335/4835703278458516698824704
02590         >>> x.approx(5)
02591         2965821/2097152
02592         """
        return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
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 2593 of file z3py.py.

02593 
02594     def as_decimal(self, prec):
02595         """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
02596 
02597         >>> x = simplify(Sqrt(2))
02598         >>> x.as_decimal(10)
02599         '1.4142135623?'
02600         >>> x.as_decimal(20)
02601         '1.41421356237309504880?'
02602         """
02603         return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines