Z3
Public Member Functions
RatNumRef Class Reference
+ Inheritance diagram for RatNumRef:

Public Member Functions

def numerator (self)
 
def denominator (self)
 
def numerator_as_long (self)
 
def denominator_as_long (self)
 
def as_decimal (self, prec)
 
def as_string (self)
 
def as_fraction (self)
 
- Public Member Functions inherited from ArithRef
def sort (self)
 
def is_int (self)
 
def is_real (self)
 
def __add__ (self, other)
 
def __radd__ (self, other)
 
def __mul__ (self, other)
 
def __rmul__ (self, other)
 
def __sub__ (self, other)
 
def __rsub__ (self, other)
 
def __pow__ (self, other)
 
def __rpow__ (self, other)
 
def __div__ (self, other)
 
def __truediv__ (self, other)
 
def __rdiv__ (self, other)
 
def __rtruediv__ (self, other)
 
def __mod__ (self, other)
 
def __rmod__ (self, other)
 
def __neg__ (self)
 
def __pos__ (self)
 
def __le__ (self, other)
 
def __lt__ (self, other)
 
def __gt__ (self, other)
 
def __ge__ (self, other)
 
- Public Member Functions inherited from ExprRef
def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
def sort_kind (self)
 
def __eq__ (self, other)
 
def __ne__ (self, other)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Rational values.

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

2560  def as_decimal(self, prec):
2561  """ Return a Z3 rational value as a string in decimal notation using at most `prec` decimal places.
2562 
2563  >>> v = RealVal("1/5")
2564  >>> v.as_decimal(3)
2565  '0.2'
2566  >>> v = RealVal("1/3")
2567  >>> v.as_decimal(3)
2568  '0.333?'
2569  """
2570  return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec)
2571 
def as_ast(self)
Definition: z3py.py:296
def as_decimal(self, prec)
Definition: z3py.py:2560
Z3_string Z3_API Z3_get_numeral_decimal_string(__in Z3_context c, __in Z3_ast a, __in unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
def ctx_ref(self)
Definition: z3py.py:305
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 2581 of file z3py.py.

2581  def as_fraction(self):
2582  """Return a Z3 rational as a Python Fraction object.
2583 
2584  >>> v = RealVal("1/5")
2585  >>> v.as_fraction()
2586  Fraction(1, 5)
2587  """
2588  return Fraction(self.numerator_as_long(), self.denominator_as_long())
2589 
def as_fraction(self)
Definition: z3py.py:2581
def denominator_as_long(self)
Definition: z3py.py:2549
def numerator_as_long(self)
Definition: z3py.py:2536
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 2572 of file z3py.py.

Referenced by BitVecNumRef.as_long().

2572  def as_string(self):
2573  """Return a Z3 rational numeral as a Python string.
2574 
2575  >>> v = Q(3,6)
2576  >>> v.as_string()
2577  '1/2'
2578  """
2579  return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2580 
def as_ast(self)
Definition: z3py.py:296
def as_string(self)
Definition: z3py.py:2572
Z3_string Z3_API Z3_get_numeral_string(__in Z3_context c, __in Z3_ast a)
Return numeral value, as a string of a numeric constant term.
def ctx_ref(self)
Definition: z3py.py:305
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 2525 of file z3py.py.

2525  def denominator(self):
2526  """ Return the denominator of a Z3 rational numeral.
2527 
2528  >>> is_rational_value(Q(3,5))
2529  True
2530  >>> n = Q(3,5)
2531  >>> n.denominator()
2532  5
2533  """
2534  return IntNumRef(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
2535 
def as_ast(self)
Definition: z3py.py:296
Z3_ast Z3_API Z3_get_denominator(__in Z3_context c, __in Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
def denominator(self)
Definition: z3py.py:2525
def ctx_ref(self)
Definition: z3py.py:305
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 2549 of file z3py.py.

Referenced by RatNumRef.as_fraction().

2550  """ Return the denominator as a Python long.
2551 
2552  >>> v = RealVal("1/3")
2553  >>> v
2554  1/3
2555  >>> v.denominator_as_long()
2556  3
2557  """
2558  return self.denominator().as_long()
2559 
def denominator_as_long(self)
Definition: z3py.py:2549
def denominator(self)
Definition: z3py.py:2525
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 2510 of file z3py.py.

2510  def numerator(self):
2511  """ Return the numerator of a Z3 rational numeral.
2512 
2513  >>> is_rational_value(RealVal("3/5"))
2514  True
2515  >>> n = RealVal("3/5")
2516  >>> n.numerator()
2517  3
2518  >>> is_rational_value(Q(3,5))
2519  True
2520  >>> Q(3,5).numerator()
2521  3
2522  """
2523  return IntNumRef(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
2524 
def as_ast(self)
Definition: z3py.py:296
Z3_ast Z3_API Z3_get_numerator(__in Z3_context c, __in Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
def ctx_ref(self)
Definition: z3py.py:305
def numerator(self)
Definition: z3py.py:2510
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 2536 of file z3py.py.

Referenced by RatNumRef.as_fraction().

2537  """ Return the numerator as a Python long.
2538 
2539  >>> v = RealVal(10000000000)
2540  >>> v
2541  10000000000
2542  >>> v + 1
2543  10000000000 + 1
2544  >>> v.numerator_as_long() + 1 == 10000000001
2545  True
2546  """
2547  return self.numerator().as_long()
2548 
def numerator_as_long(self)
Definition: z3py.py:2536
def numerator(self)
Definition: z3py.py:2510