Public Member Functions | |
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 | __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 | 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) |
Additional Inherited Members | |
![]() | |
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 | ) |
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 2586 of file z3py.py.
Referenced by BitVecNumRef.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 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().