Inheritance diagram for RatNumRef:

Public Member Functions
	numerator (self)
	denominator (self)
	numerator_as_long (self)
	denominator_as_long (self)
	is_int (self)
	is_real (self)
	is_int_value (self)
	as_long (self)
	as_decimal (self, prec)
	as_string (self)
	as_fraction (self)
	py_value (self)
Public Member Functions inherited from ArithRef
	sort (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)
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

Rational values.

Definition at line 3155 of file z3py.py.

Member Function Documentation

◆ as_decimal()

as_decimal	(		self,
			prec )

 Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.

>>> v = RealVal("1/5")
>>> v.as_decimal(3)
'0.2'
>>> v = RealVal("1/3")
>>> v.as_decimal(3)
'0.333?'

Definition at line 3221 of file z3py.py.

    def as_decimal(self, prec):
        """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
 
        >>> v = RealVal("1/5")
        >>> v.as_decimal(3)
        '0.2'
        >>> v = RealVal("1/3")
        >>> v.as_decimal(3)
        '0.333?'
        """
        return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
 

◆ as_fraction()

as_fraction ( self )

Return a Z3 rational as a Python Fraction object.

>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)

Definition at line 3242 of file z3py.py.

    def as_fraction(self):
        """Return a Z3 rational as a Python Fraction object.
 
        >>> v = RealVal("1/5")
        >>> v.as_fraction()
        Fraction(1, 5)
        """
        return Fraction(self.numerator_as_long(), self.denominator_as_long())
 

◆ as_long()

as_long ( self )

Definition at line 3217 of file z3py.py.

    def as_long(self):
        _z3_assert(self.is_int_value(), "Expected integer fraction")
        return self.numerator_as_long()
 

Referenced by BitVecNumRef.as_signed_long(), denominator_as_long(), numerator_as_long(), and BitVecNumRef.py_value().

◆ as_string()

as_string ( self )

Return a Z3 rational numeral as a Python string.

>>> v = Q(3,6)
>>> v.as_string()
'1/2'

Definition at line 3233 of file z3py.py.

    def as_string(self):
        """Return a Z3 rational numeral as a Python string.
 
        >>> v = Q(3,6)
        >>> v.as_string()
        '1/2'
        """
        return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
 

Referenced by BitVecNumRef.as_long().

◆ denominator()

denominator ( self )

 Return the denominator of a Z3 rational numeral.

>>> is_rational_value(Q(3,5))
True
>>> n = Q(3,5)
>>> n.denominator()
5

Definition at line 3173 of file z3py.py.

    def denominator(self):
        """ Return the denominator of a Z3 rational numeral.
 
        >>> is_rational_value(Q(3,5))
        True
        >>> n = Q(3,5)
        >>> n.denominator()
        5
        """
        return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
 

Referenced by denominator_as_long(), and is_int_value().

◆ denominator_as_long()

denominator_as_long ( self )

 Return the denominator as a Python long.

>>> v = RealVal("1/3")
>>> v
1/3
>>> v.denominator_as_long()
3

Definition at line 3197 of file z3py.py.

    def denominator_as_long(self):
        """ Return the denominator as a Python long.
 
        >>> v = RealVal("1/3")
        >>> v
        1/3
        >>> v.denominator_as_long()
        3
        """
        return self.denominator().as_long()
 

Referenced by as_fraction(), and is_int_value().

◆ is_int()

is_int ( self )

Return `True` if `self` is an integer expression.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> y = Real('y')
>>> (x + y).is_int()
False

Reimplemented from ArithRef.

Definition at line 3208 of file z3py.py.

    def is_int(self):
        return False
 

Referenced by is_int_value().

◆ is_int_value()

is_int_value ( self )

Definition at line 3214 of file z3py.py.

    def is_int_value(self):
        return self.denominator().is_int() and self.denominator_as_long() == 1
 

Referenced by as_long().

◆ is_real()

is_real ( self )

Return `True` if `self` is an real expression.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True

Reimplemented from ArithRef.

Definition at line 3211 of file z3py.py.

    def is_real(self):
        return True
 

◆ numerator()

numerator ( self )

 Return the numerator of a Z3 rational numeral.

>>> is_rational_value(RealVal("3/5"))
True
>>> n = RealVal("3/5")
>>> n.numerator()
3
>>> is_rational_value(Q(3,5))
True
>>> Q(3,5).numerator()
3

Definition at line 3158 of file z3py.py.

    def numerator(self):
        """ Return the numerator of a Z3 rational numeral.
 
        >>> is_rational_value(RealVal("3/5"))
        True
        >>> n = RealVal("3/5")
        >>> n.numerator()
        3
        >>> is_rational_value(Q(3,5))
        True
        >>> Q(3,5).numerator()
        3
        """
        return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
 

Referenced by numerator_as_long().

◆ numerator_as_long()

numerator_as_long ( self )

 Return the numerator as a Python long.

>>> v = RealVal(10000000000)
>>> v
10000000000
>>> v + 1
10000000000 + 1
>>> v.numerator_as_long() + 1 == 10000000001
True

Definition at line 3184 of file z3py.py.

    def numerator_as_long(self):
        """ Return the numerator as a Python long.
 
        >>> v = RealVal(10000000000)
        >>> v
        10000000000
        >>> v + 1
        10000000000 + 1
        >>> v.numerator_as_long() + 1 == 10000000001
        True
        """
        return self.numerator().as_long()
 

Referenced by as_fraction(), and as_long().

◆ py_value()

py_value ( self )

Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 3251 of file z3py.py.

    def py_value(self):
        return Z3_get_numeral_double(self.ctx_ref(), self.as_ast())

Public Member Functions

Additional Inherited Members