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 4996 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 4999 of file z3py.py.

4999 
5000  def __init__(self, m=None, ctx=None):
5001  self.map = None
5002  if m == None:
5003  self.ctx = _get_ctx(ctx)
5004  self.map = Z3_mk_ast_map(self.ctx.ref())
5005  else:
5006  self.map = m
5007  assert ctx != None
5008  self.ctx = ctx
5009  Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
Z3_ast_map_inc_ref
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_mk_ast_map
Z3_ast_map Z3_API Z3_mk_ast_map(Z3_context c)
Return an empty mapping from AST to AST.
z3py.AstMap.__init__
def __init__
Definition: z3py.py:4999
def __del__ (   self)

Definition at line 5010 of file z3py.py.

5010 
5011  def __del__(self):
5012  if self.map != None:
5013  Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
z3py.AstMap.__del__
def __del__
Definition: z3py.py:5010
Z3_ast_map_dec_ref
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 
5028  def __contains__(self, key):
5029  """Return `True` if the map contains key `key`.
5030 
5031  >>> M = AstMap()
5032  >>> x = Int('x')
5033  >>> M[x] = x + 1
5034  >>> x in M
5035  True
5036  >>> x+1 in M
5037  False
5038  """
5039  return Z3_ast_map_contains(self.ctx.ref(), self.map, key.as_ast())
z3py.AstMap.__contains__
def __contains__
Definition: z3py.py:5027
Z3_ast_map_contains
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 __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 
5041  def __getitem__(self, key):
5042  """Retrieve the value associated with key `key`.
5043 
5044  >>> M = AstMap()
5045  >>> x = Int('x')
5046  >>> M[x] = x + 1
5047  >>> M[x]
5048  x + 1
5049  """
5050  return _to_ast_ref(Z3_ast_map_find(self.ctx.ref(), self.map, key.as_ast()), self.ctx)
z3py.AstMap.__getitem__
def __getitem__
Definition: z3py.py:5040
Z3_ast_map_find
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 __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 
5015  def __len__(self):
5016  """Return the size of the map.
5017 
5018  >>> M = AstMap()
5019  >>> len(M)
5020  0
5021  >>> x = Int('x')
5022  >>> M[x] = IntVal(1)
5023  >>> len(M)
5024  1
5025  """
5026  return int(Z3_ast_map_size(self.ctx.ref(), self.map))
z3py.AstMap.__len__
def __len__
Definition: z3py.py:5014
Z3_ast_map_size
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 
5068  def __repr__(self):
5069  return Z3_ast_map_to_string(self.ctx.ref(), self.map)
z3py.AstMap.__repr__
def __repr__
Definition: z3py.py:5067
Z3_ast_map_to_string
Z3_string Z3_API Z3_ast_map_to_string(Z3_context c, Z3_ast_map m)
Convert the given map into a string.
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 
5052  def __setitem__(self, k, v):
5053  """Add/Update key `k` with value `v`.
5054 
5055  >>> M = AstMap()
5056  >>> x = Int('x')
5057  >>> M[x] = x + 1
5058  >>> len(M)
5059  1
5060  >>> M[x]
5061  x + 1
5062  >>> M[x] = IntVal(1)
5063  >>> M[x]
5064  1
5065  """
5066  Z3_ast_map_insert(self.ctx.ref(), self.map, k.as_ast(), v.as_ast())
z3py.AstMap.__setitem__
def __setitem__
Definition: z3py.py:5051
Z3_ast_map_insert
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 
5071  def erase(self, k):
5072  """Remove the entry associated with key `k`.
5073 
5074  >>> M = AstMap()
5075  >>> x = Int('x')
5076  >>> M[x] = x + 1
5077  >>> len(M)
5078  1
5079  >>> M.erase(x)
5080  >>> len(M)
5081  0
5082  """
5083  Z3_ast_map_erase(self.ctx.ref(), self.map, k.as_ast())
Z3_ast_map_erase
void Z3_API Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k)
Erase a key from the map.
z3py.AstMap.erase
def erase
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 
5100  def keys(self):
5101  """Return an AstVector containing all keys in the map.
5102 
5103  >>> M = AstMap()
5104  >>> x = Int('x')
5105  >>> M[x] = x + 1
5106  >>> M[x+x] = IntVal(1)
5107  >>> M.keys()
5108  [x, x + x]
5109  """
5110  return AstVector(Z3_ast_map_keys(self.ctx.ref(), self.map), self.ctx)
Z3_ast_map_keys
Z3_ast_vector Z3_API Z3_ast_map_keys(Z3_context c, Z3_ast_map m)
Return the keys stored in the given map.
z3py.AstMap.keys
def keys
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 
5085  def reset(self):
5086  """Remove all entries from the map.
5087 
5088  >>> M = AstMap()
5089  >>> x = Int('x')
5090  >>> M[x] = x + 1
5091  >>> M[x+x] = IntVal(1)
5092  >>> len(M)
5093  2
5094  >>> M.reset()
5095  >>> len(M)
5096  0
5097  """
5098  Z3_ast_map_reset(self.ctx.ref(), self.map)
z3py.AstMap.reset
def reset
Definition: z3py.py:5084
Z3_ast_map_reset
void Z3_API Z3_ast_map_reset(Z3_context c, Z3_ast_map m)
Remove all keys from the given map.

Field Documentation

ctx

Definition at line 5002 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), AstMap.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().

map

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

Generated on Fri Apr 12 2019 11:38:54 for Z3 by   doxygen 1.8.5