23 using System.Collections.Generic;
48 if (m_n_obj != IntPtr.Zero)
51 m_n_obj = IntPtr.Zero;
56 if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
57 GC.ReRegisterForFinalize(m_ctx);
61 GC.SuppressFinalize(
this);
64 #region Object Invariant 67 private void ObjectInvariant()
69 Contract.Invariant(this.m_ctx != null);
76 private IntPtr m_n_obj = IntPtr.Zero;
80 Contract.Requires(ctx != null);
82 Interlocked.Increment(ref ctx.refCount);
88 Contract.Requires(ctx != null);
90 Interlocked.Increment(ref ctx.refCount);
96 internal virtual void IncRef(IntPtr o) { }
97 internal virtual void DecRef(IntPtr o) { }
99 internal virtual void CheckNativeObject(IntPtr obj) { }
101 internal virtual IntPtr NativeObject
103 get {
return m_n_obj; }
106 if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
107 if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
112 internal static IntPtr GetNativeObject(
Z3Object s)
114 if (s == null)
return new IntPtr();
115 return s.NativeObject;
122 Contract.Ensures(Contract.Result<
Context>() != null);
128 internal static IntPtr[] ArrayToNative(
Z3Object[] a)
130 Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
131 Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Length);
133 if (a == null)
return null;
134 IntPtr[] an =
new IntPtr[a.Length];
135 for (uint i = 0; i < a.Length; i++)
136 if (a[i] != null) an[i] = a[i].NativeObject;
141 internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T :
Z3Object 143 Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
144 Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Count());
146 if (a == null)
return null;
147 IntPtr[] an =
new IntPtr[a.Count()];
149 foreach (var ai
in a)
151 if (ai != null) an[i] = ai.NativeObject;
158 internal static uint ArrayLength(
Z3Object[] a)
160 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.