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 params (self)
 
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 __deepcopy__ (self, memo={})
 
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 __copy__ (self)
 
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 2159 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 2197 of file z3py.py.

2197  def __add__(self, other):
2198  """Create the Z3 expression `self + other`.
2199 
2200  >>> x = Int('x')
2201  >>> y = Int('y')
2202  >>> x + y
2203  x + y
2204  >>> (x + y).sort()
2205  Int
2206  """
2207  a, b = _coerce_exprs(self, other)
2208  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
2209 

◆ __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 2296 of file z3py.py.

2296  def __div__(self, other):
2297  """Create the Z3 expression `other/self`.
2298 
2299  >>> x = Int('x')
2300  >>> y = Int('y')
2301  >>> x/y
2302  x/y
2303  >>> (x/y).sort()
2304  Int
2305  >>> (x/y).sexpr()
2306  '(div x y)'
2307  >>> x = Real('x')
2308  >>> y = Real('y')
2309  >>> x/y
2310  x/y
2311  >>> (x/y).sort()
2312  Real
2313  >>> (x/y).sexpr()
2314  '(/ x y)'
2315  """
2316  a, b = _coerce_exprs(self, other)
2317  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2318 
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 2430 of file z3py.py.

2430  def __ge__(self, other):
2431  """Create the Z3 expression `other >= self`.
2432 
2433  >>> x, y = Ints('x y')
2434  >>> x >= y
2435  x >= y
2436  >>> y = Real('y')
2437  >>> x >= y
2438  ToReal(x) >= y
2439  """
2440  a, b = _coerce_exprs(self, other)
2441  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2442 
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 2417 of file z3py.py.

2417  def __gt__(self, other):
2418  """Create the Z3 expression `other > self`.
2419 
2420  >>> x, y = Ints('x y')
2421  >>> x > y
2422  x > y
2423  >>> y = Real('y')
2424  >>> x > y
2425  ToReal(x) > y
2426  """
2427  a, b = _coerce_exprs(self, other)
2428  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2429 
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 2391 of file z3py.py.

2391  def __le__(self, other):
2392  """Create the Z3 expression `other <= self`.
2393 
2394  >>> x, y = Ints('x y')
2395  >>> x <= y
2396  x <= y
2397  >>> y = Real('y')
2398  >>> x <= y
2399  ToReal(x) <= y
2400  """
2401  a, b = _coerce_exprs(self, other)
2402  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2403 
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 2404 of file z3py.py.

2404  def __lt__(self, other):
2405  """Create the Z3 expression `other < self`.
2406 
2407  >>> x, y = Ints('x y')
2408  >>> x < y
2409  x < y
2410  >>> y = Real('y')
2411  >>> x < y
2412  ToReal(x) < y
2413  """
2414  a, b = _coerce_exprs(self, other)
2415  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2416 
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 2344 of file z3py.py.

2344  def __mod__(self, other):
2345  """Create the Z3 expression `other%self`.
2346 
2347  >>> x = Int('x')
2348  >>> y = Int('y')
2349  >>> x % y
2350  x%y
2351  >>> simplify(IntVal(10) % IntVal(3))
2352  1
2353  """
2354  a, b = _coerce_exprs(self, other)
2355  if __debug__:
2356  _z3_assert(a.is_int(), "Z3 integer expression expected")
2357  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2358 
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 2220 of file z3py.py.

2220  def __mul__(self, other):
2221  """Create the Z3 expression `self * other`.
2222 
2223  >>> x = Real('x')
2224  >>> y = Real('y')
2225  >>> x * y
2226  x*y
2227  >>> (x * y).sort()
2228  Real
2229  """
2230  if isinstance(other, BoolRef):
2231  return If(other, self, 0)
2232  a, b = _coerce_exprs(self, other)
2233  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2234 
def If(a, b, c, ctx=None)
Definition: z3py.py:1227

◆ __neg__()

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

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

Definition at line 2371 of file z3py.py.

2371  def __neg__(self):
2372  """Return an expression representing `-self`.
2373 
2374  >>> x = Int('x')
2375  >>> -x
2376  -x
2377  >>> simplify(-(-x))
2378  x
2379  """
2380  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2381 
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 2382 of file z3py.py.

2382  def __pos__(self):
2383  """Return `self`.
2384 
2385  >>> x = Int('x')
2386  >>> +x
2387  x
2388  """
2389  return self
2390 

◆ __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 2268 of file z3py.py.

