Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions
ArithRef Class Reference
+ Inheritance diagram for ArithRef:

Public Member Functions

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 sort
 
def sort_kind
 
def __eq__
 
def __ne__
 
def decl
 
def num_args
 
def arg
 
def children
 
- 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
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Integer and Real expressions.

Definition at line 1816 of file z3py.py.

Member Function Documentation

def __add__ (   self,
  other 
) 
Create the Z3 expression `self + other`.

>>> x = Int('x')
>>> y = Int('y')
>>> x + y
x + y
>>> (x + y).sort()
Int

Definition at line 1854 of file z3py.py.

1854 
1855  def __add__(self, other):
1856  """Create the Z3 expression `self + other`.
1857 
1858  >>> x = Int('x')
1859  >>> y = Int('y')
1860  >>> x + y
1861  x + y
1862  >>> (x + y).sort()
1863  Int
1864  """
1865  a, b = _coerce_exprs(self, other)
1866  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
def __div__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

>>> x = Int('x')
>>> y = Int('y')
>>> x/y
x/y
>>> (x/y).sort()
Int
>>> (x/y).sexpr()
'(div x y)'
>>> x = Real('x')
>>> y = Real('y')
>>> x/y
x/y
>>> (x/y).sort()
Real
>>> (x/y).sexpr()
'(/ x y)'

Definition at line 1951 of file z3py.py.

1951 
1952  def __div__(self, other):
1953  """Create the Z3 expression `other/self`.
1954 
1955  >>> x = Int('x')
1956  >>> y = Int('y')
1957  >>> x/y
1958  x/y
1959  >>> (x/y).sort()
1960  Int
1961  >>> (x/y).sexpr()
1962  '(div x y)'
1963  >>> x = Real('x')
1964  >>> y = Real('y')
1965  >>> x/y
1966  x/y
1967  >>> (x/y).sort()
1968  Real
1969  >>> (x/y).sexpr()
1970  '(/ x y)'
1971  """
1972  a, b = _coerce_exprs(self, other)
1973  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __ge__ (   self,
  other 
) 
Create the Z3 expression `other >= self`.

>>> x, y = Ints('x y')
>>> x >= y
x >= y
>>> y = Real('y')
>>> x >= y
ToReal(x) >= y

Definition at line 2085 of file z3py.py.

2085 
2086  def __ge__(self, other):
2087  """Create the Z3 expression `other >= self`.
2088 
2089  >>> x, y = Ints('x y')
2090  >>> x >= y
2091  x >= y
2092  >>> y = Real('y')
2093  >>> x >= y
2094  ToReal(x) >= y
2095  """
2096  a, b = _coerce_exprs(self, other)
2097  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __gt__ (   self,
  other 
) 
Create the Z3 expression `other > self`.

>>> x, y = Ints('x y')
>>> x > y
x > y
>>> y = Real('y')
>>> x > y
ToReal(x) > y

Definition at line 2072 of file z3py.py.

2072 
2073  def __gt__(self, other):
2074  """Create the Z3 expression `other > self`.
2075 
2076  >>> x, y = Ints('x y')
2077  >>> x > y
2078  x > y
2079  >>> y = Real('y')
2080  >>> x > y
2081  ToReal(x) > y
2082  """
2083  a, b = _coerce_exprs(self, other)
2084  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __le__ (   self,
  other 
) 
Create the Z3 expression `other <= self`.

>>> x, y = Ints('x y')
>>> x <= y
x <= y
>>> y = Real('y')
>>> x <= y
ToReal(x) <= y

Definition at line 2046 of file z3py.py.

2046 
2047  def __le__(self, other):
2048  """Create the Z3 expression `other <= self`.
2049 
2050  >>> x, y = Ints('x y')
2051  >>> x <= y
2052  x <= y
2053  >>> y = Real('y')
2054  >>> x <= y
2055  ToReal(x) <= y
2056  """
2057  a, b = _coerce_exprs(self, other)
2058  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __lt__ (   self,
  other 
) 
Create the Z3 expression `other < self`.

>>> x, y = Ints('x y')
>>> x < y
x < y
>>> y = Real('y')
>>> x < y
ToReal(x) < y

Definition at line 2059 of file z3py.py.

2059 
2060  def __lt__(self, other):
2061  """Create the Z3 expression `other < self`.
2062 
2063  >>> x, y = Ints('x y')
2064  >>> x < y
2065  x < y
2066  >>> y = Real('y')
2067  >>> x < y
2068  ToReal(x) < y
2069  """
2070  a, b = _coerce_exprs(self, other)
2071  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mod__ (   self,
  other 
) 
Create the Z3 expression `other%self`.

