Z3: 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 4852 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 4855 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 4866 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 4883 of file z3py.py.

 
     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
         """
         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 4896 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 4870 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 __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 4907 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 4926 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 4955 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 4940 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)

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation