Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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
 
- Public Member Functions inherited from ArithRef
def sort
 
def is_int
 
def is_real
 
def __add__
 
def __radd__
 
def __mul__
 
def __rmul__
 
def __sub__
 
def __rsub__
 
def __pow__
 
def __rpow__
 
def __div__
 
def __truediv__
 
def __rdiv__
 
def __rtruediv__
 
def __mod__
 
def __rmod__
 
def __neg__
 
def __pos__
 
def __le__
 
def __lt__
 
def __gt__
 
def __ge__
 
- Public Member Functions inherited from ExprRef
def as_ast
 
def sort
 
def sort_kind
 
def __eq__
 
def __ne__
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def ctx_ref
 
def eq
 
def translate
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Rational values.

Definition at line 2395 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 2448 of file z3py.py.

2449  def as_decimal(self, prec):
2450  """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
2451 
2452  >>> v = RealVal("1/5")
2453  >>> v.as_decimal(3)
2454  '0.2'
2455  >>> v = RealVal("1/3")
2456  >>> v.as_decimal(3)
2457  '0.333?'
2458  """
2459  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
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 2460 of file z3py.py.

2461  def as_string(self):
2462  """Return a Z3 rational numeral as a Python string.
2463 
2464  >>> v = Q(3,6)
2465  >>> v.as_string()
2466  '1/2'
2467  """
2468  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 2413 of file z3py.py.

2414  def denominator(self):
2415  """ Return the denominator of a Z3 rational numeral.
2416 
2417  >>> is_rational_value(Q(3,5))
2418  True
2419  >>> n = Q(3,5)
2420  >>> n.denominator()
2421  5
2422  """
2423  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()
3L

Definition at line 2437 of file z3py.py.

2438  def denominator_as_long(self):
2439  """ Return the denominator as a Python long.
2440 
2441  >>> v = RealVal("1/3")
2442  >>> v
2443  1/3
2444  >>> v.denominator_as_long()
2445  3L
2446  """
2447  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 2398 of file z3py.py.

2399  def numerator(self):
2400  """ Return the numerator of a Z3 rational numeral.
2401 
2402  >>> is_rational_value(RealVal("3/5"))
2403  True
2404  >>> n = RealVal("3/5")
2405  >>> n.numerator()
2406  3
2407  >>> is_rational_value(Q(3,5))
2408  True
2409  >>> Q(3,5).numerator()
2410  3
2411  """
2412  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
10000000001L

Definition at line 2424 of file z3py.py.

2425  def numerator_as_long(self):
2426  """ Return the numerator as a Python long.
2427 
2428  >>> v = RealVal(10000000000)
2429  >>> v
2430  10000000000
2431  >>> v + 1
2432  10000000000 + 1
2433  >>> v.numerator_as_long() + 1
2434  10000000001L
2435  """
2436  return self.numerator().as_long()