21 using System.Diagnostics.Contracts;
30 [ContractVerification(
true)]
46 if (m_n_obj != IntPtr.Zero)
49 m_n_obj = IntPtr.Zero;
54 if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
55 GC.ReRegisterForFinalize(m_ctx);
59 GC.SuppressFinalize(
this);
62 #region Object Invariant
64 [ContractInvariantMethod]
65 private void ObjectInvariant()
67 Contract.Invariant(this.m_ctx != null);
73 private Context m_ctx = null;
74 private IntPtr m_n_obj = IntPtr.Zero;
76 internal Z3Object(Context ctx)
78 Contract.Requires(ctx != null);
80 Interlocked.Increment(ref ctx.refCount);
84 internal Z3Object(Context ctx, IntPtr obj)
86 Contract.Requires(ctx != null);
88 Interlocked.Increment(ref ctx.refCount);
94 internal virtual void IncRef(IntPtr o) { }
95 internal virtual void DecRef(IntPtr o) { }
97 internal virtual void CheckNativeObject(IntPtr obj) { }
99 internal virtual IntPtr NativeObject
101 get {
return m_n_obj; }
104 if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
105 if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
110 internal static IntPtr GetNativeObject(Z3Object s)
112 if (s == null)
return new IntPtr();
113 return s.NativeObject;
116 internal Context Context
120 Contract.Ensures(Contract.Result<Context>() != null);
126 internal static IntPtr[] ArrayToNative(Z3Object[] a)
128 Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
129 Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Length);
131 if (a == null)
return null;
132 IntPtr[] an =
new IntPtr[a.Length];
133 for (uint i = 0; i < a.Length; i++)
134 if (a[i] != null) an[i] = a[i].NativeObject;
139 internal static uint ArrayLength(Z3Object[] a)
141 return (a == null)?0:(uint)a.Length;
void Dispose()
Disposes of the underlying native Z3 object.
Internal base class for interfacing with native Z3 objects. Should not be used externally.