Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
RatNumRef Class Reference
+ Inheritance diagram for RatNumRef:

Public Member Functions

def numerator
def denominator
def numerator_as_long
def denominator_as_long
def as_decimal
def as_string
def as_fraction

Detailed Description

Rational values.

Definition at line 2496 of file z3py.py.


Member Function Documentation

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()
        
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines