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)
 
def from_string (self, s)
 
def serialize (self)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __deepcopy__
 
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 2376 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 2414 of file z3py.py.

2414  def __add__(self, other):
2415  """Create the Z3 expression `self + other`.
2416 
2417  >>> x = Int('x')
2418  >>> y = Int('y')
2419  >>> x + y
2420  x + y
2421  >>> (x + y).sort()
2422  Int
2423  """
2424  a, b = _coerce_exprs(self, other)
2425  return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
2426 
def __add__(self, other)
Definition: z3py.py:2414
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 2513 of file z3py.py.

2513  def __div__(self, other):
2514  """Create the Z3 expression `other/self`.
2515 
2516  >>> x = Int('x')
2517  >>> y = Int('y')
2518  >>> x/y
2519  x/y
2520  >>> (x/y).sort()
2521  Int
2522  >>> (x/y).sexpr()
2523  '(div x y)'
2524  >>> x = Real('x')
2525  >>> y = Real('y')
2526  >>> x/y
2527  x/y
2528  >>> (x/y).sort()
2529  Real
2530  >>> (x/y).sexpr()
2531  '(/ x y)'
2532  """
2533  a, b = _coerce_exprs(self, other)
2534  return ArithRef(Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2535 
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 ctx_ref(self)
Definition: z3py.py:400
def __div__(self, other)
Definition: z3py.py:2513
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 2647 of file z3py.py.

2647  def __ge__(self, other):
2648  """Create the Z3 expression `other >= self`.
2649 
2650  >>> x, y = Ints('x y')
2651  >>> x >= y
2652  x >= y
2653  >>> y = Real('y')
2654  >>> x >= y
2655  ToReal(x) >= y
2656  """
2657  a, b = _coerce_exprs(self, other)
2658  return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2659 
2660 
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
def __ge__(self, other)
Definition: z3py.py:2647
def ctx_ref(self)
Definition: z3py.py:400
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 2634 of file z3py.py.

2634  def __gt__(self, other):
2635  """Create the Z3 expression `other > self`.
2636 
2637  >>> x, y = Ints('x y')
2638  >>> x > y
2639  x > y
2640  >>> y = Real('y')
2641  >>> x > y
2642  ToReal(x) > y
2643  """
2644  a, b = _coerce_exprs(self, other)
2645  return BoolRef(Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2646 
def __gt__(self, other)
Definition: z3py.py:2634
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
def ctx_ref(self)
Definition: z3py.py:400
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 2608 of file z3py.py.

2608  def __le__(self, other):
2609  """Create the Z3 expression `other <= self`.
2610 
2611  >>> x, y = Ints('x y')
2612  >>> x <= y
2613  x <= y
2614  >>> y = Real('y')
2615  >>> x <= y
2616  ToReal(x) <= y
2617  """
2618  a, b = _coerce_exprs(self, other)
2619  return BoolRef(Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2620 
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
def __le__(self, other)
Definition: z3py.py:2608
def ctx_ref(self)
Definition: z3py.py:400
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 2621 of file z3py.py.

2621  def __lt__(self, other):
2622  """Create the Z3 expression `other < self`.
2623 
2624  >>> x, y = Ints('x y')
2625  >>> x < y
2626  x < y
2627  >>> y = Real('y')
2628  >>> x < y
2629  ToReal(x) < y
2630  """
2631  a, b = _coerce_exprs(self, other)
2632  return BoolRef(Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2633 
def __lt__(self, other)
Definition: z3py.py:2621
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
def ctx_ref(self)
Definition: z3py.py:400
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 2561 of file z3py.py.

2561  def __mod__(self, other):
2562  """Create the Z3 expression `other%self`.
2563 
2564  >>> x = Int('x')
2565  >>> y = Int('y')
2566  >>> x % y
2567  x%y
2568  >>> simplify(IntVal(10) % IntVal(3))
2569  1
2570  """
2571  a, b = _coerce_exprs(self, other)
2572  if z3_debug():
2573  _z3_assert(a.is_int(), "Z3 integer expression expected")
2574  return ArithRef(Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2575 
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__(self, other)
Definition: z3py.py:2561
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
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 2437 of file z3py.py.

2437  def __mul__(self, other):
2438  """Create the Z3 expression `self * other`.
2439 
2440  >>> x = Real('x')
2441  >>> y = Real('y')
2442  >>> x * y
2443  x*y
2444  >>> (x * y).sort()
2445  Real
2446  """
2447  if isinstance(other, BoolRef):
2448  return If(other, self, 0)
2449  a, b = _coerce_exprs(self, other)
2450  return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2451 
def If
Definition: z3py.py:1377
def __mul__(self, other)
Definition: z3py.py:2437
def __neg__ (   self)
Return an expression representing `-self`.

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

Definition at line 2588 of file z3py.py.

2588  def __neg__(self):
2589  """Return an expression representing `-self`.
2590 
2591  >>> x = Int('x')
2592  >>> -x
2593  -x
2594  >>> simplify(-(-x))
2595  x
2596  """
2597  return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2598 
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
def as_ast(self)
Definition: z3py.py:392
def __neg__(self)
Definition: z3py.py:2588
def ctx_ref(self)
Definition: z3py.py:400
def __pos__ (   self)
Return `self`.

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

Definition at line 2599 of file z3py.py.

2599  def __pos__(self):
2600  """Return `self`.
2601 
2602  >>> x = Int('x')
2603  >>> +x
2604  x
2605  """
2606  return self
2607 
def __pos__(self)
Definition: z3py.py:2599
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 2485 of file z3py.py.

2485  def __pow__(self, other):
2486  """Create the Z3 expression `self**other` (** is the power operator).
2487 
2488  >>> x = Real('x')
2489  >>> x**3
2490  x**3
2491  >>> (x**3).sort()
2492  Real
2493  >>> simplify(IntVal(2)**8)
2494  256
2495  """
2496  a, b = _coerce_exprs(self, other)
2497  return ArithRef(Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2498 
def __pow__(self, other)
Definition: z3py.py:2485
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(self)
Definition: z3py.py:400
def __radd__ (   self,
  other 
)
Create the Z3 expression `other + self`.

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

Definition at line 2427 of file z3py.py.

2427  def __radd__(self, other):
2428  """Create the Z3 expression `other + self`.
2429 
2430  >>> x = Int('x')
2431  >>> 10 + x
2432  10 + x
2433  """
2434  a, b = _coerce_exprs(self, other)
2435  return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
2436 
def __radd__(self, other)
Definition: z3py.py:2427
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 2540 of file z3py.py.

2540  def __rdiv__(self, other):
2541  """Create the Z3 expression `other/self`.
2542 
2543  >>> x = Int('x')
2544  >>> 10/x
2545  10/x
2546  >>> (10/x).sexpr()
2547  '(div 10 x)'
2548  >>> x = Real('x')
2549  >>> 10/x
2550  10/x
2551  >>> (10/x).sexpr()
2552  '(/ 10.0 x)'
2553  """
2554  a, b = _coerce_exprs(self, other)
2555  return ArithRef(Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2556 
def __rdiv__(self, other)
Definition: z3py.py:2540
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 ctx_ref(self)
Definition: z3py.py:400
def __rmod__ (   self,
  other 
)
Create the Z3 expression `other%self`.

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

Definition at line 2576 of file z3py.py.

2576  def __rmod__(self, other):
2577  """Create the Z3 expression `other%self`.
2578 
2579  >>> x = Int('x')
2580  >>> 10 % x
2581  10%x
2582  """
2583  a, b = _coerce_exprs(self, other)
2584  if z3_debug():
2585  _z3_assert(a.is_int(), "Z3 integer expression expected")
2586  return ArithRef(Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2587 
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__(self, other)
Definition: z3py.py:2576
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def __rmul__ (   self,
  other 
)
Create the Z3 expression `other * self`.

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

Definition at line 2452 of file z3py.py.

2452  def __rmul__(self, other):
2453  """Create the Z3 expression `other * self`.
2454 
2455  >>> x = Real('x')
2456  >>> 10 * x
2457  10*x
2458  """
2459  a, b = _coerce_exprs(self, other)
2460  return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2461 
def __rmul__(self, other)
Definition: z3py.py:2452
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 2499 of file z3py.py.

2499  def __rpow__(self, other):
2500  """Create the Z3 expression `other**self` (** is the power operator).
2501 
2502  >>> x = Real('x')
2503  >>> 2**x
2504  2**x
2505  >>> (2**x).sort()
2506  Real
2507  >>> simplify(2**IntVal(8))
2508  256
2509  """
2510  a, b = _coerce_exprs(self, other)
2511  return ArithRef(Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2512 
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(self)
Definition: z3py.py:400
def __rpow__(self, other)
Definition: z3py.py:2499
def __rsub__ (   self,
  other 
)
Create the Z3 expression `other - self`.

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

Definition at line 2475 of file z3py.py.

2475  def __rsub__(self, other):
2476  """Create the Z3 expression `other - self`.
2477 
2478  >>> x = Int('x')
2479  >>> 10 - x
2480  10 - x
2481  """
2482  a, b = _coerce_exprs(self, other)
2483  return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2484 
def __rsub__(self, other)
Definition: z3py.py:2475
def __rtruediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2557 of file z3py.py.

2557  def __rtruediv__(self, other):
2558  """Create the Z3 expression `other/self`."""
2559  return self.__rdiv__(other)
2560 
def __rdiv__(self, other)
Definition: z3py.py:2540
def __rtruediv__(self, other)
Definition: z3py.py:2557
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 2462 of file z3py.py.

2462  def __sub__(self, other):
2463  """Create the Z3 expression `self - other`.
2464 
2465  >>> x = Int('x')
2466  >>> y = Int('y')
2467  >>> x - y
2468  x - y
2469  >>> (x - y).sort()
2470  Int
2471  """
2472  a, b = _coerce_exprs(self, other)
2473  return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2474 
def __sub__(self, other)
Definition: z3py.py:2462
def __truediv__ (   self,
  other 
)
Create the Z3 expression `other/self`.

Definition at line 2536 of file z3py.py.

2536  def __truediv__(self, other):
2537  """Create the Z3 expression `other/self`."""
2538  return self.__div__(other)
2539 
def __truediv__(self, other)
Definition: z3py.py:2536
def __div__(self, other)
Definition: z3py.py:2513
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 2389 of file z3py.py.

2389  def is_int(self):
2390  """Return `True` if `self` is an integer expression.
2391 
2392  >>> x = Int('x')
2393  >>> x.is_int()
2394  True
2395  >>> (x + 1).is_int()
2396  True
2397  >>> y = Real('y')
2398  >>> (x + y).is_int()
2399  False
2400  """
2401  return self.sort().is_int()
2402 
def is_int(self)
Definition: z3py.py:2389
def sort(self)
Definition: z3py.py:974
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 2403 of file z3py.py.

2403  def is_real(self):
2404  """Return `True` if `self` is an real expression.
2405 
2406  >>> x = Real('x')
2407  >>> x.is_real()
2408  True
2409  >>> (x + 1).is_real()
2410  True
2411  """
2412  return self.sort().is_real()
2413 
def is_real(self)
Definition: z3py.py:2403
def sort(self)
Definition: z3py.py:974
def sort (   self)
Return the sort (type) of the arithmetical expression `self`.

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

Definition at line 2379 of file z3py.py.

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

2379  def sort(self):
2380  """Return the sort (type) of the arithmetical expression `self`.
2381 
2382  >>> Int('x').sort()
2383  Int
2384  >>> (Real('x') + 1).sort()
2385  Real
2386  """
2387  return ArithSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2388 
def as_ast(self)
Definition: z3py.py:392
Arithmetic.
Definition: z3py.py:2284
def sort(self)
Definition: z3py.py:2379
def ctx_ref(self)
Definition: z3py.py:400
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.