Array expressions.
Definition at line 4216 of file z3py.py.
◆ __getitem__()
def __getitem__ |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Return the Z3 expression `self[arg]`.
>>> a = Array('a', IntSort(), BoolSort())
>>> i = Int('i')
>>> a[i]
a[i]
>>> a[i].sexpr()
'(select a i)'
Definition at line 4246 of file z3py.py.
4246 def __getitem__(self, arg):
4247 """Return the Z3 expression `self[arg]`. 4249 >>> a = Array('a', IntSort(), BoolSort()) 4256 arg = self.domain().cast(arg)
4257 return _to_expr_ref(
Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
◆ default()
Definition at line 4259 of file z3py.py.
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
◆ domain()
Shorthand for `self.sort().domain()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int
Definition at line 4228 of file z3py.py.
4229 """Shorthand for `self.sort().domain()`. 4231 >>> a = Array('a', IntSort(), BoolSort()) 4235 return self.sort().domain()
Referenced by ArrayRef.__getitem__().
◆ range()
Shorthand for `self.sort().range()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool
Definition at line 4237 of file z3py.py.
4238 """Shorthand for `self.sort().range()`. 4240 >>> a = Array('a', IntSort(), BoolSort()) 4244 return self.sort().
range()
expr range(expr const &lo, expr const &hi)
◆ sort()
Return the array sort of the array expression `self`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.sort()
Array(Int, Bool)
Reimplemented from ExprRef.
Definition at line 4219 of file z3py.py.
4220 """Return the array sort of the array expression `self`. 4222 >>> a = Array('a', IntSort(), BoolSort()) 4226 return ArraySortRef(
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.