Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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 4852 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 4855 of file z3py.py.

4856  def __init__(self, m=None, ctx=None):
4857  self.map = None
4858  if m == None:
4859  self.ctx = _get_ctx(ctx)
4860  self.map = Z3_mk_ast_map(self.ctx.ref())
4861  else:
4862  self.map = m
4863  assert ctx != None
4864  self.ctx = ctx
4865  Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
def __del__ (   self)

Definition at line 4866 of file z3py.py.

4867  def __del__(self):
4868  if self.map != None:
4869  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.

4884  def __contains__(self, key):
4885  """Return `True` if the map contains key `key`.
4886 
4887  >>> M = AstMap()
4888  >>> x = Int('x')
4889  >>> M[x] = x + 1
4890  >>> x in M
4891  True
4892  >>> x+1 in M
4893  False
4894  """
4895  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.

4897  def __getitem__(self, key):
4898  """Retrieve the value associated with key `key`.
4899 
4900  >>> M = AstMap()
4901  >>> x = Int('x')
4902  >>> M[x] = x + 1
4903  >>> M[x]
4904  x + 1
4905  """
4906  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.

4871  def __len__(self):
4872  """Return the size of the map.
4873 
4874  >>> M = AstMap()
4875  >>> len(M)
4876  0
4877  >>> x = Int('x')
4878  >>> M[x] = IntVal(1)
4879  >>> len(M)
4880  1
4881  """
4882  return int(Z3_ast_map_size(self.ctx.ref(), self.map))
def __repr__ (   self)

Definition at line 4923 of file z3py.py.

4924  def __repr__(self):
4925  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 4907 of file z3py.py.

4908  def __setitem__(self, k, v):
4909  """Add/Update key `k` with value `v`.
4910 
4911  >>> M = AstMap()
4912  >>> x = Int('x')
4913  >>> M[x] = x + 1
4914  >>> len(M)
4915  1
4916  >>> M[x]
4917  x + 1
4918  >>> M[x] = IntVal(1)
4919  >>> M[x]
4920  1
4921  """
4922  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.

4927  def erase(self, k):
4928  """Remove the entry associated with key `k`.
4929 
4930  >>> M = AstMap()
4931  >>> x = Int('x')
4932  >>> M[x] = x + 1
4933  >>> len(M)
4934  1
4935  >>> M.erase(x)
4936  >>> len(M)
4937  0
4938  """
4939  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.

4956  def keys(self):
4957  """Return an AstVector containing all keys in the map.
4958 
4959  >>> M = AstMap()
4960  >>> x = Int('x')
4961  >>> M[x] = x + 1
4962  >>> M[x+x] = IntVal(1)
4963  >>> M.keys()
4964  [x, x + x]
4965  """
4966  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.

4941  def reset(self):
4942  """Remove all entries from the map.
4943 
4944  >>> M = AstMap()
4945  >>> x = Int('x')
4946  >>> M[x] = x + 1
4947  >>> M[x+x] = IntVal(1)
4948  >>> len(M)
4949  2
4950  >>> M.reset()
4951  >>> len(M)
4952  0
4953  """
4954  Z3_ast_map_reset(self.ctx.ref(), self.map)

Field Documentation

ctx

Definition at line 4858 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), AstMap.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Tactic.solver(), and Fixedpoint.statistics().

map

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