Array expressions.
Definition at line 3986 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 4016 of file z3py.py.
4016 def __getitem__(self, arg):
4017 """Return the Z3 expression `self[arg]`. 4019 >>> a = Array('a', IntSort(), BoolSort()) 4026 arg = self.domain().cast(arg)
4027 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 4029 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 3998 of file z3py.py.
3999 """Shorthand for `self.sort().domain()`. 4001 >>> a = Array('a', IntSort(), BoolSort()) 4005 return self.sort().domain()
§ range()
Shorthand for `self.sort().range()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool
Definition at line 4007 of file z3py.py.
4008 """Shorthand for `self.sort().range()`. 4010 >>> a = Array('a', IntSort(), BoolSort()) 4014 return self.sort().range()
§ sort()
Return the array sort of the array expression `self`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.sort()
Array(Int, Bool)
Definition at line 3989 of file z3py.py.
3990 """Return the array sort of the array expression `self`. 3992 >>> a = Array('a', IntSort(), BoolSort()) 3996 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)