Z3
Public Member Functions | Data Fields
AstMap Class Reference

Public Member Functions

def __init__ (self, m=None, ctx=None)
 
def __del__ (self)
 
def __len__ (self)
 
def __contains__ (self, key)
 
def __getitem__ (self, key)
 
def __setitem__ (self, k, v)
 
def __repr__ (self)
 
def erase (self, k)
 
def reset (self)
 
def keys (self)
 

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.

4999  def __init__(self, m=None, ctx=None):
5000  self.map = None
5001  if m == None:
5002  self.ctx = _get_ctx(ctx)
5003  self.map = Z3_mk_ast_map(self.ctx.ref())
5004  else:
5005  self.map = m
5006  assert ctx != None
5007  self.ctx = ctx
5008  Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
5009 
void Z3_API Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m)
Increment the reference counter of the given AST map.
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c)
Return an empty mapping from AST to AST.
def __init__(self, m=None, ctx=None)
Definition: z3py.py:4999
def __del__ (   self)

Definition at line 5010 of file z3py.py.

5010  def __del__(self):
5011  if self.map != None:
5012  Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
5013 
def __del__(self)
Definition: z3py.py:5010
void Z3_API Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m)
Decrement the reference counter of the given AST 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.

5027  def __contains__(self, key):
5028  """Return `True` if the map contains key `key`.
5029 
5030  >>> M = AstMap()
5031  >>> x = Int('x')
5032  >>> M[x] = x + 1
5033  >>> x in M
5034  True
5035  >>> x+1 in M
5036  False
5037  """
5038  return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
5039 
Z3_bool Z3_API Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k)
Return true if the map m contains the AST key k.
def __contains__(self, key)
Definition: z3py.py:5027
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.

5040  def __getitem__(self, key):
5041  """Retrieve the value associated with key `key`.
5042 
5043  >>> M = AstMap()
5044  >>> x = Int('x')
5045  >>> M[x] = x + 1
5046  >>> M[x]
5047  x + 1
5048  """
5049  return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
5050 
Z3_ast Z3_API Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k)
Return the value associated with the key k.
def __getitem__(self, key)
Definition: z3py.py:5040
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.

5014  def __len__(self):
5015  """Return the size of the map.
5016 
5017  >>> M = AstMap()
5018  >>> len(M)
5019  0
5020  >>> x = Int('x')
5021  >>> M[x] = IntVal(1)
5022  >>> len(M)
5023  1
5024  """
5025  return int(Z3_ast_map_size(self.ctx.ref(), self.map))
5026 
def __len__(self)
Definition: z3py.py:5014
unsigned Z3_API Z3_ast_map_size(Z3_context c, Z3_ast_map m)
Return the size of the given map.
def __repr__ (   self)

Definition at line 5067 of file z3py.py.

5067  def __repr__(self):
5068  return Z3_ast_map_to_string(self.ctx.ref(), self.map)
5069 
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m)
Convert the given map into a string.
def __repr__(self)
Definition: z3py.py:5067
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.

5051  def __setitem__(self, k, v):
5052  """Add/Update key `k` with value `v`.
5053 
5054  >>> M = AstMap()
5055  >>> x = Int('x')
5056  >>> M[x] = x + 1
5057  >>> len(M)
5058  1
5059  >>> M[x]
5060  x + 1
5061  >>> M[x] = IntVal(1)
5062  >>> M[x]
5063  1
5064  """
5065  Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
5066 
def __setitem__(self, k, v)
Definition: z3py.py:5051
void Z3_API Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v)
Store/Replace a new key, value pair in the given map.
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.

5070  def erase(self, k):
5071  """Remove the entry associated with key `k`.
5072 
5073  >>> M = AstMap()
5074  >>> x = Int('x')
5075  >>> M[x] = x + 1
5076  >>> len(M)
5077  1
5078  >>> M.erase(x)
5079  >>> len(M)
5080  0
5081  """
5082  Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
5083 
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k)
Erase a key from the map.
def erase(self, k)
Definition: z3py.py:5070
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.

5099  def keys(self):
5100  """Return an AstVector containing all keys in the map.
5101 
5102  >>> M = AstMap()
5103  >>> x = Int('x')
5104  >>> M[x] = x + 1
5105  >>> M[x+x] = IntVal(1)
5106  >>> M.keys()
5107  [x, x + x]
5108  """
5109  return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
5110 
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m)
Return the keys stored in the given map.
def keys(self)
Definition: z3py.py:5099
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.

5084  def reset(self):
5085  """Remove all entries from the map.
5086 
5087  >>> M = AstMap()
5088  >>> x = Int('x')
5089  >>> M[x] = x + 1
5090  >>> M[x+x] = IntVal(1)
5091  >>> len(M)
5092  2
5093  >>> M.reset()
5094  >>> len(M)
5095  0
5096  """
5097  Z3_ast_map_reset(self.ctx.ref(), self.map)
5098 
def reset(self)
Definition: z3py.py:5084
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m)
Remove all keys from the given map.

Field Documentation

ctx
map