|
def | numerator (self) |
|
def | denominator (self) |
|
def | numerator_as_long (self) |
|
def | denominator_as_long (self) |
|
def | is_int (self) |
|
def | is_real (self) |
|
def | is_int_value (self) |
|
def | as_long (self) |
|
def | as_decimal (self, prec) |
|
def | as_string (self) |
|
def | as_fraction (self) |
|
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) |
|
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) |
|
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) |
|
def | use_pp (self) |
|
Rational values.
Definition at line 2746 of file z3py.py.
◆ as_decimal()
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?'
Definition at line 2812 of file z3py.py.
2812 def as_decimal(self, prec):
2813 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 2815 >>> v = RealVal("1/5") 2818 >>> v = RealVal("1/3") 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...
◆ as_fraction()
Return a Z3 rational as a Python Fraction object.
>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)
Definition at line 2833 of file z3py.py.
2833 def as_fraction(self):
2834 """Return a Z3 rational as a Python Fraction object. 2836 >>> v = RealVal("1/5") 2840 return Fraction(self.numerator_as_long(), self.denominator_as_long())
◆ as_long()
Definition at line 2808 of file z3py.py.
2809 _z3_assert(self.is_int_value(),
"Expected integer fraction")
2810 return self.numerator_as_long()
◆ as_string()
Return a Z3 rational numeral as a Python string.
>>> v = Q(3,6)
>>> v.as_string()
'1/2'
Definition at line 2824 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long().
2824 def as_string(self):
2825 """Return a Z3 rational numeral as a Python string. Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
◆ denominator()
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 2764 of file z3py.py.
2764 def denominator(self):
2765 """ Return the denominator of a Z3 rational numeral. 2767 >>> is_rational_value(Q(3,5)) Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
◆ denominator_as_long()
def 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 2788 of file z3py.py.
2788 def denominator_as_long(self):
2789 """ Return the denominator as a Python long. 2791 >>> v = RealVal("1/3") 2794 >>> v.denominator_as_long() 2797 return self.denominator().as_long()
◆ is_int()
◆ is_int_value()
Definition at line 2805 of file z3py.py.
2806 return self.denominator().
is_int()
and self.denominator_as_long() == 1
◆ is_real()
◆ numerator()
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 2749 of file z3py.py.
2749 def numerator(self):
2750 """ Return the numerator of a Z3 rational numeral. 2752 >>> is_rational_value(RealVal("3/5")) 2754 >>> n = RealVal("3/5") 2757 >>> is_rational_value(Q(3,5)) 2759 >>> Q(3,5).numerator() 2762 return IntNumRef(
Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
◆ numerator_as_long()
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
Definition at line 2775 of file z3py.py.
2775 def numerator_as_long(self):
2776 """ Return the numerator as a Python long. 2778 >>> v = RealVal(10000000000) 2783 >>> v.numerator_as_long() + 1 == 10000000001 2786 return self.numerator().as_long()