35 get {
return Native.Z3_ast_vector_size(
Context.nCtx, NativeObject); }
44 public AST this[uint i]
48 Contract.Ensures(Contract.Result<
AST>() != null);
54 Contract.Requires(value != null);
56 Native.Z3_ast_vector_set(
Context.nCtx, NativeObject, i, value.NativeObject);
66 Native.Z3_ast_vector_resize(
Context.nCtx, NativeObject, newSize);
76 Contract.Requires(a != null);
78 Native.Z3_ast_vector_push(
Context.nCtx, NativeObject, a.NativeObject);
88 Contract.Requires(ctx != null);
89 Contract.Ensures(Contract.Result<
ASTVector>() != null);
99 return Native.Z3_ast_vector_to_string(
Context.nCtx, NativeObject);
109 for (uint i = 0; i < n; i++)
110 res[i] =
AST.Create(
this.Context,
this[i].NativeObject);
121 for (uint i = 0; i < n; i++)
122 res[i] =
Expr.Create(
this.Context,
this[i].NativeObject);
133 for (uint i = 0; i < n; i++)
145 for (uint i = 0; i < n; i++)
157 for (uint i = 0; i < n; i++)
169 for (uint i = 0; i < n; i++)
181 for (uint i = 0; i < n; i++)
193 for (uint i = 0; i < n; i++)
205 for (uint i = 0; i < n; i++)
217 for (uint i = 0; i < n; i++)
229 for (uint i = 0; i < n; i++)
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); }
240 public DecRefQueue() : base() { }
241 public DecRefQueue(uint move_limit) : base(move_limit) { }
242 internal override void IncRef(
Context ctx, IntPtr obj)
244 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
247 internal override void DecRef(
Context ctx, IntPtr obj)
249 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
253 internal override void IncRef(IntPtr o)
259 internal override void DecRef(IntPtr o)
IDecRefQueue ASTVector_DRQ
ASTVector DRQ
override string ToString()
Retrieves a string representation of the vector.
void Resize(uint newSize)
Resize the vector to newSize .
FPRMExpr [] ToFPRMExprArray()
Translates an ASTVector into a FPRMExpr[]
ArrayExpr [] ToArrayExprArray()
Translates an ASTVector into a ArrayExpr[]
ASTVector Translate(Context ctx)
Translates all ASTs in the vector to ctx .
RealExpr [] ToRealExprArray()
Translates an ASTVector into a RealExpr[]
FloatingPoint Expressions
ArithExpr [] ToArithExprArray()
Translates an ASTVector into a ArithExpr[]
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
IntExpr [] ToIntExprArray()
Translates an ASTVector into a IntExpr[]
BitVecExpr [] ToBitVecExprArray()
Translates an ASTVector into a BitVecExpr[]
void Push(AST a)
Add the AST a to the back of the vector. The size is increased by 1.
The main interaction with Z3 happens via the Context.
Arithmetic expressions (int/real)
The abstract syntax tree (AST) class.
FloatingPoint RoundingMode Expressions
FPExpr [] ToFPExprArray()
Translates an ASTVector into a FPExpr[]
DatatypeExpr [] ToDatatypeExprArray()
Translates an ASTVector into a DatatypeExpr[]
Expr [] ToExprArray()
Translates an ASTVector into an Expr[]
Internal base class for interfacing with native Z3 objects. Should not be used externally.
AST [] ToArray()
Translates an AST vector into an AST[]