Public Member Functions | |
__init__ (self, m=None, ctx=None) | |
__deepcopy__ (self, memo={}) | |
__del__ (self) | |
__len__ (self) | |
__contains__ (self, key) | |
__getitem__ (self, key) | |
__setitem__ (self, k, v) | |
__repr__ (self) | |
erase (self, k) | |
reset (self) | |
keys (self) | |
Data Fields | |
map = None | |
ctx = _get_ctx(ctx) | |
__init__ | ( | self, | |
m = None, | |||
ctx = None ) |
Definition at line 6099 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 6113 of file z3py.py.
__contains__ | ( | self, | |
key ) |
Return `True` if the map contains key `key`. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> x in M True >>> x+1 in M False
Definition at line 6130 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__getitem__ | ( | self, | |
key ) |
Retrieve the value associated with key `key`. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> M[x] x + 1
Definition at line 6143 of file z3py.py.
__len__ | ( | self | ) |
Return the size of the map. >>> M = AstMap() >>> len(M) 0 >>> x = Int('x') >>> M[x] = IntVal(1) >>> len(M) 1
Definition at line 6117 of file z3py.py.
__repr__ | ( | self | ) |
__setitem__ | ( | self, | |
k, | |||
v ) |
Add/Update key `k` with value `v`. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> len(M) 1 >>> M[x] x + 1 >>> M[x] = IntVal(1) >>> M[x] 1
Definition at line 6154 of file z3py.py.
erase | ( | self, | |
k ) |
Remove the entry associated with key `k`. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> len(M) 1 >>> M.erase(x) >>> len(M) 0
Definition at line 6173 of file z3py.py.
keys | ( | self | ) |
Return an AstVector containing all keys in the map. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> M[x+x] = IntVal(1) >>> M.keys() [x, x + x]
Definition at line 6202 of file z3py.py.
reset | ( | self | ) |
Remove all entries from the map. >>> M = AstMap() >>> x = Int('x') >>> M[x] = x + 1 >>> M[x+x] = IntVal(1) >>> len(M) 2 >>> M.reset() >>> len(M) 0
Definition at line 6187 of file z3py.py.
ctx = _get_ctx(ctx) |
Definition at line 6102 of file z3py.py.
Referenced by __contains__(), FuncInterp.__copy__(), ModelRef.__copy__(), __deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), __del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Solver.__del__(), Statistics.__del__(), __getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), __len__(), ModelRef.__len__(), Statistics.__len__(), __repr__(), Statistics.__repr__(), __setitem__(), FuncEntry.arg_value(), FuncInterp.arity(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), erase(), ModelRef.eval(), ModelRef.get_interp(), Statistics.get_key_value(), ModelRef.get_sort(), ModelRef.get_universe(), 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(), Solver.push(), reset(), Solver.reset(), Solver.set(), ModelRef.sexpr(), ModelRef.translate(), and FuncEntry.value().
map = None |
Definition at line 6100 of file z3py.py.
Referenced by __contains__(), __deepcopy__(), __del__(), __getitem__(), __len__(), __repr__(), __setitem__(), erase(), keys(), and reset().