Array expressions.
Definition at line 4248 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 4278 of file z3py.py.
4278 def __getitem__(self, arg):
4279 """Return the Z3 expression `self[arg]`. 4281 >>> a = Array('a', IntSort(), BoolSort()) 4288 arg = self.domain().cast(arg)
4289 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 4291 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 4260 of file z3py.py.
4261 """Shorthand for `self.sort().domain()`. 4263 >>> a = Array('a', IntSort(), BoolSort()) 4267 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 4269 of file z3py.py.
4270 """Shorthand for `self.sort().range()`. 4272 >>> a = Array('a', IntSort(), BoolSort()) 4276 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 4251 of file z3py.py.
4252 """Return the array sort of the array expression `self`. 4254 >>> a = Array('a', IntSort(), BoolSort()) 4258 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.