20using System.Diagnostics;
35 get {
return Native.Z3_ast_vector_size(
Context.nCtx, NativeObject); }
44 public AST this[uint i]
53 Debug.Assert(value !=
null);
55 Native.Z3_ast_vector_set(
Context.nCtx, NativeObject, i, value.NativeObject);
65 Native.Z3_ast_vector_resize(
Context.nCtx, NativeObject, newSize);
75 Debug.Assert(a !=
null);
77 Native.Z3_ast_vector_push(
Context.nCtx, NativeObject, a.NativeObject);
87 Debug.Assert(ctx !=
null);
97 return Native.Z3_ast_vector_to_string(
Context.nCtx, NativeObject);
107 for (uint i = 0; i < n; i++)
108 res[i] =
AST.Create(
this.Context,
this[i].NativeObject);
119 for (uint i = 0; i < n; i++)
120 res[i] =
Expr.Create(
this.Context,
this[i].NativeObject);
131 for (uint i = 0; i < n; i++)
143 for (uint i = 0; i < n; i++)
155 for (uint i = 0; i < n; i++)
167 for (uint i = 0; i < n; i++)
179 for (uint i = 0; i < n; i++)
191 for (uint i = 0; i < n; i++)
203 for (uint i = 0; i < n; i++)
215 for (uint i = 0; i < n; i++)
227 for (uint i = 0; i < n; i++)
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); }
236 internal class DecRefQueue : IDecRefQueue
238 public DecRefQueue() : base() { }
239 public DecRefQueue(uint move_limit) : base(move_limit) { }
240 internal override void IncRef(Context ctx, IntPtr obj)
242 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
245 internal override void DecRef(Context ctx, IntPtr obj)
247 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
251 internal override void IncRef(IntPtr o)
257 internal override void DecRef(IntPtr o)
The abstract syntax tree (AST) class.
ArithExpr[] ToArithExprArray()
Translates an ASTVector into a ArithExpr[]
ASTVector Translate(Context ctx)
Translates all ASTs in the vector to ctx .
FPExpr[] ToFPExprArray()
Translates an ASTVector into a FPExpr[]
void Resize(uint newSize)
Resize the vector to newSize .
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
void Push(AST a)
Add the AST a to the back of the vector. The size is increased by 1.
BitVecExpr[] ToBitVecExprArray()
Translates an ASTVector into a BitVecExpr[]
uint Size
The size of the vector
RealExpr[] ToRealExprArray()
Translates an ASTVector into a RealExpr[]
FPRMExpr[] ToFPRMExprArray()
Translates an ASTVector into a FPRMExpr[]
ArrayExpr[] ToArrayExprArray()
Translates an ASTVector into a ArrayExpr[]
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
override string ToString()
Retrieves a string representation of the vector.
DatatypeExpr[] ToDatatypeExprArray()
Translates an ASTVector into a DatatypeExpr[]
IntExpr[] ToIntExprArray()
Translates an ASTVector into a IntExpr[]
AST[] ToArray()
Translates an AST vector into an AST[]
Arithmetic expressions (int/real)
The main interaction with Z3 happens via the Context.
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
FloatingPoint Expressions
FloatingPoint RoundingMode Expressions
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c)
Return an empty AST vector.