|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
|
Z3
|
|
Inheritance diagram for ArrayRef:Public Member Functions | |
| def | sort |
| def | domain |
| def | range |
| def | __getitem__ |
| def | mk_default |
| Public Member Functions inherited from ExprRef | |
| def | as_ast |
| def | get_id |
| def | sort |
| def | sort_kind |
| def | __eq__ |
| def | __ne__ |
| def | decl |
| def | num_args |
| def | arg |
| def | children |
| Public Member Functions inherited from AstRef | |
| def | __init__ |
| def | __del__ |
| def | __str__ |
| def | __repr__ |
| def | sexpr |
| def | as_ast |
| def | get_id |
| def | ctx_ref |
| def | eq |
| def | translate |
| def | hash |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp |
Additional Inherited Members | |
| Data Fields inherited from AstRef | |
| ast | |
| ctx | |
| 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 3910 of file z3py.py.
| def domain | ( | self | ) |
Shorthand for `self.sort().domain()`.
>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int
Definition at line 3892 of file z3py.py.
Referenced by ArrayRef.__getitem__().
| def mk_default | ( | self | ) |
| def range | ( | self | ) |
| def sort | ( | self | ) |
1.8.5