Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules 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 __hash__
 
def __ne__
 
def params
 
def decl
 
def num_args
 
def arg
 
def children
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 2176 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 2214 of file z3py.py.

2215  def __add__(self, other):
2216  """Create the Z3 expression `self + other`.
2217 
2218  >>> x = Int('x')
2219  >>> y = Int('y')
2220  >>> x + y
2221  x + y
2222  >>> (x + y).sort()
2223  Int
2224  """
2225  a, b = _coerce_exprs(self, other)
2226  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
def __add__
Definition: z3py.py:2214
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 2313 of file z3py.py.

2314  def __div__(self, other):
2315  """Create the Z3 expression `other/self`.
2316 
2317  >>> x = Int('x')
2318  >>> y = Int('y')
2319  >>> x/y
2320  x/y
2321  >>> (x/y).sort()
2322  Int
2323  >>> (x/y).sexpr()
2324  '(div x y)'
2325  >>> x = Real('x')
2326  >>> y = Real('y')
2327  >>> x/y
2328  x/y
2329  >>> (x/y).sort()
2330  Real
2331  >>> (x/y).sexpr()
2332  '(/ x y)'
2333  """
2334  a, b = _coerce_exprs(self, other)
2335  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
def __div__
Definition: z3py.py:2313
def ctx_ref
Definition: z3py.py:352
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 2447 of file z3py.py.

2448  def __ge__(self, other):
2449  """Create the Z3 expression `other >= self`.
2450 
2451  >>> x, y = Ints('x y')
2452  >>> x >= y
2453  x >= y
2454  >>> y = Real('y')
2455  >>> x >= y
2456  ToReal(x) >= y
2457  """
2458  a, b = _coerce_exprs(self, other)
2459  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __ge__
Definition: z3py.py:2447
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
def ctx_ref
Definition: z3py.py:352
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 2434 of file z3py.py.

2435  def __gt__(self, other):
2436  """Create the Z3 expression `other > self`.
2437 
2438  >>> x, y = Ints('x y')
2439  >>> x > y
2440  x > y
2441  >>> y = Real('y')
2442  >>> x > y
2443  ToReal(x) > y
2444  """
2445  a, b = _coerce_exprs(self, other)
2446  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
def ctx_ref
Definition: z3py.py:352
def __gt__
Definition: z3py.py:2434
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 2408 of file z3py.py.

2409  def __le__(self, other):
2410  """Create the Z3 expression `other <= self`.
2411 
2412  >>> x, y = Ints('x y')
2413  >>> x <= y
2414  x <= y
2415  >>> y = Real('y')
2416  >>> x <= y
2417  ToReal(x) <= y
2418  """
2419  a, b = _coerce_exprs(self, other)
2420  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
def __le__
Definition: z3py.py:2408
def ctx_ref
Definition: z3py.py:352
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 2421 of file z3py.py.

2422  def __lt__(self, other):
2423  """Create the Z3 expression `other < self`.
2424 
2425  >>> x, y = Ints('x y')
2426  >>> x < y
2427  x < y
2428  >>> y = Real('y')
2429  >>> x < y
2430  ToReal(x) < y
2431  """
2432  a, b = _coerce_exprs(self, other)
2433  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __lt__
Definition: z3py.py:2421
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
def ctx_ref
Definition: z3py.py:352
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 2361 of file z3py.py.

2362  def __mod__(self, other):
2363  """Create the Z3 expression `other%self`.
2364 
2365  >>> x = Int('x')
2366  >>> y = Int('y')
2367  >>> x % y
2368  x%y
2369  >>> simplify(IntVal(10) % IntVal(3))
2370  1
2371  """
2372  a, b = _coerce_exprs(self, other)
2373  if z3_debug():
2374  _z3_assert(a.is_int(), "Z3 integer expression expected")
2375  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
def __mod__
Definition: z3py.py:2361
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
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 2237 of file z3py.py.

2238  def __mul__(self, other):
2239  """Create the Z3 expression `self * other`.
2240 
2241  >>> x = Real('x')
2242  >>> y = Real('y')
2243  >>> x * y
2244  x*y
2245  >>> (x * y).sort()
2246  Real
2247  """
2248  if isinstance(other, BoolRef):
2249  return If(other, self, 0)
2250  a, b = _coerce_exprs(self, other)
2251  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
def If
Definition: z3py.py:1238
def __mul__
Definition: z3py.py:2237
def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 2388 of file z3py.py.

2389  def __neg__(self):
2390  """Return an expression representing `-self`.
2391 
2392  >>> x = Int('x')
2393  >>> -x
2394  -x
2395  >>> simplify(-(-x))
2396  x
2397  """
2398  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def __neg__
Definition: z3py.py:2388
def __pos__ (   self)
Return `self`.

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

Definition at line 2399 of file z3py.py.

2400  def __pos__(self):
2401  """Return `self`.
2402 
2403  >>> x = Int('x')
2404  >>> +x
2405  x
2406  """
2407  return self
def __pos__
Definition: z3py.py:2399
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 2285 of file z3py.py.

