RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3py_1_1_arith_ref.html below:

Z3: ArithRef Class Reference

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) def as_ast (self) def get_id (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) def __init__ (self, ast, ctx=None) def __del__ (self) def __deepcopy__ (self, memo={}) def __str__ (self) def __repr__ (self) def __nonzero__ (self) def __bool__ (self) def sexpr (self) def ctx_ref (self) def eq (self, other) def translate (self, target) def __copy__ (self) def hash (self) def use_pp (self)

Integer and Real expressions.

Definition at line 2430 of file z3py.py.

◆ __add__() 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 2468 of file z3py.py.

2468 def

__add__(self, other):

2469 """Create the Z3 expression `self + other`. 2478

a, b = _coerce_exprs(self, other)

2479 return

ArithRef(_mk_bin(Z3_mk_add, a, b), self.ctx)

◆ __div__() 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 2567 of file z3py.py.

2567 def

__div__(self, other):

2568 """Create the Z3 expression `other/self`. 2587

a, b = _coerce_exprs(self, other)

2588 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.

Referenced by ArithRef.__truediv__(), BitVecRef.__truediv__(), and FPRef.__truediv__().

◆ __ge__() 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 2701 of file z3py.py.

2701 def

__ge__(self, other):

2702 """Create the Z3 expression `other >= self`. 2704 >>> x, y = Ints('x y') 2711

a, b = _coerce_exprs(self, other)

2712 return

BoolRef(

Z3_mk_ge

(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)

Create greater than or equal to.

◆ __gt__() 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 2688 of file z3py.py.

2688 def

__gt__(self, other):

2689 """Create the Z3 expression `other > self`. 2691 >>> x, y = Ints('x y') 2698

a, b = _coerce_exprs(self, other)

2699 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.

◆ __le__() 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 2662 of file z3py.py.

2662 def

__le__(self, other):

2663 """Create the Z3 expression `other <= self`. 2665 >>> x, y = Ints('x y') 2672

a, b = _coerce_exprs(self, other)

2673 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.

◆ __lt__() 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 2675 of file z3py.py.

2675 def

__lt__(self, other):

2676 """Create the Z3 expression `other < self`. 2678 >>> x, y = Ints('x y') 2685

a, b = _coerce_exprs(self, other)

2686 return

BoolRef(

Z3_mk_lt

(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)

Create less than.

◆ __mod__() 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 2615 of file z3py.py.

2615 def

__mod__(self, other):

2616 """Create the Z3 expression `other%self`. 2622 >>> simplify(IntVal(10) % IntVal(3)) 2625

a, b = _coerce_exprs(self, other)

2627

_z3_assert(a.is_int(),

"Z3 integer expression expected"

)

2628 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.

◆ __mul__() 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 2491 of file z3py.py.

2491 def

__mul__(self, other):

2492 """Create the Z3 expression `self * other`. 2501 if

isinstance(other, BoolRef):

2502 return If

(other, self, 0)

2503

a, b = _coerce_exprs(self, other)

2504 return

ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)

def If(a, b, c, ctx=None)

◆ __neg__()

Return an expression representing `-self`.

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

Definition at line 2642 of file z3py.py.

2643 """Return an expression representing `-self`.

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 2653 of file z3py.py.

◆ __pow__() 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 2539 of file z3py.py.

2539 def

__pow__(self, other):

2540 """Create the Z3 expression `self**other` (** is the power operator). 2547 >>> simplify(IntVal(2)**8) 2550

a, b = _coerce_exprs(self, other)

2551 return

ArithRef(

Z3_mk_power

(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 ^ arg2.

◆ __radd__() def __radd__ ( self, other )

Create the Z3 expression `other + self`.

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

Definition at line 2481 of file z3py.py.

2481 def

__radd__(self, other):

2482 """Create the Z3 expression `other + self`. 2488

a, b = _coerce_exprs(self, other)

2489 return

ArithRef(_mk_bin(Z3_mk_add, b, a), self.ctx)

◆ __rdiv__() 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 2594 of file z3py.py.

2594 def

__rdiv__(self, other):

2595 """Create the Z3 expression `other/self`. 2608

a, b = _coerce_exprs(self, other)

2609 return

ArithRef(

Z3_mk_div

(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

Referenced by ArithRef.__rtruediv__(), BitVecRef.__rtruediv__(), and FPRef.__rtruediv__().

◆ __rmod__() def __rmod__ ( self, other )

Create the Z3 expression `other%self`.

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

Definition at line 2630 of file z3py.py.

2630 def

__rmod__(self, other):

2631 """Create the Z3 expression `other%self`. 2637

a, b = _coerce_exprs(self, other)

2639

_z3_assert(a.is_int(),

"Z3 integer expression expected"

)

2640 return

ArithRef(

Z3_mk_mod

(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

◆ __rmul__() def __rmul__ ( self, other )

Create the Z3 expression `other * self`.

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

Definition at line 2506 of file z3py.py.

2506 def

__rmul__(self, other):

2507 """Create the Z3 expression `other * self`. 2513

a, b = _coerce_exprs(self, other)

2514 return

ArithRef(_mk_bin(Z3_mk_mul, b, a), self.ctx)

◆ __rpow__() 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 2553 of file z3py.py.

2553 def

__rpow__(self, other):

2554 """Create the Z3 expression `other**self` (** is the power operator). 2561 >>> simplify(2**IntVal(8)) 2564

a, b = _coerce_exprs(self, other)

2565 return

ArithRef(

Z3_mk_power

(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)

◆ __rsub__() def __rsub__ ( self, other )

Create the Z3 expression `other - self`.

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

Definition at line 2529 of file z3py.py.

2529 def

__rsub__(self, other):

2530 """Create the Z3 expression `other - self`. 2536

a, b = _coerce_exprs(self, other)

2537 return

ArithRef(_mk_bin(Z3_mk_sub, b, a), self.ctx)

◆ __rtruediv__() def __rtruediv__ ( self, other )

Create the Z3 expression `other/self`.

Definition at line 2611 of file z3py.py.

2611 def

__rtruediv__(self, other):

2612 """Create the Z3 expression `other/self`.""" 2613 return

self.__rdiv__(other)

◆ __sub__() 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 2516 of file z3py.py.

2516 def

__sub__(self, other):

2517 """Create the Z3 expression `self - other`. 2526

a, b = _coerce_exprs(self, other)

2527 return

ArithRef(_mk_bin(Z3_mk_sub, a, b), self.ctx)

◆ __truediv__() def __truediv__ ( self, other )

Create the Z3 expression `other/self`.

Definition at line 2590 of file z3py.py.

2590 def

__truediv__(self, other):

2591 """Create the Z3 expression `other/self`.""" 2592 return

self.__div__(other)

◆ 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 2443 of file z3py.py.

2444 """Return `True` if `self` is an integer expression. 2449 >>> (x + 1).is_int() 2452 >>> (x + y).is_int() 2455 return

self.sort().

is_int

()

Referenced by IntNumRef.as_long(), and ArithSortRef.subsort().

◆ 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 2457 of file z3py.py.

2458 """Return `True` if `self` is an real expression. 2463 >>> (x + 1).is_real() 2466 return

self.sort().

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 2433 of file z3py.py.

2434 """Return the sort (type) of the arithmetical expression `self`. 2438 >>> (Real('x') + 1).sort() 2441 return

ArithSortRef(

Z3_get_sort

(self.ctx_ref(), self.as_ast()), self.ctx)

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

Referenced by FPNumRef.as_string(), ArrayRef.domain(), ArrayRef.domain_n(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4