|
| sort (self) |
|
| is_int (self) |
|
| is_real (self) |
|
| __add__ (self, other) |
|
| __radd__ (self, other) |
|
| __mul__ (self, other) |
|
| __rmul__ (self, other) |
|
| __sub__ (self, other) |
|
| __rsub__ (self, other) |
|
| __pow__ (self, other) |
|
| __rpow__ (self, other) |
|
| __div__ (self, other) |
|
| __truediv__ (self, other) |
|
| __rdiv__ (self, other) |
|
| __rtruediv__ (self, other) |
|
| __mod__ (self, other) |
|
| __rmod__ (self, other) |
|
| __neg__ (self) |
|
| __pos__ (self) |
|
| __le__ (self, other) |
|
| __lt__ (self, other) |
|
| __gt__ (self, other) |
|
| __ge__ (self, other) |
|
| as_ast (self) |
|
| get_id (self) |
|
| sort_kind (self) |
|
| __eq__ (self, other) |
|
| __hash__ (self) |
|
| __ne__ (self, other) |
|
| params (self) |
|
| decl (self) |
|
| kind (self) |
|
| num_args (self) |
|
| arg (self, idx) |
|
| children (self) |
|
| from_string (self, s) |
|
| serialize (self) |
|
| __init__ (self, ast, ctx=None) |
|
| __del__ (self) |
|
| __deepcopy__ (self, memo={}) |
|
| __str__ (self) |
|
| __repr__ (self) |
|
| __eq__ (self, other) |
|
| __hash__ (self) |
|
| __nonzero__ (self) |
|
| __bool__ (self) |
|
| sexpr (self) |
|
| ctx_ref (self) |
|
| eq (self, other) |
|
| translate (self, target) |
|
| __copy__ (self) |
|
| hash (self) |
|
| py_value (self) |
|
| use_pp (self) |
|
Integer and Real expressions.
Definition at line 2461 of file z3py.py.
◆ __add__()
Create the Z3 expression `self + other`.
>>> x = Int('x')
>>> y = Int('y')
>>> x + y
x + y
>>> (x + y).sort()
Int
Definition at line 2499 of file z3py.py.
2499 def __add__(self, other):
2500 """Create the Z3 expression `self + other`.
2501
2502 >>> x = Int('x')
2503 >>> y = Int('y')
2504 >>> x + y
2505 x + y
2506 >>> (x + y).sort()
2507 Int
2508 """
2509 a, b = _coerce_exprs(self, other)
2510 return ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)
2511
◆ __div__()
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 2598 of file z3py.py.
2598 def __div__(self, other):
2599 """Create the Z3 expression `other/self`.
2600
2601 >>> x = Int('x')
2602 >>> y = Int('y')
2603 >>> x/y
2604 x/y
2605 >>> (x/y).sort()
2606 Int
2607 >>> (x/y).sexpr()
2608 '(div x y)'
2609 >>> x = Real('x')
2610 >>> y = Real('y')
2611 >>> x/y
2612 x/y
2613 >>> (x/y).sort()
2614 Real
2615 >>> (x/y).sexpr()
2616 '(/ x y)'
2617 """
2618 a, b = _coerce_exprs(self, other)
2619 return ArithRef(
Z3_mk_div(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2620
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Referenced by __truediv__(), and BitVecRef.__truediv__().
◆ __ge__()
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 2732 of file z3py.py.
2732 def __ge__(self, other):
2733 """Create the Z3 expression `other >= self`.
2734
2735 >>> x, y = Ints('x y')
2736 >>> x >= y
2737 x >= y
2738 >>> y = Real('y')
2739 >>> x >= y
2740 ToReal(x) >= y
2741 """
2742 a, b = _coerce_exprs(self, other)
2743 return BoolRef(
Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2744
2745
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
◆ __gt__()
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 2719 of file z3py.py.
2719 def __gt__(self, other):
2720 """Create the Z3 expression `other > self`.
2721
2722 >>> x, y = Ints('x y')
2723 >>> x > y
2724 x > y
2725 >>> y = Real('y')
2726 >>> x > y
2727 ToReal(x) > y
2728 """
2729 a, b = _coerce_exprs(self, other)
2730 return BoolRef(
Z3_mk_gt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2731
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
◆ __le__()
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 2693 of file z3py.py.
2693 def __le__(self, other):
2694 """Create the Z3 expression `other <= self`.
2695
2696 >>> x, y = Ints('x y')
2697 >>> x <= y
2698 x <= y
2699 >>> y = Real('y')
2700 >>> x <= y
2701 ToReal(x) <= y
2702 """
2703 a, b = _coerce_exprs(self, other)
2704 return BoolRef(
Z3_mk_le(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2705
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
◆ __lt__()
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 2706 of file z3py.py.
2706 def __lt__(self, other):
2707 """Create the Z3 expression `other < self`.
2708
2709 >>> x, y = Ints('x y')
2710 >>> x < y
2711 x < y
2712 >>> y = Real('y')
2713 >>> x < y
2714 ToReal(x) < y
2715 """
2716 a, b = _coerce_exprs(self, other)
2717 return BoolRef(
Z3_mk_lt(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2718
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
◆ __mod__()
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 2646 of file z3py.py.
2646 def __mod__(self, other):
2647 """Create the Z3 expression `other%self`.
2648
2649 >>> x = Int('x')
2650 >>> y = Int('y')
2651 >>> x % y
2652 x%y
2653 >>> simplify(IntVal(10) % IntVal(3))
2654 1
2655 """
2656 a, b = _coerce_exprs(self, other)
2657 if z3_debug():
2658 _z3_assert(a.is_int(), "Z3 integer expression expected")
2659 return ArithRef(
Z3_mk_mod(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2660
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__()
Create the Z3 expression `self * other`.
>>> x = Real('x')
>>> y = Real('y')
>>> x * y
x*y
>>> (x * y).sort()
Real
Definition at line 2522 of file z3py.py.
2522 def __mul__(self, other):
2523 """Create the Z3 expression `self * other`.
2524
2525 >>> x = Real('x')
2526 >>> y = Real('y')
2527 >>> x * y
2528 x*y
2529 >>> (x * y).sort()
2530 Real
2531 """
2532 if isinstance(other, BoolRef):
2533 return If(other, self, 0)
2534 a, b = _coerce_exprs(self, other)
2535 return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
2536
◆ __neg__()
Return an expression representing `-self`.
>>> x = Int('x')
>>> -x
-x
>>> simplify(-(-x))
x
Definition at line 2673 of file z3py.py.
2673 def __neg__(self):
2674 """Return an expression representing `-self`.
2675
2676 >>> x = Int('x')
2677 >>> -x
2678 -x
2679 >>> simplify(-(-x))
2680 x
2681 """
2683
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
◆ __pos__()
Return `self`.
>>> x = Int('x')
>>> +x
x
Definition at line 2684 of file z3py.py.
2684 def __pos__(self):
2685 """Return `self`.
2686
2687 >>> x = Int('x')
2688 >>> +x
2689 x
2690 """
2691 return self
2692
◆ __pow__()
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 2570 of file z3py.py.
2570 def __pow__(self, other):
2571 """Create the Z3 expression `self**other` (** is the power operator).
2572
2573 >>> x = Real('x')
2574 >>> x**3
2575 x**3
2576 >>> (x**3).sort()
2577 Real
2578 >>> simplify(IntVal(2)**8)
2579 256
2580 """
2581 a, b = _coerce_exprs(self, other)
2582 return ArithRef(
Z3_mk_power(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
2583
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
◆ __radd__()
Create the Z3 expression `other + self`.
>>> x = Int('x')
>>> 10 + x
10 + x
Definition at line 2512 of file z3py.py.
2512 def __radd__(self, other):
2513 """Create the Z3 expression `other + self`.
2514
2515 >>> x = Int('x')
2516 >>> 10 + x
2517 10 + x
2518 """
2519 a, b = _coerce_exprs(self, other)
2520 return ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)
2521
◆ __rdiv__()
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 2625 of file z3py.py.
2625 def __rdiv__(self, other):
2626 """Create the Z3 expression `other/self`.
2627
2628 >>> x = Int('x')
2629 >>> 10/x
2630 10/x
2631 >>> (10/x).sexpr()
2632 '(div 10 x)'
2633 >>> x = Real('x')
2634 >>> 10/x
2635 10/x
2636 >>> (10/x).sexpr()
2637 '(/ 10.0 x)'
2638 """
2639 a, b = _coerce_exprs(self, other)
2640 return ArithRef(
Z3_mk_div(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2641
Referenced by __rtruediv__(), and BitVecRef.__rtruediv__().
◆ __rmod__()
Create the Z3 expression `other%self`.
>>> x = Int('x')
>>> 10 % x
10%x
Definition at line 2661 of file z3py.py.
2661 def __rmod__(self, other):
2662 """Create the Z3 expression `other%self`.
2663
2664 >>> x = Int('x')
2665 >>> 10 % x
2666 10%x
2667 """
2668 a, b = _coerce_exprs(self, other)
2669 if z3_debug():
2670 _z3_assert(a.is_int(), "Z3 integer expression expected")
2671 return ArithRef(
Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2672
◆ __rmul__()
Create the Z3 expression `other * self`.
>>> x = Real('x')
>>> 10 * x
10*x
Definition at line 2537 of file z3py.py.
2537 def __rmul__(self, other):
2538 """Create the Z3 expression `other * self`.
2539
2540 >>> x = Real('x')
2541 >>> 10 * x
2542 10*x
2543 """
2544 a, b = _coerce_exprs(self, other)
2545 return ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)
2546
◆ __rpow__()
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 2584 of file z3py.py.
2584 def __rpow__(self, other):
2585 """Create the Z3 expression `other**self` (** is the power operator).
2586
2587 >>> x = Real('x')
2588 >>> 2**x
2589 2**x
2590 >>> (2**x).sort()
2591 Real
2592 >>> simplify(2**IntVal(8))
2593 256
2594 """
2595 a, b = _coerce_exprs(self, other)
2596 return ArithRef(
Z3_mk_power(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
2597
◆ __rsub__()
Create the Z3 expression `other - self`.
>>> x = Int('x')
>>> 10 - x
10 - x
Definition at line 2560 of file z3py.py.
2560 def __rsub__(self, other):
2561 """Create the Z3 expression `other - self`.
2562
2563 >>> x = Int('x')
2564 >>> 10 - x
2565 10 - x
2566 """
2567 a, b = _coerce_exprs(self, other)
2568 return ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)
2569
◆ __rtruediv__()
__rtruediv__ |
( |
| self, |
|
|
| other ) |
Create the Z3 expression `other/self`.
Definition at line 2642 of file z3py.py.
2642 def __rtruediv__(self, other):
2643 """Create the Z3 expression `other/self`."""
2644 return self.__rdiv__(other)
2645
◆ __sub__()
Create the Z3 expression `self - other`.
>>> x = Int('x')
>>> y = Int('y')
>>> x - y
x - y
>>> (x - y).sort()
Int
Definition at line 2547 of file z3py.py.
2547 def __sub__(self, other):
2548 """Create the Z3 expression `self - other`.
2549
2550 >>> x = Int('x')
2551 >>> y = Int('y')
2552 >>> x - y
2553 x - y
2554 >>> (x - y).sort()
2555 Int
2556 """
2557 a, b = _coerce_exprs(self, other)
2558 return ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)
2559
◆ __truediv__()
__truediv__ |
( |
| self, |
|
|
| other ) |
Create the Z3 expression `other/self`.
Definition at line 2621 of file z3py.py.
2621 def __truediv__(self, other):
2622 """Create the Z3 expression `other/self`."""
2623 return self.__div__(other)
2624
◆ is_int()
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
Reimplemented in RatNumRef.
Definition at line 2474 of file z3py.py.
2474 def is_int(self):
2475 """Return `True` if `self` is an integer expression.
2476
2477 >>> x = Int('x')
2478 >>> x.is_int()
2479 True
2480 >>> (x + 1).is_int()
2481 True
2482 >>> y = Real('y')
2483 >>> (x + y).is_int()
2484 False
2485 """
2486 return self.sort().is_int()
2487
Referenced by IntNumRef.as_long(), and is_int().
◆ is_real()
Return `True` if `self` is an real expression.
>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True
Reimplemented in RatNumRef.
Definition at line 2488 of file z3py.py.
2488 def is_real(self):
2489 """Return `True` if `self` is an real expression.
2490
2491 >>> x = Real('x')
2492 >>> x.is_real()
2493 True
2494 >>> (x + 1).is_real()
2495 True
2496 """
2497 return self.sort().is_real()
2498
Referenced by is_real().
◆ sort()
Return the sort (type) of the arithmetical expression `self`.
>>> Int('x').sort()
Int
>>> (Real('x') + 1).sort()
Real
Reimplemented from ExprRef.
Definition at line 2464 of file z3py.py.
2464 def sort(self):
2465 """Return the sort (type) of the arithmetical expression `self`.
2466
2467 >>> Int('x').sort()
2468 Int
2469 >>> (Real('x') + 1).sort()
2470 Real
2471 """
2472 return ArithSortRef(
Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
2473
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.