Public Member Functions | |
sort (self) | |
domain (self) | |
domain_n (self, i) | |
range (self) | |
__getitem__ (self, arg) | |
default (self) | |
![]() | |
as_ast (self) | |
get_id (self) | |
sort_kind (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__ne__ (self, other) | |
params (self) | |
decl (self) | |
kind (self) | |
num_args (self) | |
arg (self, idx) | |
children (self) | |
from_string (self, s) | |
serialize (self) | |
![]() | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
py_value (self) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
__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 4672 of file z3py.py.
default | ( | self | ) |
domain | ( | self | ) |
Shorthand for `self.sort().domain()`. >>> a = Array('a', IntSort(), BoolSort()) >>> a.domain() Int
Definition at line 4650 of file z3py.py.
Referenced by domain().
domain_n | ( | self, | |
i ) |
Shorthand for self.sort().domain_n(i)`.
Definition at line 4659 of file z3py.py.
Referenced by domain_n().
range | ( | self | ) |
Shorthand for `self.sort().range()`. >>> a = Array('a', IntSort(), BoolSort()) >>> a.range() Bool
Definition at line 4663 of file z3py.py.
Referenced by range().
sort | ( | self | ) |
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 4641 of file z3py.py.