Z3
Public Member Functions
ArithRef Class Reference
+ Inheritance diagram for ArithRef:

Public Member Functions

def sort (self)
 
def is_int (self)
 
def is_real (self)
 
def __add__ (self, other)
 
def __radd__ (self, other)
 
def __mul__ (self, other)
 
def __rmul__ (self, other)
 
def __sub__ (self, other)
 
def __rsub__ (self, other)
 
def __pow__ (self, other)
 
def __rpow__ (self, other)
 
def __div__ (self, other)
 
def __truediv__ (self, other)
 
def __rdiv__ (self, other)
 
def __rtruediv__ (self, other)
 
def __mod__ (self, other)
 
def __rmod__ (self, other)
 
def __neg__ (self)
 
def __pos__ (self)
 
def __le__ (self, other)
 
def __lt__ (self, other)
 
def __gt__ (self, other)
 
def __ge__ (self, other)
 
- Public Member Functions inherited from ExprRef
def as_ast (self)
 
def get_id (self)
 
def sort (self)
 
def sort_kind (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __ne__ (self, other)
 
def decl (self)
 
def num_args (self)
 
def arg (self, idx)
 
def children (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)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Integer and Real expressions.

Definition at line 2008 of file z3py.py.

Member Function Documentation

§ __add__()

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

2046  def __add__(self, other):
2047  """Create the Z3 expression `self + other`.
2048 
2049  >>> x = Int('x')
2050  >>> y = Int('y')
2051  >>> x + y
2052  x + y
2053  >>> (x + y).sort()
2054  Int
2055  """
2056  a, b = _coerce_exprs(self, other)
2057  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
2058 

§ __div__()

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

2143  def __div__(self, other):
2144  """Create the Z3 expression `other/self`.
2145 
2146  >>> x = Int('x')
2147  >>> y = Int('y')
2148  >>> x/y
2149  x/y
2150  >>> (x/y).sort()
2151  Int
2152  >>> (x/y).sexpr()
2153  '(div x y)'
2154  >>> x = Real('x')
2155  >>> y = Real('y')
2156  >>> x/y
2157  x/y
2158  >>> (x/y).sort()
2159  Real
2160  >>> (x/y).sexpr()
2161  '(/ x y)'
2162  """
2163  a, b = _coerce_exprs(self, other)
2164  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2165 
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.

§ __ge__()

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

2277  def __ge__(self, other):
2278  """Create the Z3 expression `other >= self`.
2279 
2280  >>> x, y = Ints('x y')
2281  >>> x >= y
2282  x >= y
2283  >>> y = Real('y')
2284  >>> x >= y
2285  ToReal(x) >= y
2286  """
2287  a, b = _coerce_exprs(self, other)
2288  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2289 
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.

§ __gt__()

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

2264  def __gt__(self, other):
2265  """Create the Z3 expression `other > self`.
2266 
2267  >>> x, y = Ints('x y')
2268  >>> x > y
2269  x > y
2270  >>> y = Real('y')
2271  >>> x > y
2272  ToReal(x) > y
2273  """
2274  a, b = _coerce_exprs(self, other)
2275  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2276 
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.

§ __le__()

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

2238  def __le__(self, other):
2239  """Create the Z3 expression `other <= self`.
2240 
2241  >>> x, y = Ints('x y')
2242  >>> x <= y
2243  x <= y
2244  >>> y = Real('y')
2245  >>> x <= y
2246  ToReal(x) <= y
2247  """
2248  a, b = _coerce_exprs(self, other)
2249  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2250 
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.

§ __lt__()

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

2251  def __lt__(self, other):
2252  """Create the Z3 expression `other < self`.
2253 
2254  >>> x, y = Ints('x y')
2255  >>> x < y
2256  x < y
2257  >>> y = Real('y')
2258  >>> x < y
2259  ToReal(x) < y
2260  """
2261  a, b = _coerce_exprs(self, other)
2262  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2263 
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.

§ __mod__()

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

2191  def __mod__(self, other):
2192  """Create the Z3 expression `other%self`.
2193 
2194  >>> x = Int('x')
2195  >>> y = Int('y')
2196  >>> x % y
2197  x%y
2198  >>> simplify(IntVal(10) % IntVal(3))
2199  1
2200  """
2201  a, b = _coerce_exprs(self, other)
2202  if __debug__:
2203  _z3_assert(a.is_int(), "Z3 integer expression expected")
2204  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2205 
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.

§ __mul__()

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

2069  def __mul__(self, other):
2070  """Create the Z3 expression `self * other`.
2071 
2072  >>> x = Real('x')
2073  >>> y = Real('y')
2074  >>> x * y
2075  x*y
2076  >>> (x * y).sort()
2077  Real
2078  """
2079  a, b = _coerce_exprs(self, other)
2080  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2081 

§ __neg__()

def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 2218 of file z3py.py.

2218  def __neg__(self):
2219  """Return an expression representing `-self`.
2220 
2221  >>> x = Int('x')
2222  >>> -x
2223  -x
2224  >>> simplify(-(-x))
2225  x
2226  """
2227  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2228 
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.

§ __pos__()

def __pos__ (   self)
Return `self`.

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

Definition at line 2229 of file z3py.py.

2229  def __pos__(self):
2230  """Return `self`.
2231 
2232  >>> x = Int('x')
2233  >>> +x
2234  x
2235  """
2236  return self
2237 

§ __pow__()

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

2115  def __pow__(self, other):
2116  """Create the Z3 expression `self**other` (** is the power operator).
2117 
2118  >>> x = Real('x')
2119  >>> x**3
2120  x**3
2121  >>> (x**3).sort()
2122  Real
2123  >>> simplify(IntVal(2)**8)
2124  256
2125  """
2126  a, b = _coerce_exprs(self, other)
2127  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2128 
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.

§ __radd__()

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

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

Definition at line 2059 of file z3py.py.

2059  def __radd__(self, other):
2060  """Create the Z3 expression `other + self`.
2061 
2062  >>> x = Int('x')
2063  >>> 10 + x
2064  10 + x
2065  """
2066  a, b = _coerce_exprs(self, other)
2067  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
2068 

§ __rdiv__()

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

2170  def __rdiv__(self, other):
2171  """Create the Z3 expression `other/self`.
2172 
2173  >>> x = Int('x')
2174  >>> 10/x
2175  10/x
2176  >>> (10/x).sexpr()
2177  '(div 10 x)'
2178  >>> x = Real('x')
2179  >>> 10/x
2180  10/x
2181  >>> (10/x).sexpr()
2182  '(/ 10.0 x)'
2183  """
2184  a, b = _coerce_exprs(self, other)
2185  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2186 
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.

§ __rmod__()

def __rmod__ (   self,
  other 
)
Create the Z3 expression `other%self`.

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

Definition at line 2206 of file z3py.py.

2206  def __rmod__(self, other):
2207  """Create the Z3 expression `other%self`.
2208 
2209  >>> x = Int('x')
2210  >>> 10 % x
2211  10%x
2212  """
2213  a, b = _coerce_exprs(self, other)
2214  if __debug__:
2215  _z3_assert(a.is_int(), "Z3 integer expression expected")
2216  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2217 
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.

§ __rmul__()

def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 2082 of file z3py.py.

2082  def __rmul__(self, other):
2083  """Create the Z3 expression `other * self`.
2084 
2085  >>> x = Real('x')
2086  >>> 10 * x
2087  10*x
2088  """
2089  a, b = _coerce_exprs(self, other)
2090  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2091 

§ __rpow__()

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

2129  def __rpow__(self, other):
2130  """Create the Z3 expression `other**self` (** is the power operator).
2131 
2132  >>> x = Real('x')
2133  >>> 2**x
2134  2**x
2135  >>> (2**x).sort()
2136  Real
2137  >>> simplify(2**IntVal(8))
2138  256
2139  """
2140  a, b = _coerce_exprs(self, other)
2141  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2142 
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.

§ __rsub__()

def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 2105 of file z3py.py.

2105  def __rsub__(self, other):
2106  """Create the Z3 expression `other - self`.
2107 
2108  >>> x = Int('x')
2109  >>> 10 - x
2110  10 - x
2111  """
2112  a, b = _coerce_exprs(self, other)
2113  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2114 

§ __rtruediv__()

def __rtruediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2187 of file z3py.py.

2187  def __rtruediv__(self, other):
2188  """Create the Z3 expression `other/self`."""
2189  return self.__rdiv__(other)
2190 

§ __sub__()

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

2092  def __sub__(self, other):
2093  """Create the Z3 expression `self - other`.
2094 
2095  >>> x = Int('x')
2096  >>> y = Int('y')
2097  >>> x - y
2098  x - y
2099  >>> (x - y).sort()
2100  Int
2101  """
2102  a, b = _coerce_exprs(self, other)
2103  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2104 

§ __truediv__()

def __truediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2166 of file z3py.py.

2166  def __truediv__(self, other):
2167  """Create the Z3 expression `other/self`."""
2168  return self.__div__(other)
2169 

§ is_int()

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

2021  def is_int(self):
2022  """Return `True` if `self` is an integer expression.
2023 
2024  >>> x = Int('x')
2025  >>> x.is_int()
2026  True
2027  >>> (x + 1).is_int()
2028  True
2029  >>> y = Real('y')
2030  >>> (x + y).is_int()
2031  False
2032  """
2033  return self.sort().is_int()
2034 
def is_int(a)
Definition: z3py.py:2310

§ is_real()

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

2035  def is_real(self):
2036  """Return `True` if `self` is an real expression.
2037 
2038  >>> x = Real('x')
2039  >>> x.is_real()
2040  True
2041  >>> (x + 1).is_real()
2042  True
2043  """
2044  return self.sort().is_real()
2045 
def is_real(a)
Definition: z3py.py:2328

§ sort()

def sort (   self)
Return the sort (type) of the arithmetical expression `self`.

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

Definition at line 2011 of file z3py.py.

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

2011  def sort(self):
2012  """Return the sort (type) of the arithmetical expression `self`.
2013 
2014  >>> Int('x').sort()
2015  Int
2016  >>> (Real('x') + 1).sort()
2017  Real
2018  """
2019  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2020