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)
 
def __hash__ (self)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (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 1922 of file z3py.py.

Member Function Documentation

§ cast()

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 1957 of file z3py.py.

1957  def cast(self, val):
1958  """Try to cast `val` as an Integer or Real.
1959 
1960  >>> IntSort().cast(10)
1961  10
1962  >>> is_int(IntSort().cast(10))
1963  True
1964  >>> is_int(10)
1965  False
1966  >>> RealSort().cast(10)
1967  10
1968  >>> is_real(RealSort().cast(10))
1969  True
1970  """
1971  if is_expr(val):
1972  if __debug__:
1973  _z3_assert(self.ctx == val.ctx, "Context mismatch")
1974  val_s = val.sort()
1975  if self.eq(val_s):
1976  return val
1977  if val_s.is_int() and self.is_real():
1978  return ToReal(val)
1979  if val_s.is_bool() and self.is_int():
1980  return If(val, 1, 0)
1981  if val_s.is_bool() and self.is_real():
1982  return ToReal(If(val, 1, 0))
1983  if __debug__:
1984  _z3_assert(False, "Z3 Integer/Real expression expected" )
1985  else:
1986  if self.is_int():
1987  return IntVal(val, self.ctx)
1988  if self.is_real():
1989  return RealVal(val, self.ctx)
1990  if __debug__:
1991  _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
1992 
def IntVal(val, ctx=None)
Definition: z3py.py:2752
def If(a, b, c, ctx=None)
Definition: z3py.py:1140
def RealVal(val, ctx=None)
Definition: z3py.py:2763
def ToReal(a)
Definition: z3py.py:2908
def is_expr(a)
Definition: z3py.py:1007

§ is_int()

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 1939 of file z3py.py.

Referenced by ArithSortRef.cast().

1939  def is_int(self):
1940  """Return `True` if `self` is of the sort Integer.
1941 
1942  >>> x = Int('x')
1943  >>> x.is_int()
1944  True
1945  >>> (x + 1).is_int()
1946  True
1947  >>> x = Real('x')
1948  >>> x.is_int()
1949  False
1950  """
1951  return self.kind() == Z3_INT_SORT
1952 
def is_int(a)
Definition: z3py.py:2310

§ is_real()

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 1925 of file z3py.py.

Referenced by ArithSortRef.cast().

1925  def is_real(self):
1926  """Return `True` if `self` is of the sort Real.
1927 
1928  >>> x = Real('x')
1929  >>> x.is_real()
1930  True
1931  >>> (x + 1).is_real()
1932  True
1933  >>> x = Int('x')
1934  >>> x.is_real()
1935  False
1936  """
1937  return self.kind() == Z3_REAL_SORT
1938 
def is_real(a)
Definition: z3py.py:2328

§ subsort()

def subsort (   self,
  other 
)
Return `True` if `self` is a subsort of `other`.

Definition at line 1953 of file z3py.py.

1953  def subsort(self, other):
1954  """Return `True` if `self` is a subsort of `other`."""
1955  return self.is_int() and is_arith_sort(other) and other.is_real()
1956 
def is_arith_sort(s)
Definition: z3py.py:1993

Field Documentation

§ ctx

ctx