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)

	__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)

Data Fields
	ctx

Data Fields inherited from ArithRef
	ctx

Data Fields inherited from ExprRef
	ctx

	ast

Data Fields inherited from AstRef
	ast

	ctx

Additional Inherited Members
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(), RatNumRef.denominator_as_long(), RatNumRef.numerator_as_long(), IntNumRef.py_value(), 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 IntNumRef.as_long(), and 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 RatNumRef.denominator_as_long(), and RatNumRef.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 RatNumRef.as_fraction(), and RatNumRef.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 IntNumRef.as_long(), RatNumRef.is_int_value(), and ArithSortRef.subsort().

◆ 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 RatNumRef.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 RatNumRef.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 RatNumRef.as_fraction(), and RatNumRef.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())

Field Documentation

◆ ctx

ctx

Definition at line 3171 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), FiniteSetSortRef.cast(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), AstVector.push(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), DatatypeRef.update_field(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

Public Member Functions

Data Fields

Additional Inherited Members