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);
103 internal ASTVector(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
104 internal ASTVector(Context ctx) : base(ctx, Native.
Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
106 internal class DecRefQueue : IDecRefQueue
108 public DecRefQueue() : base() { }
109 public DecRefQueue(uint move_limit) : base(move_limit) { }
110 internal override void IncRef(Context ctx, IntPtr obj)
112 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
115 internal override void DecRef(Context ctx, IntPtr obj)
117 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
121 internal override void IncRef(IntPtr o)
123 Context.ASTVector_DRQ.IncAndClear(Context, o);
127 internal override void DecRef(IntPtr o)
129 Context.ASTVector_DRQ.Add(o);
static Z3_ast Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, uint a2)
override string ToString()
Retrieves a string representation of the vector.
void Resize(uint newSize)
Resize the vector to newSize .
ASTVector Translate(Context ctx)
Translates all ASTs in the vector to ctx .
static void Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2)
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)
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.
The abstract syntax tree (AST) class.
static uint Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
static string Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1)
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.