Z3
Public Member Functions | Data Fields
AstVector Class Reference
+ Inheritance diagram for AstVector:

Public Member Functions

def __init__
 
def __del__ (self)
 
def __len__ (self)
 
def __getitem__ (self, i)
 
def __setitem__ (self, i, v)
 
def push (self, v)
 
def resize (self, sz)
 
def __contains__ (self, item)
 
def translate (self, other_ctx)
 
def __copy__ (self)
 
def __deepcopy__
 
def __repr__ (self)
 
def sexpr (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 vector
 
 ctx
 

Detailed Description

A collection (vector) of ASTs.

Definition at line 5901 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 5904 of file z3py.py.

5904  def __init__(self, v=None, ctx=None):
5905  self.vector = None
5906  if v is None:
5907  self.ctx = _get_ctx(ctx)
5908  self.vector = Z3_mk_ast_vector(self.ctx.ref())
5909  else:
5910  self.vector = v
5911  assert ctx is not None
5912  self.ctx = ctx
5913  Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
5914 
void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v)
Increment the reference counter of the given AST vector.
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.
def __init__
Definition: z3py.py:5904
def __del__ (   self)

Definition at line 5915 of file z3py.py.

5915  def __del__(self):
5916  if self.vector is not None and self.ctx.ref() is not None and Z3_ast_vector_dec_ref is not None:
5917  Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
5918 
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.
def __del__(self)
Definition: z3py.py:5915

Member Function Documentation

def __contains__ (   self,
  item 
)
Return `True` if the vector contains `item`.

>>> x = Int('x')
>>> A = AstVector()
>>> x in A
False
>>> A.push(x)
>>> x in A
True
>>> (x+1) in A
False
>>> A.push(x+1)
>>> (x+1) in A
True
>>> A
[x, x + 1]

Definition at line 6002 of file z3py.py.

6002  def __contains__(self, item):
6003  """Return `True` if the vector contains `item`.
6004 
6005  >>> x = Int('x')
6006  >>> A = AstVector()
6007  >>> x in A
6008  False
6009  >>> A.push(x)
6010  >>> x in A
6011  True
6012  >>> (x+1) in A
6013  False
6014  >>> A.push(x+1)
6015  >>> (x+1) in A
6016  True
6017  >>> A
6018  [x, x + 1]
6019  """
6020  for elem in self:
6021  if elem.eq(item):
6022  return True
6023  return False
6024 
def __contains__(self, item)
Definition: z3py.py:6002
def __copy__ (   self)

Definition at line 6041 of file z3py.py.

6041  def __copy__(self):
6042  return self.translate(self.ctx)
6043 
def translate(self, other_ctx)
Definition: z3py.py:6025
def __copy__(self)
Definition: z3py.py:6041
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6044 of file z3py.py.

6044  def __deepcopy__(self, memo={}):
6045  return self.translate(self.ctx)
6046 
def translate(self, other_ctx)
Definition: z3py.py:6025
def __deepcopy__
Definition: z3py.py:6044
def __getitem__ (   self,
  i 
)
Return the AST at position `i`.

>>> A = AstVector()
>>> A.push(Int('x') + 1)
>>> A.push(Int('y'))
>>> A[0]
x + 1
>>> A[1]
y

Definition at line 5932 of file z3py.py.

5932  def __getitem__(self, i):
5933  """Return the AST at position `i`.
5934 
5935  >>> A = AstVector()
5936  >>> A.push(Int('x') + 1)
5937  >>> A.push(Int('y'))
5938  >>> A[0]
5939  x + 1
5940  >>> A[1]
5941  y
5942  """
5943 
5944  if isinstance(i, int):
5945  if i < 0:
5946  i += self.__len__()
5947 
5948  if i >= self.__len__():
5949  raise IndexError
5950  return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
5951 
5952  elif isinstance(i, slice):
5953  result = []
5954  for ii in range(*i.indices(self.__len__())):
5955  result.append(_to_ast_ref(
5956  Z3_ast_vector_get(self.ctx.ref(), self.vector, ii),
5957  self.ctx,
5958  ))
5959  return result
5960 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i)
Return the AST at position i in the AST vector v.
def __len__(self)
Definition: z3py.py:5919
def __getitem__(self, i)
Definition: z3py.py:5932
def __len__ (   self)
Return the size of the vector `self`.

