Public Member Functions | |
def | __init__ |
def | __del__ |
def | __len__ |
def | __contains__ |
def | __getitem__ |
def | __setitem__ |
def | __repr__ |
def | erase |
def | reset |
def | keys |
Data Fields | |
map | |
ctx |
def __init__ | ( | self, | |
m = None , |
|||
ctx = None |
|||
) |
Definition at line 4939 of file z3py.py.
04939 04940 def __init__(self, m=None, ctx=None): 04941 self.map = None 04942 if m == None: 04943 self.ctx = _get_ctx(ctx) 04944 self.map = Z3_mk_ast_map(self.ctx.ref()) 04945 else: 04946 self.map = m 04947 assert ctx != None 04948 self.ctx = ctx 04949 Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
def __del__ | ( | self | ) |
def __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 4967 of file z3py.py.
04967 04968 def __contains__(self, key): 04969 """Return `True` if the map contains key `key`. 04970 04971 >>> M = AstMap() 04972 >>> x = Int('x') 04973 >>> M[x] = x + 1 04974 >>> x in M 04975 True 04976 >>> x+1 in M 04977 False 04978 """ 04979 return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
def __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 4980 of file z3py.py.
04980 04981 def __getitem__(self, key): 04982 """Retrieve the value associated with key `key`. 04983 04984 >>> M = AstMap() 04985 >>> x = Int('x') 04986 >>> M[x] = x + 1 04987 >>> M[x] 04988 x + 1 04989 """ 04990 return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
def __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 4954 of file z3py.py.
04954 04955 def __len__(self): 04956 """Return the size of the map. 04957 04958 >>> M = AstMap() 04959 >>> len(M) 04960 0 04961 >>> x = Int('x') 04962 >>> M[x] = IntVal(1) 04963 >>> len(M) 04964 1 04965 """ 04966 return int(Z3_ast_map_size(self.ctx.ref(), self.map))
def __repr__ | ( | self | ) |
def __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 4991 of file z3py.py.
04991 04992 def __setitem__(self, k, v): 04993 """Add/Update key `k` with value `v`. 04994 04995 >>> M = AstMap() 04996 >>> x = Int('x') 04997 >>> M[x] = x + 1 04998 >>> len(M) 04999 1 05000 >>> M[x] 05001 x + 1 05002 >>> M[x] = IntVal(1) 05003 >>> M[x] 05004 1 05005 """ 05006 Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
def 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 5010 of file z3py.py.
05010 05011 def erase(self, k): 05012 """Remove the entry associated with key `k`. 05013 05014 >>> M = AstMap() 05015 >>> x = Int('x') 05016 >>> M[x] = x + 1 05017 >>> len(M) 05018 1 05019 >>> M.erase(x) 05020 >>> len(M) 05021 0 05022 """ 05023 Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
def 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 5039 of file z3py.py.
05039 05040 def keys(self): 05041 """Return an AstVector containing all keys in the map. 05042 05043 >>> M = AstMap() 05044 >>> x = Int('x') 05045 >>> M[x] = x + 1 05046 >>> M[x+x] = IntVal(1) 05047 >>> M.keys() 05048 [x, x + x] 05049 """ 05050 return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
def 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 5024 of file z3py.py.
05024 05025 def reset(self): 05026 """Remove all entries from the map. 05027 05028 >>> M = AstMap() 05029 >>> x = Int('x') 05030 >>> M[x] = x + 1 05031 >>> M[x+x] = IntVal(1) 05032 >>> len(M) 05033 2 05034 >>> M.reset() 05035 >>> len(M) 05036 0 05037 """ 05038 Z3_ast_map_reset(self.ctx.ref(), self.map)
Definition at line 4939 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_rule(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 4939 of file z3py.py.
Referenced by AstMap::__contains__(), AstMap::__del__(), AstMap::__getitem__(), AstMap::__len__(), AstMap::__repr__(), AstMap::__setitem__(), AstMap::erase(), AstMap::keys(), and AstMap::reset().