Z3
Public Member Functions | Data Fields
ArithSortRef Class Reference

Arithmetic. More...

+ Inheritance diagram for ArithSortRef:

Public Member Functions

def is_real (self)
 
def is_int (self)
 
def subsort (self, other)
 
def cast (self, val)
 
- Public Member Functions inherited from SortRef
def as_ast (self)
 
def get_id (self)
 
def kind (self)
 
def subsort (self, other)
 
def cast (self, val)
 
def name (self)
 
def __eq__ (self, other)
 
def __ne__ (self, other)
 
- 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)
 

Data Fields

 ctx
 
- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Arithmetic.

Real and Integer sorts.

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

1881  def cast(self, val):
1882  """Try to cast `val` as an Integer or Real.
1883 
1884  >>> IntSort().cast(10)
1885  10
1886  >>> is_int(IntSort().cast(10))
1887  True
1888  >>> is_int(10)
1889  False
1890  >>> RealSort().cast(10)
1891  10
1892  >>> is_real(RealSort().cast(10))
1893  True
1894  """
1895  if is_expr(val):
1896  if __debug__:
1897  _z3_assert(self.ctx == val.ctx, "Context mismatch")
1898  val_s = val.sort()
1899  if self.eq(val_s):
1900  return val
1901  if val_s.is_int() and self.is_real():
1902  return ToReal(val)
1903  if __debug__:
1904  _z3_assert(False, "Z3 Integer/Real expression expected" )
1905  else:
1906  if self.is_int():
1907  return IntVal(val, self.ctx)
1908  if self.is_real():
1909  return RealVal(val, self.ctx)
1910  if __debug__:
1911  _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
1912 
def is_int(self)
Definition: z3py.py:1863
def is_real(self)
Definition: z3py.py:1849
def eq(self, other)
Definition: z3py.py:309
def ToReal(a)
Definition: z3py.py:2828
def cast(self, val)
Definition: z3py.py:1881
def RealVal
Definition: z3py.py:2683
def is_expr(a)
Definition: z3py.py:961
def IntVal
Definition: z3py.py:2672
def is_int (   self)
Return `True` if `self` is of the sort Integer.

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

Definition at line 1863 of file z3py.py.

Referenced by ArithSortRef.cast().

1863  def is_int(self):
1864  """Return `True` if `self` is of the sort Integer.
1865 
1866  >>> x = Int('x')
1867  >>> x.is_int()
1868  True
1869  >>> (x + 1).is_int()
1870  True
1871  >>> x = Real('x')
1872  >>> x.is_int()
1873  False
1874  """
1875  return self.kind() == Z3_INT_SORT
1876 
def is_int(self)
Definition: z3py.py:1863
def kind(self)
Definition: z3py.py:459
def is_real (   self)
Return `True` if `self` is of the sort Real.

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

Definition at line 1849 of file z3py.py.

Referenced by ArithSortRef.cast().

1849  def is_real(self):
1850  """Return `True` if `self` is of the sort Real.
1851 
1852  >>> x = Real('x')
1853  >>> x.is_real()
1854  True
1855  >>> (x + 1).is_real()
1856  True
1857  >>> x = Int('x')
1858  >>> x.is_real()
1859  False
1860  """
1861  return self.kind() == Z3_REAL_SORT
1862 
def is_real(self)
Definition: z3py.py:1849
def kind(self)
Definition: z3py.py:459
def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

Definition at line 1877 of file z3py.py.

1877  def subsort(self, other):
1878  """Return `True` if `self` is a subsort of `other`."""
1879  return self.is_int() and is_arith_sort(other) and other.is_real()
1880 
def is_arith_sort(s)
Definition: z3py.py:1913
def is_int(self)
Definition: z3py.py:1863
def subsort(self, other)
Definition: z3py.py:1877

Field Documentation

ctx