2268  def __pow__(self, other):
2269  """Create the Z3 expression `self**other` (** is the power operator).
2270 
2271  >>> x = Real('x')
2272  >>> x**3
2273  x**3
2274  >>> (x**3).sort()
2275  Real
2276  >>> simplify(IntVal(2)**8)
2277  256
2278  """
2279  a, b = _coerce_exprs(self, other)
2280  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2281 
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 2210 of file z3py.py.

2210  def __radd__(self, other):
2211  """Create the Z3 expression `other + self`.
2212 
2213  >>> x = Int('x')
2214  >>> 10 + x
2215  10 + x
2216  """
2217  a, b = _coerce_exprs(self, other)
2218  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
2219 

◆ __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 2323 of file z3py.py.

2323  def __rdiv__(self, other):
2324  """Create the Z3 expression `other/self`.
2325 
2326  >>> x = Int('x')
2327  >>> 10/x
2328  10/x
2329  >>> (10/x).sexpr()
2330  '(div 10 x)'
2331  >>> x = Real('x')
2332  >>> 10/x
2333  10/x
2334  >>> (10/x).sexpr()
2335  '(/ 10.0 x)'
2336  """
2337  a, b = _coerce_exprs(self, other)
2338  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2339 
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 2359 of file z3py.py.

2359  def __rmod__(self, other):
2360  """Create the Z3 expression `other%self`.
2361 
2362  >>> x = Int('x')
2363  >>> 10 % x
2364  10%x
2365  """
2366  a, b = _coerce_exprs(self, other)
2367  if __debug__:
2368  _z3_assert(a.is_int(), "Z3 integer expression expected")
2369  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2370 
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 2235 of file z3py.py.

2235  def __rmul__(self, other):
2236  """Create the Z3 expression `other * self`.
2237 
2238  >>> x = Real('x')
2239  >>> 10 * x
2240  10*x
2241  """
2242  a, b = _coerce_exprs(self, other)
2243  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2244 

◆ __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 2282 of file z3py.py.

2282  def __rpow__(self, other):
2283  """Create the Z3 expression `other**self` (** is the power operator).
2284 
2285  >>> x = Real('x')
2286  >>> 2**x
2287  2**x
2288  >>> (2**x).sort()
2289  Real
2290  >>> simplify(2**IntVal(8))
2291  256
2292  """
2293  a, b = _coerce_exprs(self, other)
2294  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2295 
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 2258 of file z3py.py.

2258  def __rsub__(self, other):
2259  """Create the Z3 expression `other - self`.
2260 
2261  >>> x = Int('x')
2262  >>> 10 - x
2263  10 - x
2264  """
2265  a, b = _coerce_exprs(self, other)
2266  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2267 

◆ __rtruediv__()

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

Definition at line 2340 of file z3py.py.

2340  def __rtruediv__(self, other):
2341  """Create the Z3 expression `other/self`."""
2342  return self.__rdiv__(other)
2343 

◆ __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 2245 of file z3py.py.

2245  def __sub__(self, other):
2246  """Create the Z3 expression `self - other`.
2247 
2248  >>> x = Int('x')
2249  >>> y = Int('y')
2250  >>> x - y
2251  x - y
2252  >>> (x - y).sort()
2253  Int
2254  """
2255  a, b = _coerce_exprs(self, other)
2256  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2257 

◆ __truediv__()

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

Definition at line 2319 of file z3py.py.

2319  def __truediv__(self, other):
2320  """Create the Z3 expression `other/self`."""
2321  return self.__div__(other)
2322 

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

2172  def is_int(self):
2173  """Return `True` if `self` is an integer expression.
2174 
2175  >>> x = Int('x')
2176  >>> x.is_int()
2177  True
2178  >>> (x + 1).is_int()
2179  True
2180  >>> y = Real('y')
2181  >>> (x + y).is_int()
2182  False
2183  """
2184  return self.sort().is_int()
2185 
def is_int(a)
Definition: z3py.py:2463

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

2186  def is_real(self):
2187  """Return `True` if `self` is an real expression.
2188 
2189  >>> x = Real('x')
2190  >>> x.is_real()
2191  True
2192  >>> (x + 1).is_real()
2193  True
2194  """
2195  return self.sort().is_real()
2196 
def is_real(a)
Definition: z3py.py:2481

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

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

2162  def sort(self):
2163  """Return the sort (type) of the arithmetical expression `self`.
2164 
2165  >>> Int('x').sort()
2166  Int
2167  >>> (Real('x') + 1).sort()
2168  Real
2169  """
2170  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2171 
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.