>>> A = AstVector()
>>> len(A)
0
>>> A.push(Int('x'))
>>> A.push(Int('x'))
>>> len(A)
2

Definition at line 5919 of file z3py.py.

Referenced by AstVector.__getitem__().

5919  def __len__(self):
5920  """Return the size of the vector `self`.
5921 
5922  >>> A = AstVector()
5923  >>> len(A)
5924  0
5925  >>> A.push(Int('x'))
5926  >>> A.push(Int('x'))
5927  >>> len(A)
5928  2
5929  """
5930  return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
5931 
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.
def __len__(self)
Definition: z3py.py:5919
def __repr__ (   self)

Definition at line 6047 of file z3py.py.

6047  def __repr__(self):
6048  return obj_to_string(self)
6049 
def __repr__(self)
Definition: z3py.py:6047
def __setitem__ (   self,
  i,
  v 
)
Update AST at position `i`.

>>> A = AstVector()
>>> A.push(Int('x') + 1)
>>> A.push(Int('y'))
>>> A[0]
x + 1
>>> A[0] = Int('x')
>>> A[0]
x

Definition at line 5961 of file z3py.py.

5961  def __setitem__(self, i, v):
5962  """Update AST at position `i`.
5963 
5964  >>> A = AstVector()
5965  >>> A.push(Int('x') + 1)
5966  >>> A.push(Int('y'))
5967  >>> A[0]
5968  x + 1
5969  >>> A[0] = Int('x')
5970  >>> A[0]
5971  x
5972  """
5973  if i >= self.__len__():
5974  raise IndexError
5975  Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
5976 
def __len__(self)
Definition: z3py.py:5919
def __setitem__(self, i, v)
Definition: z3py.py:5961
void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a)
Update position i of the AST vector v with the AST a.
def push (   self,
  v 
)
Add `v` in the end of the vector.

>>> A = AstVector()
>>> len(A)
0
>>> A.push(Int('x'))
>>> len(A)
1

Definition at line 5977 of file z3py.py.

5977  def push(self, v):
5978  """Add `v` in the end of the vector.
5979 
5980  >>> A = AstVector()
5981  >>> len(A)
5982  0
5983  >>> A.push(Int('x'))
5984  >>> len(A)
5985  1
5986  """
5987  Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
5988 
def push(self, v)
Definition: z3py.py:5977
void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a)
Add the AST a in the end of the AST vector v. The size of v is increased by one.
def resize (   self,
  sz 
)
Resize the vector to `sz` elements.

>>> A = AstVector()
>>> A.resize(10)
>>> len(A)
10
>>> for i in range(10): A[i] = Int('x')
>>> A[5]
x

Definition at line 5989 of file z3py.py.

5989  def resize(self, sz):
5990  """Resize the vector to `sz` elements.
5991 
5992  >>> A = AstVector()
5993  >>> A.resize(10)
5994  >>> len(A)
5995  10
5996  >>> for i in range(10): A[i] = Int('x')
5997  >>> A[5]
5998  x
5999  """
6000  Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
6001 
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.
def resize(self, sz)
Definition: z3py.py:5989
def sexpr (   self)
Return a textual representation of the s-expression representing the vector.

Definition at line 6050 of file z3py.py.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

6050  def sexpr(self):
6051  """Return a textual representation of the s-expression representing the vector."""
6052  return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
6053 
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.
def sexpr(self)
Definition: z3py.py:6050
def translate (   self,
  other_ctx 
)
Copy vector `self` to context `other_ctx`.

>>> x = Int('x')
>>> A = AstVector()
>>> A.push(x)
>>> c2 = Context()
>>> B = A.translate(c2)
>>> B
[x]

Definition at line 6025 of file z3py.py.

Referenced by AstVector.__copy__(), and AstVector.__deepcopy__().

6025  def translate(self, other_ctx):
6026  """Copy vector `self` to context `other_ctx`.
6027 
6028  >>> x = Int('x')
6029  >>> A = AstVector()
6030  >>> A.push(x)
6031  >>> c2 = Context()
6032  >>> B = A.translate(c2)
6033  >>> B
6034  [x]
6035  """
6036  return AstVector(
6037  Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()),
6038  ctx=other_ctx,
6039  )
6040 
def translate(self, other_ctx)
Definition: z3py.py:6025
Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t)
Translate the AST vector v from context s into an AST vector in context t.

Field Documentation

ctx
vector