AstMap Class Reference

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

---

Detailed Description

A mapping from ASTs to ASTs.

Definition at line 4996 of file z3py.py.

---

Constructor & Destructor Documentation

def __init__	(		self,
			m = None,
			ctx = None
	)

Definition at line 4999 of file z3py.py.

    def __init__(self, m=None, ctx=None):
        self.map = None
        if m == None:
            self.ctx = _get_ctx(ctx)
            self.map = Z3_mk_ast_map(self.ctx.ref())
        else:
            self.map = m
            assert ctx != None
            self.ctx    = ctx
        Z3_ast_map_inc_ref(self.ctx.ref(), self.map)

def __del__

(

self

)

Definition at line 5010 of file z3py.py.

    def __del__(self):
        if self.map != None:
            Z3_ast_map_dec_ref(self.ctx.ref(), self.map)

---

Member Function Documentation

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 5027 of file z3py.py.

05027 
05028     def __contains__(self, key):
05029         """Return `True` if the map contains key `key`.
05030 
05031         >>> M = AstMap()
05032         >>> x = Int('x')
05033         >>> M[x] = x + 1
05034         >>> x in M
05035         True
05036         >>> x+1 in M
05037         False
05038         """
05039         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 5040 of file z3py.py.

    def __getitem__(self, key):
        """Retrieve the value associated with key `key`.

        >>> M = AstMap()
        >>> x = Int('x')
        >>> M[x] = x + 1
        >>> M[x]
        x + 1
        """
        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 5014 of file z3py.py.

    def __len__(self):
        """Return the size of the map. 

        >>> M = AstMap()
        >>> len(M)
        0
        >>> x = Int('x')
        >>> M[x] = IntVal(1)
        >>> len(M)
        1
        """
        return int(Z3_ast_map_size(self.ctx.ref(), self.map))

def __repr__

(

self

)

Definition at line 5067 of file z3py.py.

    def __repr__(self):
        return Z3_ast_map_to_string(self.ctx.ref(), self.map)

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 5051 of file z3py.py.

    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
        """
        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 5070 of file z3py.py.

    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
        """
        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 5099 of file z3py.py.

    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]
        """
        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 5084 of file z3py.py.

    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
        """
        Z3_ast_map_reset(self.ctx.ref(), self.map)

---

Field Documentation

ctx

Definition at line 4999 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(), Optimize.add_soft(), 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(), ArrayRef.mk_default(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

map

Definition at line 4999 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().