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 (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 | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (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 3051 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 3054 of file z3py.py.

3054 def approx(self, precision=10):
3055 """Return a Z3 rational number that approximates the algebraic number `self`.
3056 The result `r` is such that |r - self| <= 1/10^precision
3057
3058 >>> x = simplify(Sqrt(2))
3059 >>> x.approx(20)
3060 6838717160008073720548335/4835703278458516698824704
3061 >>> x.approx(5)
3062 2965821/2097152
3063 """
3064 return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
3065
z3py.simplify
def simplify(a, *arguments, **keywords)
Utils.
Definition: z3py.py:8645
z3py.Sqrt
def Sqrt(a, ctx=None)
Definition: z3py.py:3373
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...

## ◆ 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 3066 of file z3py.py.

3066 def as_decimal(self, prec):
3067 """Return a string representation of the algebraic number `self` in decimal notation
3068 using `prec` decimal places.
3069
3070 >>> x = simplify(Sqrt(2))
3071 >>> x.as_decimal(10)
3072 '1.4142135623?'
3073 >>> x.as_decimal(20)
3074 '1.41421356237309504880?'
3075 """
3076 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
3077
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.

## ◆ index()

def index | ( |  | self | ) |

Definition at line 3081 of file z3py.py.

3081 def index(self):
3082 return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())
3083
3084
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.

## ◆ poly()

def poly | ( |  | self | ) |

Definition at line 3078 of file z3py.py.

3078 def poly(self):
3079 return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx)
3080
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.