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