|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
|
Z3
|
|
Inheritance diagram for RatNumRef:Public Member Functions | |
| def | numerator |
| def | denominator |
| def | numerator_as_long |
| def | denominator_as_long |
| def | as_decimal |
| def | as_string |
| def | as_fraction |
| Public Member Functions inherited from ArithRef | |
| def | sort |
| def | is_int |
| def | is_real |
| def | __add__ |
| def | __radd__ |
| def | __mul__ |
| def | __rmul__ |
| def | __sub__ |
| def | __rsub__ |
| def | __pow__ |
| def | __rpow__ |
| def | __div__ |
| def | __truediv__ |
| def | __rdiv__ |
| def | __rtruediv__ |
| def | __mod__ |
| def | __rmod__ |
| def | __neg__ |
| def | __pos__ |
| def | __le__ |
| def | __lt__ |
| def | __gt__ |
| def | __ge__ |
| Public Member Functions inherited from ExprRef | |
| def | as_ast |
| def | get_id |
| def | sort |
| def | sort_kind |
| def | __eq__ |
| def | __ne__ |
| def | decl |
| def | num_args |
| def | arg |
| def | children |
| Public Member Functions inherited from AstRef | |
| def | __init__ |
| def | __del__ |
| def | __str__ |
| def | __repr__ |
| def | sexpr |
| def | as_ast |
| def | get_id |
| def | ctx_ref |
| def | eq |
| def | translate |
| def | hash |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp |
Additional Inherited Members | |
| Data Fields inherited from AstRef | |
| ast | |
| ctx | |
| 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 2574 of file z3py.py.
| def as_fraction | ( | self | ) |
| def as_string | ( | self | ) |
| 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
Definition at line 2539 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
Definition at line 2563 of file z3py.py.
Referenced by RatNumRef.as_fraction().
| 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
Definition at line 2524 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
Definition at line 2550 of file z3py.py.
Referenced by RatNumRef.as_fraction().
1.8.5