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)
	__abs__ (self)
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)
	update (self, *args)
	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 3277 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 3280 of file z3py.py.

    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
        """
        return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
 

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

    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?'
        """
        return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
 

◆ index()

index ( self )

Definition at line 3307 of file z3py.py.

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

◆ poly()

poly ( self )

Definition at line 3304 of file z3py.py.

    def poly(self):
        return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx)
 