|
def | sort (self) |
|
def | domain (self) |
|
def | range (self) |
|
def | __getitem__ (self, arg) |
|
def | default (self) |
|
def | as_ast (self) |
|
def | get_id (self) |
|
def | sort (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 | __eq__ (self, other) |
|
def | __hash__ (self) |
|
def | __nonzero__ (self) |
|
def | __bool__ (self) |
|
def | sexpr (self) |
|
def | as_ast (self) |
|
def | get_id (self) |
|
def | ctx_ref (self) |
|
def | eq (self, other) |
|
def | translate (self, target) |
|
def | __copy__ (self) |
|
def | hash (self) |
|
def | use_pp (self) |
|
Array expressions.
Definition at line 4210 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 4240 of file z3py.py.
4240 def __getitem__(self, arg):
4241 """Return the Z3 expression `self[arg]`. 4243 >>> a = Array('a', IntSort(), BoolSort()) 4250 arg = self.domain().cast(arg)
4251 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 4253 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 4222 of file z3py.py.
4223 """Shorthand for `self.sort().domain()`. 4225 >>> a = Array('a', IntSort(), BoolSort()) 4229 return self.sort().domain()
◆ range()
Shorthand for `self.sort().range()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool
Definition at line 4231 of file z3py.py.
4232 """Shorthand for `self.sort().range()`. 4234 >>> a = Array('a', IntSort(), BoolSort()) 4238 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)
Definition at line 4213 of file z3py.py.
4214 """Return the array sort of the array expression `self`. 4216 >>> a = Array('a', IntSort(), BoolSort()) 4220 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.