Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 internal class ASTVector : Z3Object
00029 {
00033 public uint Size
00034 {
00035 get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); }
00036 }
00037
00044 public AST this[uint i]
00045 {
00046 get
00047 {
00048 Contract.Ensures(Contract.Result<AST>() != null);
00049
00050 return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
00051 }
00052 set
00053 {
00054 Contract.Requires(value != null);
00055
00056 Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
00057 }
00058 }
00059
00064 public void Resize(uint newSize)
00065 {
00066 Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
00067 }
00068
00074 public void Push(AST a)
00075 {
00076 Contract.Requires(a != null);
00077
00078 Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
00079 }
00080
00086 public ASTVector Translate(Context ctx)
00087 {
00088 Contract.Requires(ctx != null);
00089 Contract.Ensures(Contract.Result<ASTVector>() != null);
00090
00091 return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
00092 }
00093
00097 public override string ToString()
00098 {
00099 return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
00100 }
00101
00102 #region Internal
00103 internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00104 internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
00105
00106 internal class DecRefQueue : IDecRefQueue
00107 {
00108 public override void IncRef(Context ctx, IntPtr obj)
00109 {
00110 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
00111 }
00112
00113 public override void DecRef(Context ctx, IntPtr obj)
00114 {
00115 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
00116 }
00117 };
00118
00119 internal override void IncRef(IntPtr o)
00120 {
00121 Context.ASTVector_DRQ.IncAndClear(Context, o);
00122 base.IncRef(o);
00123 }
00124
00125 internal override void DecRef(IntPtr o)
00126 {
00127 Context.ASTVector_DRQ.Add(o);
00128 base.DecRef(o);
00129 }
00130 #endregion
00131 }
00132 }