21 using System.Diagnostics.Contracts;
28 internal class ASTVector : Z3Object
35 get {
return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); }
44 public AST
this[uint i]
48 Contract.Ensures(Contract.Result<AST>() != null);
50 return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
54 Contract.Requires(value != null);
56 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
64 public void Resize(uint newSize)
66 Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
74 public void Push(AST a)
76 Contract.Requires(a != null);
78 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
86 public ASTVector Translate(Context ctx)
88 Contract.Requires(ctx != null);
89 Contract.Ensures(Contract.Result<ASTVector>() != null);
91 return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
97 public override string ToString()
99 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
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); }
108 public override void IncRef(Context ctx, IntPtr obj)
110 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
113 public override void DecRef(Context ctx, IntPtr obj)
115 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
119 internal override void IncRef(IntPtr o)
121 Context.ASTVector_DRQ.IncAndClear(Context, o);
125 internal override void DecRef(IntPtr o)
127 Context.ASTVector_DRQ.Add(o);
Z3_ast_vector Z3_API Z3_mk_ast_vector(__in Z3_context c)
Return an empty AST vector.