Z3
Loading...
Searching...
No Matches
ArithRef Class Reference
Inheritance diagram for ArithRef:

Public Member Functions

 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)
Public Member Functions inherited from ExprRef
 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)
Public Member Functions inherited from AstRef
 __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)
Public Member Functions inherited from Z3PPObject
 use_pp (self)

Additional Inherited Members

Data Fields inherited from AstRef
 ast = ast
 ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)

Detailed Description

Integer and Real expressions.

Definition at line 2461 of file z3py.py.

Member Function Documentation

◆ __add__()

__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 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__()

__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 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__()

__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 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__()

__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 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__()

__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 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__()

__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 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__()

__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 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__()

__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 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__()

__neg__ ( self)
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 """
2682 return ArithRef(Z3_mk_unary_minus(self.ctx_ref(), self.as_ast()), self.ctx)
2683
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.

◆ __pos__()

__pos__ ( self)
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__()

__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 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__()

__radd__ ( self,
other )
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__()

__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 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__()

__rmod__ ( self,
other )
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__()

__rmul__ ( self,
other )
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__()

__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 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__()

__rsub__ ( self,
other )
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__()

__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 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()

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

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()

is_real ( self)
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()

sort ( self)
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.