>>> x = Int('x')
>>> y = Int('y')
>>> x % y
x%y
>>> simplify(IntVal(10) % IntVal(3))
1

Definition at line 1999 of file z3py.py.

1999 
2000  def __mod__(self, other):
2001  """Create the Z3 expression `other%self`.
2002 
2003  >>> x = Int('x')
2004  >>> y = Int('y')
2005  >>> x % y
2006  x%y
2007  >>> simplify(IntVal(10) % IntVal(3))
2008  1
2009  """
2010  a, b = _coerce_exprs(self, other)
2011  if __debug__:
2012  _z3_assert(a.is_int(), "Z3 integer expression expected")
2013  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __mul__ (   self,
  other 
) 
Create the Z3 expression `self * other`.

>>> x = Real('x')
>>> y = Real('y')
>>> x * y
x*y
>>> (x * y).sort()
Real

Definition at line 1877 of file z3py.py.

1877 
1878  def __mul__(self, other):
1879  """Create the Z3 expression `self * other`.
1880 
1881  >>> x = Real('x')
1882  >>> y = Real('y')
1883  >>> x * y
1884  x*y
1885  >>> (x * y).sort()
1886  Real
1887  """
1888  a, b = _coerce_exprs(self, other)
1889  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
def __neg__ (   self) 
Return an expression representing `-self`.

>>> x = Int('x')
>>> -x
-x
>>> simplify(-(-x))
x

Definition at line 2026 of file z3py.py.

2026 
2027  def __neg__(self):
2028  """Return an expression representing `-self`.
2029 
2030  >>> x = Int('x')
2031  >>> -x
2032  -x
2033  >>> simplify(-(-x))
2034  x
2035  """
2036  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
def __pos__ (   self) 
Return `self`.

>>> x = Int('x')
>>> +x
x

Definition at line 2037 of file z3py.py.

2037 
2038  def __pos__(self):
2039  """Return `self`.
2040 
2041  >>> x = Int('x')
2042  >>> +x
2043  x
2044  """
2045  return self
def __pow__ (   self,
  other 
) 
Create the Z3 expression `self**other` (** is the power operator).

>>> x = Real('x')
>>> x**3
x**3
>>> (x**3).sort()
Real
>>> simplify(IntVal(2)**8)
256

Definition at line 1923 of file z3py.py.

1923 
1924  def __pow__(self, other):
1925  """Create the Z3 expression `self**other` (** is the power operator).
1926 
1927  >>> x = Real('x')
1928  >>> x**3
1929  x**3
1930  >>> (x**3).sort()
1931  Real
1932  >>> simplify(IntVal(2)**8)
1933  256
1934  """
1935  a, b = _coerce_exprs(self, other)
1936  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __radd__ (   self,
  other 
) 
Create the Z3 expression `other + self`.

>>> x = Int('x')
>>> 10 + x
10 + x

Definition at line 1867 of file z3py.py.

1867 
1868  def __radd__(self, other):
1869  """Create the Z3 expression `other + self`.
1870 
1871  >>> x = Int('x')
1872  >>> 10 + x
1873  10 + x
1874  """
1875  a, b = _coerce_exprs(self, other)
1876  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
def __rdiv__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

>>> x = Int('x')
>>> 10/x
10/x
>>> (10/x).sexpr()
'(div 10 x)'
>>> x = Real('x')
>>> 10/x
10/x
>>> (10/x).sexpr()
'(/ 10.0 x)'

Definition at line 1978 of file z3py.py.

1978 
1979  def __rdiv__(self, other):
1980  """Create the Z3 expression `other/self`.
1981 
1982  >>> x = Int('x')
1983  >>> 10/x
1984  10/x
1985  >>> (10/x).sexpr()
1986  '(div 10 x)'
1987  >>> x = Real('x')
1988  >>> 10/x
1989  10/x
1990  >>> (10/x).sexpr()
1991  '(/ 10.0 x)'
1992  """
1993  a, b = _coerce_exprs(self, other)
1994  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmod__ (   self,
  other 
) 
Create the Z3 expression `other%self`.

>>> x = Int('x')
>>> 10 % x
10%x

Definition at line 2014 of file z3py.py.

