Array expressions.
Definition at line 4244 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 4274 of file z3py.py.
4274 def __getitem__(self, arg):
4275 """Return the Z3 expression `self[arg]`.
4277 >>> a = Array('a', IntSort(), BoolSort())
4284 arg = self.domain().cast(arg)
4285 return _to_expr_ref(
Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
◆ default()
◆ domain()
Shorthand for `self.sort().domain()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int
Definition at line 4256 of file z3py.py.
4257 """Shorthand for `self.sort().domain()`.
4259 >>> a = Array('a', IntSort(), BoolSort())
4263 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 4265 of file z3py.py.
4266 """Shorthand for `self.sort().range()`.
4268 >>> a = Array('a', IntSort(), BoolSort())
4272 return self.sort().
range()
◆ 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 4247 of file z3py.py.
4248 """Return the array sort of the array expression `self`.
4250 >>> a = Array('a', IntSort(), BoolSort())
4254 return ArraySortRef(
Z3_get_sort(self.ctx_ref(), self.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.
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 ...