|
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 | __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 2197 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 2235 of file z3py.py.
2235 def __add__(self, other):
2236 """Create the Z3 expression `self + other`. 2245 a, b = _coerce_exprs(self, other)
2246 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 2334 of file z3py.py.
2334 def __div__(self, other):
2335 """Create the Z3 expression `other/self`. 2354 a, b = _coerce_exprs(self, other)
2355 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 2468 of file z3py.py.
2468 def __ge__(self, other):
2469 """Create the Z3 expression `other >= self`. 2471 >>> x, y = Ints('x y') 2478 a, b = _coerce_exprs(self, other)
2479 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 2455 of file z3py.py.
2455 def __gt__(self, other):
2456 """Create the Z3 expression `other > self`. 2458 >>> x, y = Ints('x y') 2465 a, b = _coerce_exprs(self, other)
2466 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 2429 of file z3py.py.
2429 def __le__(self, other):
2430 """Create the Z3 expression `other <= self`. 2432 >>> x, y = Ints('x y') 2439 a, b = _coerce_exprs(self, other)
2440 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 2442 of file z3py.py.
2442 def __lt__(self, other):
2443 """Create the Z3 expression `other < self`. 2445 >>> x, y = Ints('x y') 2452 a, b = _coerce_exprs(self, other)
2453 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 2382 of file z3py.py.
2382 def __mod__(self, other):
2383 """Create the Z3 expression `other%self`. 2389 >>> simplify(IntVal(10) % IntVal(3)) 2392 a, b = _coerce_exprs(self, other)
2394 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2395 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 2258 of file z3py.py.
2258 def __mul__(self, other):
2259 """Create the Z3 expression `self * other`. 2268 if isinstance(other, BoolRef):
2269 return If(other, self, 0)
2270 a, b = _coerce_exprs(self, other)
2271 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 2409 of file z3py.py.
2410 """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 2420 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 2306 of file z3py.py.
2306 def __pow__(self, other):
2307 """Create the Z3 expression `self**other` (** is the power operator). 2314 >>> simplify(IntVal(2)**8) 2317 a, b = _coerce_exprs(self, other)
2318 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 2248 of file z3py.py.
2248 def __radd__(self, other):
2249 """Create the Z3 expression `other + self`. 2255 a, b = _coerce_exprs(self, other)
2256 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 2361 of file z3py.py.
2361 def __rdiv__(self, other):
2362 """Create the Z3 expression `other/self`. 2375 a, b = _coerce_exprs(self, other)
2376 return ArithRef(
Z3_mk_div(self.ctx_ref(), b.as_ast(), a.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.__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 2397 of file z3py.py.
2397 def __rmod__(self, other):
2398 """Create the Z3 expression `other%self`. 2404 a, b = _coerce_exprs(self, other)
2406 _z3_assert(a.is_int(),
"Z3 integer expression expected")
2407 return ArithRef(
Z3_mk_mod(self.ctx_ref(), b.as_ast(), a.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.
◆ __rmul__()
def __rmul__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Create the Z3 expression `other * self`.
>>> x = Real('x')
>>> 10 * x
10*x
Definition at line 2273 of file z3py.py.
2273 def __rmul__(self, other):
2274 """Create the Z3 expression `other * self`. 2280 a, b = _coerce_exprs(self, other)
2281 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 2320 of file z3py.py.
2320 def __rpow__(self, other):
2321 """Create the Z3 expression `other**self` (** is the power operator). 2328 >>> simplify(2**IntVal(8)) 2331 a, b = _coerce_exprs(self, other)
2332 return ArithRef(
Z3_mk_power(self.ctx_ref(), b.as_ast(), a.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.
◆ __rsub__()
def __rsub__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Create the Z3 expression `other - self`.
>>> x = Int('x')
>>> 10 - x
10 - x
Definition at line 2296 of file z3py.py.
2296 def __rsub__(self, other):
2297 """Create the Z3 expression `other - self`. 2303 a, b = _coerce_exprs(self, other)
2304 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 2378 of file z3py.py.
2378 def __rtruediv__(self, other):
2379 """Create the Z3 expression `other/self`.""" 2380 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 2283 of file z3py.py.
2283 def __sub__(self, other):
2284 """Create the Z3 expression `self - other`. 2293 a, b = _coerce_exprs(self, other)
2294 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 2357 of file z3py.py.
2357 def __truediv__(self, other):
2358 """Create the Z3 expression `other/self`.""" 2359 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 2210 of file z3py.py.
2211 """Return `True` if `self` is an integer expression. 2216 >>> (x + 1).is_int() 2219 >>> (x + y).is_int() 2222 return self.sort().
is_int()
Referenced by IntNumRef.as_long().
◆ 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 2224 of file z3py.py.
2225 """Return `True` if `self` is an real expression. 2230 >>> (x + 1).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 2200 of file z3py.py.
2201 """Return the sort (type) of the arithmetical expression `self`. 2205 >>> (Real('x') + 1).sort() 2208 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.