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 get_id
 
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 get_id
 
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 1942 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 1980 of file z3py.py.

1980 
1981  def __add__(self, other):
1982  """Create the Z3 expression `self + other`.
1983 
1984  >>> x = Int('x')
1985  >>> y = Int('y')
1986  >>> x + y
1987  x + y
1988  >>> (x + y).sort()
1989  Int
1990  """
1991  a, b = _coerce_exprs(self, other)
1992  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
z3py.ArithRef.__add__
def __add__
Definition: z3py.py:1980
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 2077 of file z3py.py.

2077 
2078  def __div__(self, other):
2079  """Create the Z3 expression `other/self`.
2080 
2081  >>> x = Int('x')
2082  >>> y = Int('y')
2083  >>> x/y
2084  x/y
2085  >>> (x/y).sort()
2086  Int
2087  >>> (x/y).sexpr()
2088  '(div x y)'
2089  >>> x = Real('x')
2090  >>> y = Real('y')
2091  >>> x/y
2092  x/y
2093  >>> (x/y).sort()
2094  Real
2095  >>> (x/y).sexpr()
2096  '(/ x y)'
2097  """
2098  a, b = _coerce_exprs(self, other)
2099  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_mk_div
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
z3py.ArithRef.__div__
def __div__
Definition: z3py.py:2077
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 2211 of file z3py.py.

2211 
2212  def __ge__(self, other):
2213  """Create the Z3 expression `other >= self`.
2214 
2215  >>> x, y = Ints('x y')
2216  >>> x >= y
2217  x >= y
2218  >>> y = Real('y')
2219  >>> x >= y
2220  ToReal(x) >= y
2221  """
2222  a, b = _coerce_exprs(self, other)
2223  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
z3py.ArithRef.__ge__
def __ge__
Definition: z3py.py:2211
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 2198 of file z3py.py.

2198 
2199  def __gt__(self, other):
2200  """Create the Z3 expression `other > self`.
2201 
2202  >>> x, y = Ints('x y')
2203  >>> x > y
2204  x > y
2205  >>> y = Real('y')
2206  >>> x > y
2207  ToReal(x) > y
2208  """
2209  a, b = _coerce_exprs(self, other)
2210  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
z3py.ArithRef.__gt__
def __gt__
Definition: z3py.py:2198
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 2172 of file z3py.py.

2172 
2173  def __le__(self, other):
2174  """Create the Z3 expression `other <= self`.
2175 
2176  >>> x, y = Ints('x y')
2177  >>> x <= y
2178  x <= y
2179  >>> y = Real('y')
2180  >>> x <= y
2181  ToReal(x) <= y
2182  """
2183  a, b = _coerce_exprs(self, other)
2184  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
z3py.ArithRef.__le__
def __le__
Definition: z3py.py:2172
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 2185 of file z3py.py.

2185 
2186  def __lt__(self, other):
2187  """Create the Z3 expression `other < self`.
2188 
2189  >>> x, y = Ints('x y')
2190  >>> x < y
2191  x < y
2192  >>> y = Real('y')
2193  >>> x < y
2194  ToReal(x) < y
2195  """
2196  a, b = _coerce_exprs(self, other)
2197  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
z3py.ArithRef.__lt__
def __lt__
Definition: z3py.py:2185
Z3_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 2125 of file z3py.py.

2125 
2126  def __mod__(self, other):
2127  """Create the Z3 expression `other%self`.
2128 
2129  >>> x = Int('x')
2130  >>> y = Int('y')
2131  >>> x % y
2132  x%y
2133  >>> simplify(IntVal(10) % IntVal(3))
2134  1
2135  """
2136  a, b = _coerce_exprs(self, other)
2137  if __debug__:
2138  _z3_assert(a.is_int(), "Z3 integer expression expected")
2139  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.The arguments must have int type.
z3py.ArithRef.__mod__
def __mod__
Definition: z3py.py:2125
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
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 2003 of file z3py.py.

