Z3
ASTVector.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  ASTVector.cs
7 
8 Abstract:
9 
10  Z3 Managed API: AST Vectors
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace 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  Contract.Ensures(Contract.Result<AST>() != null);
49 
50  return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
51  }
52  set
53  {
54  Contract.Requires(value != null);
55 
56  Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
57  }
58  }
59 
64  public void Resize(uint newSize)
65  {
66  Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
67  }
68 
74  public void Push(AST a)
75  {
76  Contract.Requires(a != null);
77 
78  Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
79  }
80 
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  }
93 
97  public override string ToString()
98  {
99  return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
100  }
101 
105  public AST[] ToArray()
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  }
113 
117  public Expr[] ToExprArray()
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  }
125 
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  }
137 
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  }
149 
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  }
161 
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  }
173 
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  }
185 
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  }
197 
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  }
209 
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  }
221 
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  }
233 
234  #region Internal
235  internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
236  internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
237 
238  internal class DecRefQueue : IDecRefQueue
239  {
240  public DecRefQueue() : base() { }
241  public DecRefQueue(uint move_limit) : base(move_limit) { }
242  internal override void IncRef(Context ctx, IntPtr obj)
243  {
244  Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
245  }
246 
247  internal override void DecRef(Context ctx, IntPtr obj)
248  {
249  Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
250  }
251  };
252 
253  internal override void IncRef(IntPtr o)
254  {
255  Context.ASTVector_DRQ.IncAndClear(Context, o);
256  base.IncRef(o);
257  }
258 
259  internal override void DecRef(IntPtr o)
260  {
261  Context.ASTVector_DRQ.Add(o);
262  base.DecRef(o);
263  }
264  #endregion
265  }
266 }
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
Definition: Context.cs:4893
override string ToString()
Retrieves a string representation of the vector.
Definition: ASTVector.cs:97
void Resize(uint newSize)
Resize the vector to newSize .
Definition: ASTVector.cs:64
FPRMExpr [] ToFPRMExprArray()
Translates an ASTVector into a FPRMExpr[]
Definition: ASTVector.cs:201
Boolean expressions
Definition: BoolExpr.cs:31
ArrayExpr [] ToArrayExprArray()
Translates an ASTVector into a ArrayExpr[]
Definition: ASTVector.cs:165
ASTVector Translate(Context ctx)
Translates all ASTs in the vector to ctx .
Definition: ASTVector.cs:86
RealExpr [] ToRealExprArray()
Translates an ASTVector into a RealExpr[]
Definition: ASTVector.cs:225
Vectors of ASTs.
Definition: ASTVector.cs:28
Expressions are terms.
Definition: Expr.cs:29
Bit-vector expressions
Definition: BitVecExpr.cs:31
FloatingPoint Expressions
Definition: FPExpr.cs:31
Array expressions
Definition: ArrayExpr.cs:31
ArithExpr [] ToArithExprArray()
Translates an ASTVector into a ArithExpr[]
Definition: ASTVector.cs:153
Datatype expressions
Definition: DatatypeExpr.cs:31
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
IntExpr [] ToIntExprArray()
Translates an ASTVector into a IntExpr[]
Definition: ASTVector.cs:213
DecRefQueue interface
Definition: IDecRefQueue.cs:32
BitVecExpr [] ToBitVecExprArray()
Translates an ASTVector into a BitVecExpr[]
Definition: ASTVector.cs:141
void Push(AST a)
Add the AST a to the back of the vector. The size is increased by 1.
Definition: ASTVector.cs:74
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
The abstract syntax tree (AST) class.
Definition: AST.cs:31
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
FPExpr [] ToFPExprArray()
Translates an ASTVector into a FPExpr[]
Definition: ASTVector.cs:189
DatatypeExpr [] ToDatatypeExprArray()
Translates an ASTVector into a DatatypeExpr[]
Definition: ASTVector.cs:177
Expr [] ToExprArray()
Translates an ASTVector into an Expr[]
Definition: ASTVector.cs:117
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Int expressions
Definition: IntExpr.cs:31
AST [] ToArray()
Translates an AST vector into an AST[]
Definition: ASTVector.cs:105
Real expressions
Definition: RealExpr.cs:31