|
def | numerator (self) |
|
def | denominator (self) |
|
def | numerator_as_long (self) |
|
def | denominator_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 | decl (self) |
|
def | num_args (self) |
|
def | arg (self, idx) |
|
def | children (self) |
|
def | __init__ (self, ast, ctx=None) |
|
def | __del__ (self) |
|
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 | hash (self) |
|
def | use_pp (self) |
|
Rational values.
Definition at line 2587 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 2640 of file z3py.py.
2640 def as_decimal(self, prec):
2641 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 2643 >>> v = RealVal("1/5") 2646 >>> 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 2661 of file z3py.py.
2661 def as_fraction(self):
2662 """Return a Z3 rational as a Python Fraction object. 2664 >>> v = RealVal("1/5") 2668 return Fraction(self.numerator_as_long(), self.denominator_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 2652 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long().
2652 def as_string(self):
2653 """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 2605 of file z3py.py.
2605 def denominator(self):
2606 """ Return the denominator of a Z3 rational numeral. 2608 >>> 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 2629 of file z3py.py.
2629 def denominator_as_long(self):
2630 """ Return the denominator as a Python long. 2632 >>> v = RealVal("1/3") 2635 >>> v.denominator_as_long() 2638 return self.denominator().as_long()
§ 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 2590 of file z3py.py.
2590 def numerator(self):
2591 """ Return the numerator of a Z3 rational numeral. 2593 >>> is_rational_value(RealVal("3/5")) 2595 >>> n = RealVal("3/5") 2598 >>> is_rational_value(Q(3,5)) 2600 >>> Q(3,5).numerator() 2603 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 2616 of file z3py.py.
2616 def numerator_as_long(self):
2617 """ Return the numerator as a Python long. 2619 >>> v = RealVal(10000000000) 2624 >>> v.numerator_as_long() + 1 == 10000000001 2627 return self.numerator().as_long()