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 73 of file ASTVector.cs.

74 {
75 Debug.Assert(a != null);
76
77 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
78 }

◆ Resize()

void Resize ( uint  newSize)
inline

Resize the vector to newSize .

Parameters
newSizeThe new size of the vector.

Definition at line 63 of file ASTVector.cs.

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

◆ ToArithExprArray()

ArithExpr[] ToArithExprArray ( )
inline

Translates an ASTVector into a ArithExpr[]


Definition at line 151 of file ASTVector.cs.

152 {
153 uint n = Size;
154 ArithExpr[] res = new ArithExpr[n];
155 for (uint i = 0; i < n; i++)
156 res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
157 return res;
158 }
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 103 of file ASTVector.cs.

104 {
105 uint n = Size;
106 AST[] res = new AST[n];
107 for (uint i = 0; i < n; i++)
108 res[i] = AST.Create(this.Context, this[i].NativeObject);
109 return res;
110 }

◆ ToArrayExprArray()

ArrayExpr[] ToArrayExprArray ( )
inline

Translates an ASTVector into a ArrayExpr[]


Definition at line 163 of file ASTVector.cs.

164 {
165 uint n = Size;
166 ArrayExpr[] res = new ArrayExpr[n];
167 for (uint i = 0; i < n; i++)
168 res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
169 return res;
170 }

◆ ToBitVecExprArray()

BitVecExpr[] ToBitVecExprArray ( )
inline

Translates an ASTVector into a BitVecExpr[]


Definition at line 139 of file ASTVector.cs.

140 {
141 uint n = Size;
142 BitVecExpr[] res = new BitVecExpr[n];
143 for (uint i = 0; i < n; i++)
144 res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
145 return res;
146 }

◆ ToBoolExprArray()

BoolExpr[] ToBoolExprArray ( )
inline

Translates an ASTVector into a BoolExpr[]


Definition at line 127 of file ASTVector.cs.

128 {
129 uint n = Size;
130 BoolExpr[] res = new BoolExpr[n];
131 for (uint i = 0; i < n; i++)
132 res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
133 return res;
134 }

Referenced by Solver.Cube(), Fixedpoint.ParseFile(), Context.ParseSMTLIB2File(), Context.ParseSMTLIB2String(), and Fixedpoint.ParseString().

◆ ToDatatypeExprArray()

DatatypeExpr[] ToDatatypeExprArray ( )
inline

Translates an ASTVector into a DatatypeExpr[]


Definition at line 175 of file ASTVector.cs.

176 {
177 uint n = Size;
178 DatatypeExpr[] res = new DatatypeExpr[n];
179 for (uint i = 0; i < n; i++)
180 res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
181 return res;
182 }

◆ ToExprArray()

Expr[] ToExprArray ( )
inline

Translates an ASTVector into an Expr[]


Definition at line 115 of file ASTVector.cs.

116 {
117 uint n = Size;
118 Expr[] res = new Expr[n];
119 for (uint i = 0; i < n; i++)
120 res[i] = Expr.Create(this.Context, this[i].NativeObject);
121 return res;
122 }

Referenced by Model.SortUniverse().

◆ ToFPExprArray()

FPExpr[] ToFPExprArray ( )
inline

Translates an ASTVector into a FPExpr[]


Definition at line 187 of file ASTVector.cs.

188 {
189 uint n = Size;
190 FPExpr[] res = new FPExpr[n];
191 for (uint i = 0; i < n; i++)
192 res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
193 return res;
194 }

◆ ToFPRMExprArray()

FPRMExpr[] ToFPRMExprArray ( )
inline

Translates an ASTVector into a FPRMExpr[]


Definition at line 199 of file ASTVector.cs.

200 {
201 uint n = Size;
202 FPRMExpr[] res = new FPRMExpr[n];
203 for (uint i = 0; i < n; i++)
204 res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
205 return res;
206 }

◆ ToIntExprArray()

IntExpr[] ToIntExprArray ( )
inline

Translates an ASTVector into a IntExpr[]


Definition at line 211 of file ASTVector.cs.

212 {
213 uint n = Size;
214 IntExpr[] res = new IntExpr[n];
215 for (uint i = 0; i < n; i++)
216 res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
217 return res;
218 }

◆ ToRealExprArray()

RealExpr[] ToRealExprArray ( )
inline

Translates an ASTVector into a RealExpr[]


Definition at line 223 of file ASTVector.cs.

224 {
225 uint n = Size;
226 RealExpr[] res = new RealExpr[n];
227 for (uint i = 0; i < n; i++)
228 res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
229 return res;
230 }

◆ ToString()

override string ToString ( )
inline

Retrieves a string representation of the vector.


Definition at line 95 of file ASTVector.cs.

96 {
97 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
98 }

◆ Translate()

ASTVector Translate ( Context  ctx)
inline

Translates all ASTs in the vector to ctx .

Parameters
ctxA context
Returns
A new ASTVector

Definition at line 85 of file ASTVector.cs.

86 {
87 Debug.Assert(ctx != null);
88
89 return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
90 }

Property Documentation

◆ Size

uint Size
get

◆ 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 44 of file ASTVector.cs.

45 {
46 get
47 {
48
49 return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
50 }
51 set
52 {
53 Debug.Assert(value != null);
54
55 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
56 }
57 }