Z3
 
Loading...
Searching...
No Matches
AstVector Class Reference
+ Inheritance diagram for AstVector:

Public Member Functions

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

Data Fields

 vector = None
 
 ctx = _get_ctx(ctx)
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

A collection (vector) of ASTs.

Definition at line 5936 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 5939 of file z3py.py.

5939 def __init__(self, v=None, ctx=None):
5940 self.vector = None
5941 if v is None:
5942 self.ctx = _get_ctx(ctx)
5943 self.vector = Z3_mk_ast_vector(self.ctx.ref())
5944 else:
5945 self.vector = v
5946 assert ctx is not None
5947 self.ctx = ctx
5948 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
5949
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.

◆ __del__()

__del__ ( self)

Definition at line 5950 of file z3py.py.

5950 def __del__(self):
5951 if self.vector is not None and self.ctx.ref() is not None and Z3_ast_vector_dec_ref is not None:
5952 Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
5953
void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v)
Decrement the reference counter of the given AST vector.

Member Function Documentation

◆ __contains__()

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

6037 def __contains__(self, item):
6038 """Return `True` if the vector contains `item`.
6039
6040 >>> x = Int('x')
6041 >>> A = AstVector()
6042 >>> x in A
6043 False
6044 >>> A.push(x)
6045 >>> x in A
6046 True
6047 >>> (x+1) in A
6048 False
6049 >>> A.push(x+1)
6050 >>> (x+1) in A
6051 True
6052 >>> A
6053 [x, x + 1]
6054 """
6055 for elem in self:
6056 if elem.eq(item):
6057 return True
6058 return False
6059

◆ __copy__()

__copy__ ( self)

Definition at line 6076 of file z3py.py.

6076 def __copy__(self):
6077 return self.translate(self.ctx)
6078

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6079 of file z3py.py.

6079 def __deepcopy__(self, memo={}):
6080 return self.translate(self.ctx)
6081

◆ __getitem__()

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

5967 def __getitem__(self, i):
5968 """Return the AST at position `i`.
5969
5970 >>> A = AstVector()
5971 >>> A.push(Int('x') + 1)
5972 >>> A.push(Int('y'))
5973 >>> A[0]
5974 x + 1
5975 >>> A[1]
5976 y
5977 """
5978
5979 if isinstance(i, int):
5980 if i < 0:
5981 i += self.__len__()
5982
5983 if i >= self.__len__():
5984 raise IndexError
5985 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
5986
5987 elif isinstance(i, slice):
5988 result = []
5989 for ii in range(*i.indices(self.__len__())):
5990 result.append(_to_ast_ref(
5991 Z3_ast_vector_get(self.ctx.ref(), self.vector, ii),
5992 self.ctx,
5993 ))
5994 return result
5995
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.

◆ __len__()

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

5954 def __len__(self):
5955 """Return the size of the vector `self`.
5956
5957 >>> A = AstVector()
5958 >>> len(A)
5959 0
5960 >>> A.push(Int('x'))
5961 >>> A.push(Int('x'))
5962 >>> len(A)
5963 2
5964 """
5965 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
5966
unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v)
Return the size of the given AST vector.

Referenced by __getitem__(), and __setitem__().

◆ __repr__()

__repr__ ( self)

Definition at line 6082 of file z3py.py.

6082 def __repr__(self):
6083 return obj_to_string(self)
6084

◆ __setitem__()

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

5996 def __setitem__(self, i, v):
5997 """Update AST at position `i`.
5998
5999 >>> A = AstVector()
6000 >>> A.push(Int('x') + 1)
6001 >>> A.push(Int('y'))
6002 >>> A[0]
6003 x + 1
6004 >>> A[0] = Int('x')
6005 >>> A[0]
6006 x
6007 """
6008 if i >= self.__len__():
6009 raise IndexError
6010 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
6011
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.

◆ push()

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

6012 def push(self, v):
6013 """Add `v` in the end of the vector.
6014
6015 >>> A = AstVector()
6016 >>> len(A)
6017 0
6018 >>> A.push(Int('x'))
6019 >>> len(A)
6020 1
6021 """
6022 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
6023
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.

Referenced by Solver.__enter__().

◆ resize()

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

6024 def resize(self, sz):
6025 """Resize the vector to `sz` elements.
6026
6027 >>> A = AstVector()
6028 >>> A.resize(10)
6029 >>> len(A)
6030 10
6031 >>> for i in range(10): A[i] = Int('x')
6032 >>> A[5]
6033 x
6034 """
6035 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
6036
void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n)
Resize the AST vector v.

◆ sexpr()

sexpr ( self)
Return a textual representation of the s-expression representing the vector.

Definition at line 6085 of file z3py.py.

6085 def sexpr(self):
6086 """Return a textual representation of the s-expression representing the vector."""
6087 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
6088
Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v)
Convert AST vector into a string.

◆ translate()

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

6060 def translate(self, other_ctx):
6061 """Copy vector `self` to context `other_ctx`.
6062
6063 >>> x = Int('x')
6064 >>> A = AstVector()
6065 >>> A.push(x)
6066 >>> c2 = Context()
6067 >>> B = A.translate(c2)
6068 >>> B
6069 [x]
6070 """
6071 return AstVector(
6072 Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()),
6073 ctx=other_ctx,
6074 )
6075
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.

Referenced by __copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), __deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().

Field Documentation

◆ ctx

◆ vector

vector = None

Definition at line 5940 of file z3py.py.

Referenced by __del__(), __getitem__(), __len__(), __setitem__(), push(), resize(), sexpr(), and translate().