Z3
Public Member Functions | Data Fields
AstMap Class Reference

Public Member Functions

def __init__
 
def __deepcopy__
 
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 6007 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6010 of file z3py.py.

6010  def __init__(self, m=None, ctx=None):
6011  self.map = None
6012  if m is None:
6013  self.ctx = _get_ctx(ctx)
6014  self.map = Z3_mk_ast_map(self.ctx.ref())
6015  else:
6016  self.map = m
6017  assert ctx is not None
6018  self.ctx = ctx
6019  Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
6020 
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__
Definition: z3py.py:6010
def __del__ (   self)

Definition at line 6024 of file z3py.py.

6024  def __del__(self):
6025  if self.map is not None and self.ctx.ref() is not None and Z3_ast_map_dec_ref is not None:
6026  Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
6027 
def __del__(self)
Definition: z3py.py:6024
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 6041 of file z3py.py.

6041  def __contains__(self, key):
6042  """Return `True` if the map contains key `key`.
6043 
6044  >>> M = AstMap()
6045  >>> x = Int('x')
6046  >>> M[x] = x + 1
6047  >>> x in M
6048  True
6049  >>> x+1 in M
6050  False
6051  """
6052  return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
6053 
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:6041
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6021 of file z3py.py.

6021  def __deepcopy__(self, memo={}):
6022  return AstMap(self.map, self.ctx)
6023 
def __deepcopy__
Definition: z3py.py:6021
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 6054 of file z3py.py.

6054  def __getitem__(self, key):
6055  """Retrieve the value associated with key `key`.
6056 
6057  >>> M = AstMap()
6058  >>> x = Int('x')
6059  >>> M[x] = x + 1
6060  >>> M[x]
6061  x + 1
6062  """
6063  return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
6064 
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:6054
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 6028 of file z3py.py.

6028  def __len__(self):
6029  """Return the size of the map.
6030 
6031  >>> M = AstMap()
6032  >>> len(M)
6033  0
6034  >>> x = Int('x')
6035  >>> M[x] = IntVal(1)
6036  >>> len(M)
6037  1
6038  """
6039  return int(Z3_ast_map_size(self.ctx.ref(), self.map))
6040 
def __len__(self)
Definition: z3py.py:6028
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 6081 of file z3py.py.

6081  def __repr__(self):
6082  return Z3_ast_map_to_string(self.ctx.ref(), self.map)
6083 
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:6081
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 6065 of file z3py.py.

6065  def __setitem__(self, k, v):
6066  """Add/Update key `k` with value `v`.
6067 
6068  >>> M = AstMap()
6069  >>> x = Int('x')
6070  >>> M[x] = x + 1
6071  >>> len(M)
6072  1
6073  >>> M[x]
6074  x + 1
6075  >>> M[x] = IntVal(1)
6076  >>> M[x]
6077  1
6078  """
6079  Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
6080 
def __setitem__(self, k, v)
Definition: z3py.py:6065
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 6084 of file z3py.py.

6084  def erase(self, k):
6085  """Remove the entry associated with key `k`.
6086 
6087  >>> M = AstMap()
6088  >>> x = Int('x')
6089  >>> M[x] = x + 1
6090  >>> len(M)
6091  1
6092  >>> M.erase(x)
6093  >>> len(M)
6094  0
6095  """
6096  Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
6097 
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:6084
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 6113 of file z3py.py.

6113  def keys(self):
6114  """Return an AstVector containing all keys in the map.
6115 
6116  >>> M = AstMap()
6117  >>> x = Int('x')
6118  >>> M[x] = x + 1
6119  >>> M[x+x] = IntVal(1)
6120  >>> M.keys()
6121  [x, x + x]
6122  """
6123  return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
6124 
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:6113
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 6098 of file z3py.py.

6098  def reset(self):
6099  """Remove all entries from the map.
6100 
6101  >>> M = AstMap()
6102  >>> x = Int('x')
6103  >>> M[x] = x + 1
6104  >>> M[x+x] = IntVal(1)
6105  >>> len(M)
6106  2
6107  >>> M.reset()
6108  >>> len(M)
6109  0
6110  """
6111  Z3_ast_map_reset(self.ctx.ref(), self.map)
6112 
def reset(self)
Definition: z3py.py:6098
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