Public Member Functions | |
__init__ (self, v=None, ctx=None) | |
__del__ (self) | |
__len__ (self) | |
__getitem__ (self, i) | |
__setitem__ (self, i, v) | |
push (self, v) | |
resize (self, sz) | |
__contains__ (self, item) | |
translate (self, other_ctx) | |
__copy__ (self) | |
__deepcopy__ (self, memo={}) | |
__repr__ (self) | |
sexpr (self) | |
![]() | |
use_pp (self) | |
Data Fields | |
vector = None | |
ctx = _get_ctx(ctx) | |
Additional Inherited Members | |
![]() | |
_repr_html_ (self) | |
__init__ | ( | self, | |
v = None, | |||
ctx = None ) |
Definition at line 5939 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 5950 of file z3py.py.
__contains__ | ( | self, | |
item ) |
Return `True` if the vector contains `item`. >>> x = Int('x') >>> A = AstVector() >>> x in A False >>> A.push(x) >>> x in A True >>> (x+1) in A False >>> A.push(x+1) >>> (x+1) in A True >>> A [x, x + 1]
Definition at line 6037 of file z3py.py.
__copy__ | ( | self | ) |
__deepcopy__ | ( | self, | |
memo = {} ) |
__getitem__ | ( | self, | |
i ) |
Return the AST at position `i`. >>> A = AstVector() >>> A.push(Int('x') + 1) >>> A.push(Int('y')) >>> A[0] x + 1 >>> A[1] y
Definition at line 5967 of file z3py.py.
__len__ | ( | self | ) |
Return the size of the vector `self`. >>> A = AstVector() >>> len(A) 0 >>> A.push(Int('x')) >>> A.push(Int('x')) >>> len(A) 2
Definition at line 5954 of file z3py.py.
Referenced by __getitem__(), and __setitem__().
__repr__ | ( | self | ) |
__setitem__ | ( | self, | |
i, | |||
v ) |
Update AST at position `i`. >>> A = AstVector() >>> A.push(Int('x') + 1) >>> A.push(Int('y')) >>> A[0] x + 1 >>> A[0] = Int('x') >>> A[0] x
Definition at line 5996 of file z3py.py.
push | ( | self, | |
v ) |
Add `v` in the end of the vector. >>> A = AstVector() >>> len(A) 0 >>> A.push(Int('x')) >>> len(A) 1
Definition at line 6012 of file z3py.py.
Referenced by Solver.__enter__().
resize | ( | self, | |
sz ) |
Resize the vector to `sz` elements. >>> A = AstVector() >>> A.resize(10) >>> len(A) 10 >>> for i in range(10): A[i] = Int('x') >>> A[5] x
Definition at line 6024 of file z3py.py.
sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the vector.
Definition at line 6085 of file z3py.py.
translate | ( | self, | |
other_ctx ) |
Copy vector `self` to context `other_ctx`. >>> x = Int('x') >>> A = AstVector() >>> A.push(x) >>> c2 = Context() >>> B = A.translate(c2) >>> B [x]
Definition at line 6060 of file z3py.py.
Referenced by __copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), __deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().
ctx = _get_ctx(ctx) |
Definition at line 5942 of file z3py.py.
Referenced by AstMap.__contains__(), __copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), __deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), __del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Solver.__del__(), Statistics.__del__(), AstMap.__getitem__(), __getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__len__(), __len__(), ModelRef.__len__(), Statistics.__len__(), AstMap.__repr__(), Statistics.__repr__(), AstMap.__setitem__(), __setitem__(), FuncEntry.arg_value(), FuncInterp.arity(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), ModelRef.get_interp(), Statistics.get_key_value(), ModelRef.get_sort(), ModelRef.get_universe(), AstMap.keys(), Statistics.keys(), Solver.model(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), Solver.pop(), ModelRef.project(), ModelRef.project_with_witness(), push(), Solver.push(), AstMap.reset(), Solver.reset(), resize(), Solver.set(), sexpr(), ModelRef.sexpr(), translate(), ModelRef.translate(), and FuncEntry.value().
vector = None |
Definition at line 5940 of file z3py.py.
Referenced by __del__(), __getitem__(), __len__(), __setitem__(), push(), resize(), sexpr(), and translate().