Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
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 4936 of file z3py.py.


Constructor & Destructor Documentation

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)

Definition at line 4950 of file z3py.py.

04950 
04951     def __del__(self):
04952         if self.map != None:
04953             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 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)

Definition at line 5007 of file z3py.py.

05007 
05008     def __repr__(self):
05009         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 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)


Field Documentation

ctx

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().

map
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines