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?'
Definition at line 2823 of file z3py.py.
def as_fraction | ( | self | ) |
def as_long | ( | 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 2835 of file z3py.py.
Referenced by 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 2775 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 2799 of file z3py.py.
Referenced by RatNumRef.as_fraction().
def is_int | ( | self | ) |
def is_int_value | ( | self | ) |
def is_real | ( | self | ) |
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 2760 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 2786 of file z3py.py.
Referenced by RatNumRef.as_fraction(), and RatNumRef.as_long().