Public Member Functions | |
def | numerator |
def | denominator |
def | numerator_as_long |
def | denominator_as_long |
def | as_decimal |
def | as_string |
def | as_fraction |
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 2549 of file z3py.py.
02549 02550 def as_decimal(self, prec): 02551 """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places. 02552 02553 >>> v = RealVal("1/5") 02554 >>> v.as_decimal(3) 02555 '0.2' 02556 >>> v = RealVal("1/3") 02557 >>> v.as_decimal(3) 02558 '0.333?' 02559 """ 02560 return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
def 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 2570 of file z3py.py.
02570 02571 def as_fraction(self): 02572 """Return a Z3 rational as a Python Fraction object. 02573 02574 >>> v = RealVal("1/5") 02575 >>> v.as_fraction() 02576 Fraction(1, 5) 02577 """ 02578 return Fraction(self.numerator_as_long(), self.denominator_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 2561 of file z3py.py.
02561 02562 def as_string(self): 02563 """Return a Z3 rational numeral as a Python string. 02564 02565 >>> v = Q(3,6) 02566 >>> v.as_string() 02567 '1/2' 02568 """ 02569 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
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 2514 of file z3py.py.
02514 02515 def denominator(self): 02516 """ Return the denominator of a Z3 rational numeral. 02517 02518 >>> is_rational_value(Q(3,5)) 02519 True 02520 >>> n = Q(3,5) 02521 >>> n.denominator() 02522 5 02523 """ 02524 return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
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 2538 of file z3py.py.
Referenced by RatNumRef.as_fraction().
02538 02539 def denominator_as_long(self): 02540 """ Return the denominator as a Python long. 02541 02542 >>> v = RealVal("1/3") 02543 >>> v 02544 1/3 02545 >>> v.denominator_as_long() 02546 3 02547 """ 02548 return self.denominator().as_long()
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 2499 of file z3py.py.
02499 02500 def numerator(self): 02501 """ Return the numerator of a Z3 rational numeral. 02502 02503 >>> is_rational_value(RealVal("3/5")) 02504 True 02505 >>> n = RealVal("3/5") 02506 >>> n.numerator() 02507 3 02508 >>> is_rational_value(Q(3,5)) 02509 True 02510 >>> Q(3,5).numerator() 02511 3 02512 """ 02513 return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
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 2525 of file z3py.py.
Referenced by RatNumRef.as_fraction().
02525 02526 def numerator_as_long(self): 02527 """ Return the numerator as a Python long. 02528 02529 >>> v = RealVal(10000000000) 02530 >>> v 02531 10000000000 02532 >>> v + 1 02533 10000000000 + 1 02534 >>> v.numerator_as_long() + 1 == 10000000001 02535 True 02536 """ 02537 return self.numerator().as_long()