Z3
ASTVector.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 ASTVector.cs
7
8Abstract:
9
10 Z3 Managed API: AST Vectors
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
28 public class ASTVector : Z3Object
29 {
33 public uint Size
34 {
35 get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); }
36 }
37
44 public AST this[uint i]
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 }
58
63 public void Resize(uint newSize)
64 {
65 Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
66 }
67
73 public void Push(AST a)
74 {
75 Debug.Assert(a != null);
76
77 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
78 }
79
86 {
87 Debug.Assert(ctx != null);
88
89 return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
90 }
91
95 public override string ToString()
96 {
97 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
98 }
99
103 public AST[] ToArray()
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 }
111
115 public Expr[] ToExprArray()
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 }
123
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 }
135
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 }
147
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 }
159
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 }
171
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 }
183
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 }
195
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 }
207
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 }
219
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 }
231
232 #region Internal
233 internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
234 internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Debug.Assert(ctx != null); }
235
236 internal class DecRefQueue : IDecRefQueue
237 {
238 public DecRefQueue() : base() { }
239 public DecRefQueue(uint move_limit) : base(move_limit) { }
240 internal override void IncRef(Context ctx, IntPtr obj)
241 {
242 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
243 }
244
245 internal override void DecRef(Context ctx, IntPtr obj)
246 {
247 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
248 }
249 };
250
251 internal override void IncRef(IntPtr o)
252 {
253 Context.ASTVector_DRQ.IncAndClear(Context, o);
254 base.IncRef(o);
255 }
256
257 internal override void DecRef(IntPtr o)
258 {
259 Context.ASTVector_DRQ.Add(o);
260 base.DecRef(o);
261 }
262 #endregion
263 }
264}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Vectors of ASTs.
Definition: ASTVector.cs:29
ArithExpr[] ToArithExprArray()
Translates an ASTVector into a ArithExpr[]
Definition: ASTVector.cs:151
ASTVector Translate(Context ctx)
Translates all ASTs in the vector to ctx .
Definition: ASTVector.cs:85
FPExpr[] ToFPExprArray()
Translates an ASTVector into a FPExpr[]
Definition: ASTVector.cs:187
void Resize(uint newSize)
Resize the vector to newSize .
Definition: ASTVector.cs:63
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:127
void Push(AST a)
Add the AST a to the back of the vector. The size is increased by 1.
Definition: ASTVector.cs:73
BitVecExpr[] ToBitVecExprArray()
Translates an ASTVector into a BitVecExpr[]
Definition: ASTVector.cs:139
uint Size
The size of the vector
Definition: ASTVector.cs:34
RealExpr[] ToRealExprArray()
Translates an ASTVector into a RealExpr[]
Definition: ASTVector.cs:223
FPRMExpr[] ToFPRMExprArray()
Translates an ASTVector into a FPRMExpr[]
Definition: ASTVector.cs:199
ArrayExpr[] ToArrayExprArray()
Translates an ASTVector into a ArrayExpr[]
Definition: ASTVector.cs:163
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
Definition: ASTVector.cs:115
override string ToString()
Retrieves a string representation of the vector.
Definition: ASTVector.cs:95
DatatypeExpr[] ToDatatypeExprArray()
Translates an ASTVector into a DatatypeExpr[]
Definition: ASTVector.cs:175
IntExpr[] ToIntExprArray()
Translates an ASTVector into a IntExpr[]
Definition: ASTVector.cs:211
AST[] ToArray()
Translates an AST vector into an AST[]
Definition: ASTVector.cs:103
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:32
Array expressions
Definition: ArrayExpr.cs:32
Bit-vector expressions
Definition: BitVecExpr.cs:32
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4735
Datatype expressions
Definition: DatatypeExpr.cs:32
Expressions are terms.
Definition: Expr.cs:31
FloatingPoint Expressions
Definition: FPExpr.cs:32
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:32
Int expressions
Definition: IntExpr.cs:32
Real expressions
Definition: RealExpr.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.