Z3
Z3Object.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Z3Object.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Internal Z3 Objects
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 using System.Threading;
23 
24 namespace Microsoft.Z3
25 {
30  [ContractVerification(true)]
31  public class Z3Object : IDisposable
32  {
36  ~Z3Object()
37  {
38  Dispose();
39  }
40 
44  public void Dispose()
45  {
46  if (m_n_obj != IntPtr.Zero)
47  {
48  DecRef(m_n_obj);
49  m_n_obj = IntPtr.Zero;
50  }
51 
52  if (m_ctx != null)
53  {
54  if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
55  GC.ReRegisterForFinalize(m_ctx);
56  m_ctx = null;
57  }
58 
59  GC.SuppressFinalize(this);
60  }
61 
62  #region Object Invariant
63 
64  [ContractInvariantMethod]
65  private void ObjectInvariant()
66  {
67  Contract.Invariant(this.m_ctx != null);
68  }
69 
70  #endregion
71 
72  #region Internal
73  private Context m_ctx = null;
74  private IntPtr m_n_obj = IntPtr.Zero;
75 
76  internal Z3Object(Context ctx)
77  {
78  Contract.Requires(ctx != null);
79 
80  Interlocked.Increment(ref ctx.refCount);
81  m_ctx = ctx;
82  }
83 
84  internal Z3Object(Context ctx, IntPtr obj)
85  {
86  Contract.Requires(ctx != null);
87 
88  Interlocked.Increment(ref ctx.refCount);
89  m_ctx = ctx;
90  IncRef(obj);
91  m_n_obj = obj;
92  }
93 
94  internal virtual void IncRef(IntPtr o) { }
95  internal virtual void DecRef(IntPtr o) { }
96 
97  internal virtual void CheckNativeObject(IntPtr obj) { }
98 
99  internal virtual IntPtr NativeObject
100  {
101  get { return m_n_obj; }
102  set
103  {
104  if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
105  if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
106  m_n_obj = value;
107  }
108  }
109 
110  internal static IntPtr GetNativeObject(Z3Object s)
111  {
112  if (s == null) return new IntPtr();
113  return s.NativeObject;
114  }
115 
116  internal Context Context
117  {
118  get
119  {
120  Contract.Ensures(Contract.Result<Context>() != null);
121  return m_ctx;
122  }
123  }
124 
125  [Pure]
126  internal static IntPtr[] ArrayToNative(Z3Object[] a)
127  {
128  Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
129  Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Length);
130 
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;
135  return an;
136  }
137 
138  [Pure]
139  internal static uint ArrayLength(Z3Object[] a)
140  {
141  return (a == null)?0:(uint)a.Length;
142  }
143  #endregion
144  }
145 }
using System
void Dispose()
Disposes of the underlying native Z3 object.
Definition: Z3Object.cs:44
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31