Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules 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 is_int
 
def is_real
 
def is_int_value
 
def as_long
 
def as_decimal
 
def as_string
 
def as_fraction
 
- 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 get_id
 
def sort
 
def sort_kind
 
def __eq__
 
def __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 2757 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 2823 of file z3py.py.

2824  def as_decimal(self, prec):
2825  """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
2826 
2827  >>> v = RealVal("1/5")
2828  >>> v.as_decimal(3)
2829  '0.2'
2830  >>> v = RealVal("1/3")
2831  >>> v.as_decimal(3)
2832  '0.333?'
2833  """
2834  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
def as_decimal
Definition: z3py.py:2823
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
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 2844 of file z3py.py.

2845  def as_fraction(self):
2846  """Return a Z3 rational as a Python Fraction object.
2847 
2848  >>> v = RealVal("1/5")
2849  >>> v.as_fraction()
2850  Fraction(1, 5)
2851  """
2852  return Fraction(self.numerator_as_long(), self.denominator_as_long())
def numerator_as_long
Definition: z3py.py:2786
def as_fraction
Definition: z3py.py:2844
def denominator_as_long
Definition: z3py.py:2799
def as_long (   self)

Definition at line 2819 of file z3py.py.

Referenced by BitVecNumRef.as_signed_long().

2820  def as_long(self):
2821  _z3_assert(self.is_int_value(), "Expected integer fraction")
2822  return self.numerator_as_long()
def numerator_as_long
Definition: z3py.py:2786
def as_long
Definition: z3py.py:2819
def is_int_value
Definition: z3py.py:2816
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().

2836  def as_string(self):
2837  """Return a Z3 rational numeral as a Python string.
2838 
2839  >>> v = Q(3,6)
2840  >>> v.as_string()
2841  '1/2'
2842  """
2843  return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
def as_ast
Definition: z3py.py:344
def as_string
Definition: z3py.py:2835
def ctx_ref
Definition: z3py.py:352
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.

2776  def denominator(self):
2777  """ Return the denominator of a Z3 rational numeral.
2778 
2779  >>> is_rational_value(Q(3,5))
2780  True
2781  >>> n = Q(3,5)
2782  >>> n.denominator()
2783  5
2784  """
2785  return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
def denominator
Definition: z3py.py:2775
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
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().

2800  def denominator_as_long(self):
2801  """ Return the denominator as a Python long.
2802 
2803  >>> v = RealVal("1/3")
2804  >>> v
2805  1/3
2806  >>> v.denominator_as_long()
2807  3
2808  """
2809  return self.denominator().as_long()
def as_long
Definition: z3py.py:2819
def denominator
Definition: z3py.py:2775
def denominator_as_long
Definition: z3py.py:2799
def is_int (   self)

Definition at line 2810 of file z3py.py.

2811  def is_int(self):
2812  return False
def is_int
Definition: z3py.py:2810
def is_int_value (   self)

Definition at line 2816 of file z3py.py.

Referenced by RatNumRef.as_long().

2817  def is_int_value(self):
2818  return self.denominator().is_int() and self.denominator_as_long() == 1
def is_int
Definition: z3py.py:2810
def is_int_value
Definition: z3py.py:2816
def denominator
Definition: z3py.py:2775
def denominator_as_long
Definition: z3py.py:2799
def is_real (   self)

Definition at line 2813 of file z3py.py.

2814  def is_real(self):
2815  return True
def is_real
Definition: z3py.py:2813
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.

2761  def numerator(self):
2762  """ Return the numerator of a Z3 rational numeral.
2763 
2764  >>> is_rational_value(RealVal("3/5"))
2765  True
2766  >>> n = RealVal("3/5")
2767  >>> n.numerator()
2768  3
2769  >>> is_rational_value(Q(3,5))
2770  True
2771  >>> Q(3,5).numerator()
2772  3
2773  """
2774  return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
def numerator
Definition: z3py.py:2760
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
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().

2787  def numerator_as_long(self):
2788  """ Return the numerator as a Python long.
2789 
2790  >>> v = RealVal(10000000000)
2791  >>> v
2792  10000000000
2793  >>> v + 1
2794  10000000000 + 1
2795  >>> v.numerator_as_long() + 1 == 10000000001
2796  True
2797  """
2798  return self.numerator().as_long()
def numerator_as_long
Definition: z3py.py:2786
def numerator
Definition: z3py.py:2760
def as_long
Definition: z3py.py:2819