2014 
2015  def __rmod__(self, other):
2016  """Create the Z3 expression `other%self`.
2017 
2018  >>> x = Int('x')
2019  >>> 10 % x
2020  10%x
2021  """
2022  a, b = _coerce_exprs(self, other)
2023  if __debug__:
2024  _z3_assert(a.is_int(), "Z3 integer expression expected")
2025  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rmul__ (   self,
  other 
) 
Create the Z3 expression `other * self`.

>>> x = Real('x')
>>> 10 * x
10*x

Definition at line 1890 of file z3py.py.

1890 
1891  def __rmul__(self, other):
1892  """Create the Z3 expression `other * self`.
1893 
1894  >>> x = Real('x')
1895  >>> 10 * x
1896  10*x
1897  """
1898  a, b = _coerce_exprs(self, other)
1899  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
def __rpow__ (   self,
  other 
) 
Create the Z3 expression `other**self` (** is the power operator).

>>> x = Real('x')
>>> 2**x
2**x
>>> (2**x).sort()
Real
>>> simplify(2**IntVal(8))
256

Definition at line 1937 of file z3py.py.

1937 
1938  def __rpow__(self, other):
1939  """Create the Z3 expression `other**self` (** is the power operator).
1940 
1941  >>> x = Real('x')
1942  >>> 2**x
1943  2**x
1944  >>> (2**x).sort()
1945  Real
1946  >>> simplify(2**IntVal(8))
1947  256
1948  """
1949  a, b = _coerce_exprs(self, other)
1950  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rsub__ (   self,
  other 
) 
Create the Z3 expression `other - self`.

>>> x = Int('x')
>>> 10 - x
10 - x

Definition at line 1913 of file z3py.py.

1913 
1914  def __rsub__(self, other):
1915  """Create the Z3 expression `other - self`.
1916 
1917  >>> x = Int('x')
1918  >>> 10 - x
1919  10 - x
1920  """
1921  a, b = _coerce_exprs(self, other)
1922  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
def __rtruediv__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

Definition at line 1995 of file z3py.py.

1995 
1996  def __rtruediv__(self, other):
1997  """Create the Z3 expression `other/self`."""
1998  self.__rdiv__(other)
def __sub__ (   self,
  other 
) 
Create the Z3 expression `self - other`.

>>> x = Int('x')
>>> y = Int('y')
>>> x - y
x - y
>>> (x - y).sort()
Int

Definition at line 1900 of file z3py.py.

1900 
1901  def __sub__(self, other):
1902  """Create the Z3 expression `self - other`.
1903 
1904  >>> x = Int('x')
1905  >>> y = Int('y')
1906  >>> x - y
1907  x - y
1908  >>> (x - y).sort()
1909  Int
1910  """
1911  a, b = _coerce_exprs(self, other)
1912  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
def __truediv__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

Definition at line 1974 of file z3py.py.

1974 
1975  def __truediv__(self, other):
1976  """Create the Z3 expression `other/self`."""
1977  self.__div__(other)
def is_int (   self) 
Return `True` if `self` is an integer expression.

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

Definition at line 1829 of file z3py.py.

1829 
1830  def is_int(self):
1831  """Return `True` if `self` is an integer expression.
1832 
1833  >>> x = Int('x')
1834  >>> x.is_int()
1835  True
1836  >>> (x + 1).is_int()
1837  True
1838  >>> y = Real('y')
1839  >>> (x + y).is_int()
1840  False
1841  """
1842  return self.sort().is_int()
def is_real (   self) 
Return `True` if `self` is an real expression.

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

Definition at line 1843 of file z3py.py.

1843 
1844  def is_real(self):
1845  """Return `True` if `self` is an real expression.
1846 
1847  >>> x = Real('x')
1848  >>> x.is_real()
1849  True
1850  >>> (x + 1).is_real()
1851  True
1852  """
1853  return self.sort().is_real()
def sort (   self) 
Return the sort (type) of the arithmetical expression `self`.

>>> Int('x').sort()
Int
>>> (Real('x') + 1).sort()
Real

Definition at line 1819 of file z3py.py.

Referenced by ArithRef.__add__(), ArithRef.__div__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), and ArithRef.__sub__().

1819 
1820  def sort(self):
1821  """Return the sort (type) of the arithmetical expression `self`.
1822 
1823  >>> Int('x').sort()
1824  Int
1825  >>> (Real('x') + 1).sort()
1826  Real
1827  """
1828  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Generated on Thu Nov 22 2012 18:37:31 for Z3 by   doxygen 1.8.2