21 using System.Diagnostics.Contracts;
44 public AST this[uint i]
48 Contract.Ensures(Contract.Result<
AST>() != null);
54 Contract.Requires(value != null);
76 Contract.Requires(a != null);
88 Contract.Requires(ctx != null);
89 Contract.Ensures(Contract.Result<
ASTVector>() != null);
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); }
240 public DecRefQueue() : base() { }
241 public DecRefQueue(uint move_limit) : base(move_limit) { }
242 internal override void IncRef(
Context ctx, IntPtr obj)
247 internal override void DecRef(
Context ctx, IntPtr obj)
253 internal override void IncRef(IntPtr o)
259 internal override void DecRef(IntPtr o)
static Z3_ast Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, uint a2)
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[]
static void Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1)
static void Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1)
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[]
static void Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2)
FloatingPoint Expressions
static void Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, uint a2)
static void Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, uint a2, Z3_ast a3)
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.
static Z3_ast_vector Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2)
The main interaction with Z3 happens via the Context.
Arithmetic expressions (int/real)
The abstract syntax tree (AST) class.
static uint Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1)
static Z3_ast_vector Z3_mk_ast_vector(Z3_context a0)
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[]
static string Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1)