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 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 }