2003 
2004  def __mul__(self, other):
2005  """Create the Z3 expression `self * other`.
2006 
2007  >>> x = Real('x')
2008  >>> y = Real('y')
2009  >>> x * y
2010  x*y
2011  >>> (x * y).sort()
2012  Real
2013  """
2014  a, b = _coerce_exprs(self, other)
2015  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
z3py.ArithRef.__mul__
def __mul__
Definition: z3py.py:2003
def __neg__ (   self) 
Return an expression representing `-self`.

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

Definition at line 2152 of file z3py.py.

2152 
2153  def __neg__(self):
2154  """Return an expression representing `-self`.
2155 
2156  >>> x = Int('x')
2157  >>> -x
2158  -x
2159  >>> simplify(-(-x))
2160  x
2161  """
2162  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
z3py.AstRef.as_ast
def as_ast
Definition: z3py.py:296
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
z3py.ArithRef.__neg__
def __neg__
Definition: z3py.py:2152
def __pos__ (   self) 
Return `self`.

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

Definition at line 2163 of file z3py.py.

2163 
2164  def __pos__(self):
2165  """Return `self`.
2166 
2167  >>> x = Int('x')
2168  >>> +x
2169  x
2170  """
2171  return self
z3py.ArithRef.__pos__
def __pos__
Definition: z3py.py:2163
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 2049 of file z3py.py.

2049 
2050  def __pow__(self, other):
2051  """Create the Z3 expression `self**other` (** is the power operator).
2052 
2053  >>> x = Real('x')
2054  >>> x**3
2055  x**3
2056  >>> (x**3).sort()
2057  Real
2058  >>> simplify(IntVal(2)**8)
2059  256
2060  """
2061  a, b = _coerce_exprs(self, other)
2062  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
z3py.ArithRef.__pow__
def __pow__
Definition: z3py.py:2049
Z3_mk_power
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1^arg2.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
def __radd__ (   self,
  other 
) 
Create the Z3 expression `other + self`.

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

Definition at line 1993 of file z3py.py.

1993 
1994  def __radd__(self, other):
1995  """Create the Z3 expression `other + self`.
1996 
1997  >>> x = Int('x')
1998  >>> 10 + x
1999  10 + x
2000  """
2001  a, b = _coerce_exprs(self, other)
2002  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
z3py.ArithRef.__radd__
def __radd__
Definition: z3py.py:1993
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 2104 of file z3py.py.

2104 
2105  def __rdiv__(self, other):
2106  """Create the Z3 expression `other/self`.
2107 
2108  >>> x = Int('x')
2109  >>> 10/x
2110  10/x
2111  >>> (10/x).sexpr()
2112  '(div 10 x)'
2113  >>> x = Real('x')
2114  >>> 10/x
2115  10/x
2116  >>> (10/x).sexpr()
2117  '(/ 10.0 x)'
2118  """
2119  a, b = _coerce_exprs(self, other)
2120  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_mk_div
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
z3py.ArithRef.__rdiv__
def __rdiv__
Definition: z3py.py:2104
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
def __rmod__ (   self,
  other 
) 
Create the Z3 expression `other%self`.

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

Definition at line 2140 of file z3py.py.

2140 
2141  def __rmod__(self, other):
2142  """Create the Z3 expression `other%self`.
2143 
2144  >>> x = Int('x')
2145  >>> 10 % x
2146  10%x
2147  """
2148  a, b = _coerce_exprs(self, other)
2149  if __debug__:
2150  _z3_assert(a.is_int(), "Z3 integer expression expected")
2151  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.The arguments must have int type.
z3py.ArithRef.__rmod__
def __rmod__
Definition: z3py.py:2140
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
def __rmul__ (   self,
  other 
) 
Create the Z3 expression `other * self`.

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

Definition at line 2016 of file z3py.py.

2016 
2017  def __rmul__(self, other):
2018  """Create the Z3 expression `other * self`.
2019 
2020  >>> x = Real('x')
2021  >>> 10 * x
2022  10*x
2023  """
2024  a, b = _coerce_exprs(self, other)
2025  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
z3py.ArithRef.__rmul__
def __rmul__
Definition: z3py.py:2016
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 2063 of file z3py.py.

