Z3
src/api/dotnet/Z3Object.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Z3Object.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Internal Z3 Objects
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 using System.Threading;
00023 
00024 namespace Microsoft.Z3
00025 {
00030     [ContractVerification(true)]
00031     public class Z3Object : IDisposable
00032     {
00036         ~Z3Object()
00037         {
00038             Dispose();            
00039         }
00040 
00044         public void Dispose()
00045         {
00046             if (m_n_obj != IntPtr.Zero)
00047             {
00048                 DecRef(m_n_obj);
00049                 m_n_obj = IntPtr.Zero;                
00050             }
00051 
00052             if (m_ctx != null)
00053             {
00054                 if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
00055                     GC.ReRegisterForFinalize(m_ctx);
00056                 m_ctx = null;
00057             }
00058 
00059             GC.SuppressFinalize(this);
00060         }
00061 
00062         #region Object Invariant
00063         
00064         [ContractInvariantMethod]
00065         private void ObjectInvariant()
00066         {
00067             Contract.Invariant(this.m_ctx != null);
00068         }
00069 
00070         #endregion
00071 
00072         #region Internal
00073         private Context m_ctx = null;
00074         private IntPtr m_n_obj = IntPtr.Zero;
00075 
00076         internal Z3Object(Context ctx)
00077         {
00078             Contract.Requires(ctx != null);
00079 
00080             Interlocked.Increment(ref ctx.refCount);
00081             m_ctx = ctx;
00082         }
00083 
00084         internal Z3Object(Context ctx, IntPtr obj)
00085         {
00086             Contract.Requires(ctx != null);
00087 
00088             Interlocked.Increment(ref ctx.refCount);
00089             m_ctx = ctx;
00090             IncRef(obj);
00091             m_n_obj = obj;
00092         }
00093 
00094         internal virtual void IncRef(IntPtr o) { }
00095         internal virtual void DecRef(IntPtr o) { }
00096 
00097         internal virtual void CheckNativeObject(IntPtr obj) { }
00098 
00099         internal virtual IntPtr NativeObject
00100         {
00101             get { return m_n_obj; }
00102             set
00103             {
00104                 if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
00105                 if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
00106                 m_n_obj = value;
00107             }
00108         }
00109 
00110         internal static IntPtr GetNativeObject(Z3Object s)
00111         {
00112             if (s == null) return new IntPtr();
00113             return s.NativeObject;
00114         }
00115 
00116         internal Context Context
00117         {
00118             get 
00119             {
00120                 Contract.Ensures(Contract.Result<Context>() != null);
00121                 return m_ctx; 
00122             }            
00123         }
00124 
00125         [Pure]
00126         internal static IntPtr[] ArrayToNative(Z3Object[] a)
00127         {
00128             Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
00129             Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Length);
00130 
00131             if (a == null) return null;
00132             IntPtr[] an = new IntPtr[a.Length];
00133             for (uint i = 0; i < a.Length; i++)
00134                 if (a[i] != null) an[i] = a[i].NativeObject;
00135             return an;
00136         }
00137 
00138         [Pure]
00139         internal static uint ArrayLength(Z3Object[] a)
00140         {
00141             return (a == null)?0:(uint)a.Length;
00142         }
00143         #endregion
00144     }
00145 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines