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);
74 private IntPtr m_n_obj = IntPtr.Zero;
78 Contract.Requires(ctx != null);
80 Interlocked.Increment(ref ctx.refCount);
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;
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.
The main interaction with Z3 happens via the Context.
Internal base class for interfacing with native Z3 objects. Should not be used externally.