2286  def __pow__(self, other):
2287  """Create the Z3 expression `self**other` (** is the power operator).
2288 
2289  >>> x = Real('x')
2290  >>> x**3
2291  x**3
2292  >>> (x**3).sort()
2293  Real
2294  >>> simplify(IntVal(2)**8)
2295  256
2296  """
2297  a, b = _coerce_exprs(self, other)
2298  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
def __pow__
Definition: z3py.py:2285
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
def ctx_ref
Definition: z3py.py:352
def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 2227 of file z3py.py.

2228  def __radd__(self, other):
2229  """Create the Z3 expression `other + self`.
2230 
2231  >>> x = Int('x')
2232  >>> 10 + x
2233  10 + x
2234  """
2235  a, b = _coerce_exprs(self, other)
2236  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
def __radd__
Definition: z3py.py:2227
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 2340 of file z3py.py.

2341  def __rdiv__(self, other):
2342  """Create the Z3 expression `other/self`.
2343 
2344  >>> x = Int('x')
2345  >>> 10/x
2346  10/x
2347  >>> (10/x).sexpr()
2348  '(div 10 x)'
2349  >>> x = Real('x')
2350  >>> 10/x
2351  10/x
2352  >>> (10/x).sexpr()
2353  '(/ 10.0 x)'
2354  """
2355  a, b = _coerce_exprs(self, other)
2356  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
def __rdiv__
Definition: z3py.py:2340
def ctx_ref
Definition: z3py.py:352
def __rmod__ (   self,
  other 
)
Create the Z3 expression `other%self`.

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

Definition at line 2376 of file z3py.py.

2377  def __rmod__(self, other):
2378  """Create the Z3 expression `other%self`.
2379 
2380  >>> x = Int('x')
2381  >>> 10 % x
2382  10%x
2383  """
2384  a, b = _coerce_exprs(self, other)
2385  if z3_debug():
2386  _z3_assert(a.is_int(), "Z3 integer expression expected")
2387  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
def __rmod__
Definition: z3py.py:2376
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 2252 of file z3py.py.

2253  def __rmul__(self, other):
2254  """Create the Z3 expression `other * self`.
2255 
2256  >>> x = Real('x')
2257  >>> 10 * x
2258  10*x
2259  """
2260  a, b = _coerce_exprs(self, other)
2261  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
def __rmul__
Definition: z3py.py:2252
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 2299 of file z3py.py.

2300  def __rpow__(self, other):
2301  """Create the Z3 expression `other**self` (** is the power operator).
2302 
2303  >>> x = Real('x')
2304  >>> 2**x
2305  2**x
2306  >>> (2**x).sort()
2307  Real
2308  >>> simplify(2**IntVal(8))
2309  256
2310  """
2311  a, b = _coerce_exprs(self, other)
2312  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
def __rpow__
Definition: z3py.py:2299
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
def ctx_ref
Definition: z3py.py:352
def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 2275 of file z3py.py.

2276  def __rsub__(self, other):
2277  """Create the Z3 expression `other - self`.
2278 
2279  >>> x = Int('x')
2280  >>> 10 - x
2281  10 - x
2282  """
2283  a, b = _coerce_exprs(self, other)
2284  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
def __rsub__
Definition: z3py.py:2275
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2357 of file z3py.py.

2358  def __rtruediv__(self, other):
2359  """Create the Z3 expression `other/self`."""
2360  return self.__rdiv__(other)
def __rtruediv__
Definition: z3py.py:2357
def __rdiv__
Definition: z3py.py:2340
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 2262 of file z3py.py.

2263  def __sub__(self, other):
2264  """Create the Z3 expression `self - other`.
2265 
2266  >>> x = Int('x')
2267  >>> y = Int('y')
2268  >>> x - y
2269  x - y
2270  >>> (x - y).sort()
2271  Int
2272  """
2273  a, b = _coerce_exprs(self, other)
2274  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
def __sub__
Definition: z3py.py:2262
def __truediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2336 of file z3py.py.

2337  def __truediv__(self, other):
2338  """Create the Z3 expression `other/self`."""
2339  return self.__div__(other)
def __div__
Definition: z3py.py:2313
def __truediv__
Definition: z3py.py:2336
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 2189 of file z3py.py.

2190  def is_int(self):
2191  """Return `True` if `self` is an integer expression.
2192 
2193  >>> x = Int('x')
2194  >>> x.is_int()
2195  True
2196  >>> (x + 1).is_int()
2197  True
2198  >>> y = Real('y')
2199  >>> (x + y).is_int()
2200  False
2201  """
2202  return self.sort().is_int()
def sort
Definition: z3py.py:879
def is_int
Definition: z3py.py:2189
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 2203 of file z3py.py.

2204  def is_real(self):
2205  """Return `True` if `self` is an real expression.
2206 
2207  >>> x = Real('x')
2208  >>> x.is_real()
2209  True
2210  >>> (x + 1).is_real()
2211  True
2212  """
2213  return self.sort().is_real()
def sort
Definition: z3py.py:879
def is_real
Definition: z3py.py:2203
def sort (   self)
Return the sort (type) of the arithmetical expression `self`.

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

Definition at line 2179 of file z3py.py.

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

2180  def sort(self):
2181  """Return the sort (type) of the arithmetical expression `self`.
2182 
2183  >>> Int('x').sort()
2184  Int
2185  >>> (Real('x') + 1).sort()
2186  Real
2187  """
2188  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Arithmetic.
Definition: z3py.py:2090
def sort
Definition: z3py.py:2179
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.