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) | |
![]() | |
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) | |
![]() | |
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) | |
from_string (self, s) | |
serialize (self) | |
![]() | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
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 3142 of file z3py.py.
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 3163 of file z3py.py.
as_long | ( | self | ) |
Definition at line 3138 of file z3py.py.
Referenced by BitVecNumRef.as_signed_long(), denominator_as_long(), numerator_as_long(), and BitVecNumRef.py_value().
as_string | ( | self | ) |
Return a Z3 rational numeral as a Python string. >>> v = Q(3,6) >>> v.as_string() '1/2'
Definition at line 3154 of file z3py.py.
Referenced by BitVecNumRef.as_long().
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 3094 of file z3py.py.
Referenced by denominator_as_long(), and is_int_value().
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 3118 of file z3py.py.
Referenced by as_fraction(), and is_int_value().
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 3129 of file z3py.py.
Referenced by is_int_value().
is_int_value | ( | self | ) |
is_real | ( | self | ) |
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 3079 of file z3py.py.
Referenced by 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 3105 of file z3py.py.
Referenced by as_fraction(), and as_long().