|
Z3
|
|
|
Z3
|
|
Inheritance diagram for RatNumRef:Public Member Functions | |
| 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) |
| Public Member Functions inherited from ArithRef | |
| def | sort (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) |
| Public Member Functions inherited from ExprRef | |
| def | as_ast (self) |
| def | get_id (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 | from_string (self, s) |
| def | serialize (self) |
| Public Member Functions inherited from AstRef | |
| def | __init__ (self, ast, ctx=None) |
| def | __del__ (self) |
| def | __deepcopy__ (self, memo={}) |
| def | __str__ (self) |
| def | __repr__ (self) |
| def | __nonzero__ (self) |
| def | __bool__ (self) |
| def | sexpr (self) |
| def | ctx_ref (self) |
| def | eq (self, other) |
| def | translate (self, target) |
| def | __copy__ (self) |
| def | hash (self) |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp (self) |
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?'
| def as_fraction | ( | self | ) |
Return a Z3 rational as a Python Fraction object.
>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)
| def as_long | ( | self | ) |
Definition at line 3054 of file z3py.py.
Referenced by BitVecNumRef.as_signed_long(), RatNumRef.denominator_as_long(), and RatNumRef.numerator_as_long().
| def as_string | ( | self | ) |
Return a Z3 rational numeral as a Python string. >>> v = Q(3,6) >>> v.as_string() '1/2'
Definition at line 3070 of file z3py.py.
Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().
| 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 3010 of file z3py.py.
Referenced by RatNumRef.denominator_as_long(), and RatNumRef.is_int_value().
| 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 3034 of file z3py.py.
Referenced by RatNumRef.as_fraction(), and RatNumRef.is_int_value().
| def 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 3045 of file z3py.py.
Referenced by IntNumRef.as_long(), RatNumRef.is_int_value(), and ArithSortRef.subsort().
| def is_int_value | ( | self | ) |
| def 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.
| 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 2995 of file z3py.py.
Referenced by RatNumRef.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 3021 of file z3py.py.
Referenced by RatNumRef.as_fraction(), and RatNumRef.as_long().
1.9.1