Z3
src/api/dotnet/ASTVector.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     ASTVector.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: AST Vectors
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines