Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
ArithSortRef Class Reference

Arithmetic. More...

+ Inheritance diagram for ArithSortRef:

Public Member Functions

def is_real
 
def is_int
 
def subsort
 
def cast
 
- Public Member Functions inherited from SortRef
def as_ast
 
def kind
 
def subsort
 
def cast
 
def name
 
def __eq__
 
def __ne__
 
- 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
 

Data Fields

 ctx
 

Detailed Description

Arithmetic.

Real and Integer sorts.

Definition at line 1734 of file z3py.py.

Member Function Documentation

def cast (   self,
  val 
)
Try to cast `val` as an Integer or Real.

>>> IntSort().cast(10)
10
>>> is_int(IntSort().cast(10))
True
>>> is_int(10)
False
>>> RealSort().cast(10)
10
>>> is_real(RealSort().cast(10))
True

Definition at line 1769 of file z3py.py.

1770  def cast(self, val):
1771  """Try to cast `val` as an Integer or Real.
1772 
1773  >>> IntSort().cast(10)
1774  10
1775  >>> is_int(IntSort().cast(10))
1776  True
1777  >>> is_int(10)
1778  False
1779  >>> RealSort().cast(10)
1780  10
1781  >>> is_real(RealSort().cast(10))
1782  True
1783  """
1784  if is_expr(val):
1785  if __debug__:
1786  _z3_assert(self.ctx == val.ctx, "Context mismatch")
1787  val_s = val.sort()
1788  if self.eq(val_s):
1789  return val
1790  if val_s.is_int() and self.is_real():
1791  return ToReal(val)
1792  if __debug__:
1793  _z3_assert(False, "Z3 Integer/Real expression expected" )
1794  else:
1795  if self.is_int():
1796  return IntVal(val, self.ctx)
1797  if self.is_real():
1798  return RealVal(val, self.ctx)
1799  if __debug__:
1800  _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
def is_int (   self)
Return `True` if `self` is the real sort.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> x = Real('x')
>>> x.is_int()
False

Definition at line 1751 of file z3py.py.

Referenced by ArithSortRef.cast().

1752  def is_int(self):
1753  """Return `True` if `self` is the real sort.
1754 
1755  >>> x = Int('x')
1756  >>> x.is_int()
1757  True
1758  >>> (x + 1).is_int()
1759  True
1760  >>> x = Real('x')
1761  >>> x.is_int()
1762  False
1763  """
1764  return self.kind() == Z3_INT_SORT
def is_real (   self)
Return `True` if `self` is the integer sort.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True
>>> x = Int('x')
>>> x.is_real()
False

Definition at line 1737 of file z3py.py.

Referenced by ArithSortRef.cast().

1738  def is_real(self):
1739  """Return `True` if `self` is the integer sort.
1740 
1741  >>> x = Real('x')
1742  >>> x.is_real()
1743  True
1744  >>> (x + 1).is_real()
1745  True
1746  >>> x = Int('x')
1747  >>> x.is_real()
1748  False
1749  """
1750  return self.kind() == Z3_REAL_SORT
def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

Definition at line 1765 of file z3py.py.

1766  def subsort(self, other):
1767  """Return `True` if `self` is a subsort of `other`."""
1768  return self.is_int() and is_arith_sort(other) and other.is_real()

Field Documentation

ctx

Definition at line 1785 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Tactic.solver(), and Fixedpoint.statistics().