Z3
Data Structures | Public Member Functions | Properties
ASTVector Class Reference

Vectors of ASTs. More...

+ Inheritance diagram for ASTVector:

Data Structures

class  DecRefQueue
 

Public Member Functions

void Resize (uint newSize)
 Resize the vector to newSize . More...
 
void Push (AST a)
 Add the AST a to the back of the vector. The size is increased by 1. More...
 
ASTVector Translate (Context ctx)
 Translates all ASTs in the vector to ctx . More...
 
override string ToString ()
 Retrieves a string representation of the vector. More...
 
AST [] ToArray ()
 Translates an AST vector into an AST[] More...
 
Expr [] ToExprArray ()
 Translates an ASTVector into an Expr[] More...
 
BoolExpr [] ToBoolExprArray ()
 Translates an ASTVector into a BoolExpr[] More...
 
BitVecExpr [] ToBitVecExprArray ()
 Translates an ASTVector into a BitVecExpr[] More...
 
ArithExpr [] ToArithExprArray ()
 Translates an ASTVector into a ArithExpr[] More...
 
ArrayExpr [] ToArrayExprArray ()
 Translates an ASTVector into a ArrayExpr[] More...
 
DatatypeExpr [] ToDatatypeExprArray ()
 Translates an ASTVector into a DatatypeExpr[] More...
 
FPExpr [] ToFPExprArray ()
 Translates an ASTVector into a FPExpr[] More...
 
FPRMExpr [] ToFPRMExprArray ()
 Translates an ASTVector into a FPRMExpr[] More...
 
IntExpr [] ToIntExprArray ()
 Translates an ASTVector into a IntExpr[] More...
 
RealExpr [] ToRealExprArray ()
 Translates an ASTVector into a RealExpr[] More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

uint Size [get]
 The size of the vector More...
 
AST this[uint i] [get, set]
 Retrieves the i-th object in the vector. More...
 

Detailed Description

Vectors of ASTs.

Definition at line 28 of file ASTVector.cs.

Member Function Documentation

§ Push()

void Push ( AST  a)
inline

Add the AST a to the back of the vector. The size is increased by 1.

Parameters
aAn AST

Definition at line 74 of file ASTVector.cs.

75  {
76  Contract.Requires(a != null);
77 
78  Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
79  }

§ Resize()

void Resize ( uint  newSize)
inline

Resize the vector to newSize .

Parameters
newSizeThe new size of the vector.

Definition at line 64 of file ASTVector.cs.

65  {
66  Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
67  }

§ ToArithExprArray()

ArithExpr [] ToArithExprArray ( )
inline

Translates an ASTVector into a ArithExpr[]

Definition at line 153 of file ASTVector.cs.

154  {
155  uint n = Size;
156  ArithExpr[] res = new ArithExpr[n];
157  for (uint i = 0; i < n; i++)
158  res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
159  return res;
160  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToArray()

AST [] ToArray ( )
inline

Translates an AST vector into an AST[]

Definition at line 105 of file ASTVector.cs.

106  {
107  uint n = Size;
108  AST[] res = new AST[n];
109  for (uint i = 0; i < n; i++)
110  res[i] = AST.Create(this.Context, this[i].NativeObject);
111  return res;
112  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToArrayExprArray()

ArrayExpr [] ToArrayExprArray ( )
inline

Translates an ASTVector into a ArrayExpr[]

Definition at line 165 of file ASTVector.cs.

166  {
167  uint n = Size;
168  ArrayExpr[] res = new ArrayExpr[n];
169  for (uint i = 0; i < n; i++)
170  res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
171  return res;
172  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToBitVecExprArray()

BitVecExpr [] ToBitVecExprArray ( )
inline

Translates an ASTVector into a BitVecExpr[]

Definition at line 141 of file ASTVector.cs.

142  {
143  uint n = Size;
144  BitVecExpr[] res = new BitVecExpr[n];
145  for (uint i = 0; i < n; i++)
146  res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
147  return res;
148  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToBoolExprArray()

BoolExpr [] ToBoolExprArray ( )
inline

Translates an ASTVector into a BoolExpr[]

Definition at line 129 of file ASTVector.cs.

Referenced by InterpolationContext.ComputeInterpolant(), InterpolationContext.GetInterpolant(), Fixedpoint.ParseFile(), and Fixedpoint.ParseString().

130  {
131  uint n = Size;
132  BoolExpr[] res = new BoolExpr[n];
133  for (uint i = 0; i < n; i++)
134  res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
135  return res;
136  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToDatatypeExprArray()

DatatypeExpr [] ToDatatypeExprArray ( )
inline

Translates an ASTVector into a DatatypeExpr[]

Definition at line 177 of file ASTVector.cs.

178  {
179  uint n = Size;
180  DatatypeExpr[] res = new DatatypeExpr[n];
181  for (uint i = 0; i < n; i++)
182  res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
183  return res;
184  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToExprArray()

Expr [] ToExprArray ( )
inline

Translates an ASTVector into an Expr[]

Definition at line 117 of file ASTVector.cs.

Referenced by Model.SortUniverse().

118  {
119  uint n = Size;
120  Expr[] res = new Expr[n];
121  for (uint i = 0; i < n; i++)
122  res[i] = Expr.Create(this.Context, this[i].NativeObject);
123  return res;
124  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToFPExprArray()

FPExpr [] ToFPExprArray ( )
inline

Translates an ASTVector into a FPExpr[]

Definition at line 189 of file ASTVector.cs.

190  {
191  uint n = Size;
192  FPExpr[] res = new FPExpr[n];
193  for (uint i = 0; i < n; i++)
194  res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
195  return res;
196  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToFPRMExprArray()

FPRMExpr [] ToFPRMExprArray ( )
inline

Translates an ASTVector into a FPRMExpr[]

Definition at line 201 of file ASTVector.cs.

202  {
203  uint n = Size;
204  FPRMExpr[] res = new FPRMExpr[n];
205  for (uint i = 0; i < n; i++)
206  res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
207  return res;
208  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToIntExprArray()

IntExpr [] ToIntExprArray ( )
inline

Translates an ASTVector into a IntExpr[]

Definition at line 213 of file ASTVector.cs.

214  {
215  uint n = Size;
216  IntExpr[] res = new IntExpr[n];
217  for (uint i = 0; i < n; i++)
218  res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
219  return res;
220  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToRealExprArray()

RealExpr [] ToRealExprArray ( )
inline

Translates an ASTVector into a RealExpr[]

Definition at line 225 of file ASTVector.cs.

226  {
227  uint n = Size;
228  RealExpr[] res = new RealExpr[n];
229  for (uint i = 0; i < n; i++)
230  res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
231  return res;
232  }
uint Size
The size of the vector
Definition: ASTVector.cs:34

§ ToString()

override string ToString ( )
inline

Retrieves a string representation of the vector.

Definition at line 97 of file ASTVector.cs.

98  {
99  return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
100  }

§ Translate()

ASTVector Translate ( Context  ctx)
inline

Translates all ASTs in the vector to ctx .

Parameters
ctxA context
Returns
A new ASTVector

Definition at line 86 of file ASTVector.cs.

87  {
88  Contract.Requires(ctx != null);
89  Contract.Ensures(Contract.Result<ASTVector>() != null);
90 
91  return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
92  }

Property Documentation

§ Size

uint Size
get

The size of the vector

Definition at line 34 of file ASTVector.cs.

§ this[uint i]

AST this[uint i]
getset

Retrieves the i-th object in the vector.

May throw an IndexOutOfBoundsException when i is out of range.

Parameters
iIndex
Returns
An AST

Definition at line 45 of file ASTVector.cs.