2063 
2064  def __rpow__(self, other):
2065  """Create the Z3 expression `other**self` (** is the power operator).
2066 
2067  >>> x = Real('x')
2068  >>> 2**x
2069  2**x
2070  >>> (2**x).sort()
2071  Real
2072  >>> simplify(2**IntVal(8))
2073  256
2074  """
2075  a, b = _coerce_exprs(self, other)
2076  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
z3py.ArithRef.__rpow__
def __rpow__
Definition: z3py.py:2063
Z3_mk_power
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1^arg2.
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
def __rsub__ (   self,
  other 
) 
Create the Z3 expression `other - self`.

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

Definition at line 2039 of file z3py.py.

2039 
2040  def __rsub__(self, other):
2041  """Create the Z3 expression `other - self`.
2042 
2043  >>> x = Int('x')
2044  >>> 10 - x
2045  10 - x
2046  """
2047  a, b = _coerce_exprs(self, other)
2048  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
z3py.ArithRef.__rsub__
def __rsub__
Definition: z3py.py:2039
def __rtruediv__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

Definition at line 2121 of file z3py.py.

2121 
2122  def __rtruediv__(self, other):
2123  """Create the Z3 expression `other/self`."""
2124  return self.__rdiv__(other)
z3py.ArithRef.__rtruediv__
def __rtruediv__
Definition: z3py.py:2121
z3py.ArithRef.__rdiv__
def __rdiv__
Definition: z3py.py:2104
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 2026 of file z3py.py.

2026 
2027  def __sub__(self, other):
2028  """Create the Z3 expression `self - other`.
2029 
2030  >>> x = Int('x')
2031  >>> y = Int('y')
2032  >>> x - y
2033  x - y
2034  >>> (x - y).sort()
2035  Int
2036  """
2037  a, b = _coerce_exprs(self, other)
2038  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
z3py.ArithRef.__sub__
def __sub__
Definition: z3py.py:2026
def __truediv__ (   self,
  other 
) 
Create the Z3 expression `other/self`.

Definition at line 2100 of file z3py.py.

2100 
2101  def __truediv__(self, other):
2102  """Create the Z3 expression `other/self`."""
2103  return self.__div__(other)
z3py.ArithRef.__div__
def __div__
Definition: z3py.py:2077
z3py.ArithRef.__truediv__
def __truediv__
Definition: z3py.py:2100
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 1955 of file z3py.py.

1955 
1956  def is_int(self):
1957  """Return `True` if `self` is an integer expression.
1958 
1959  >>> x = Int('x')
1960  >>> x.is_int()
1961  True
1962  >>> (x + 1).is_int()
1963  True
1964  >>> y = Real('y')
1965  >>> (x + y).is_int()
1966  False
1967  """
1968  return self.sort().is_int()
z3py.ExprRef.sort
def sort
Definition: z3py.py:752
z3py.ArithRef.is_int
def is_int
Definition: z3py.py:1955
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 1969 of file z3py.py.

1969 
1970  def is_real(self):
1971  """Return `True` if `self` is an real expression.
1972 
1973  >>> x = Real('x')
1974  >>> x.is_real()
1975  True
1976  >>> (x + 1).is_real()
1977  True
1978  """
1979  return self.sort().is_real()
z3py.ExprRef.sort
def sort
Definition: z3py.py:752
z3py.ArithRef.is_real
def is_real
Definition: z3py.py:1969
def sort (   self) 
Return the sort (type) of the arithmetical expression `self`.

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

Definition at line 1945 of file z3py.py.

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

1945 
1946  def sort(self):
1947  """Return the sort (type) of the arithmetical expression `self`.
1948 
1949  >>> Int('x').sort()
1950  Int
1951  >>> (Real('x') + 1).sort()
1952  Real
1953  """
1954  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
z3py.ArithSortRef
Arithmetic.
Definition: z3py.py:1856
z3py.ArithRef.sort
def sort
Definition: z3py.py:1945
z3py.AstRef.as_ast
def as_ast
Definition: z3py.py:296
z3py.AstRef.ctx_ref
def ctx_ref
Definition: z3py.py:304
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Generated on Fri Apr 12 2019 11:38:54 for Z3 by   doxygen 1.8.5