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;
22 using System.Threading;
23 using System.Collections.Generic;
24 using System.Linq;
25 
26 namespace Microsoft.Z3
27 {
32  [ContractVerification(true)]
33  public class Z3Object : IDisposable
34  {
38  ~Z3Object()
39  {
40  Dispose();
41  }
42 
46  public void Dispose()
47  {
48  if (m_n_obj != IntPtr.Zero)
49  {
50  DecRef(m_n_obj);
51  m_n_obj = IntPtr.Zero;
52  }
53 
54  if (m_ctx != null)
55  {
56  if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
57  GC.ReRegisterForFinalize(m_ctx);
58  m_ctx = null;
59  }
60 
61  GC.SuppressFinalize(this);
62  }
63 
64  #region Object Invariant
65 
67  private void ObjectInvariant()
68  {
69  Contract.Invariant(this.m_ctx != null);
70  }
71 
72  #endregion
73 
74  #region Internal
75  private Context m_ctx = null;
76  private IntPtr m_n_obj = IntPtr.Zero;
77 
78  internal Z3Object(Context ctx)
79  {
80  Contract.Requires(ctx != null);
81 
82  Interlocked.Increment(ref ctx.refCount);
83  m_ctx = ctx;
84  }
85 
86  internal Z3Object(Context ctx, IntPtr obj)
87  {
88  Contract.Requires(ctx != null);
89 
90  Interlocked.Increment(ref ctx.refCount);
91  m_ctx = ctx;
92  IncRef(obj);
93  m_n_obj = obj;
94  }
95 
96  internal virtual void IncRef(IntPtr o) { }
97  internal virtual void DecRef(IntPtr o) { }
98 
99  internal virtual void CheckNativeObject(IntPtr obj) { }
100 
101  internal virtual IntPtr NativeObject
102  {
103  get { return m_n_obj; }
104  set
105  {
106  if (value != IntPtr.Zero) { CheckNativeObject(value); IncRef(value); }
107  if (m_n_obj != IntPtr.Zero) { DecRef(m_n_obj); }
108  m_n_obj = value;
109  }
110  }
111 
112  internal static IntPtr GetNativeObject(Z3Object s)
113  {
114  if (s == null) return new IntPtr();
115  return s.NativeObject;
116  }
117 
118  internal Context Context
119  {
120  get
121  {
122  Contract.Ensures(Contract.Result<Context>() != null);
123  return m_ctx;
124  }
125  }
126 
127  [Pure]
128  internal static IntPtr[] ArrayToNative(Z3Object[] a)
129  {
130  Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
131  Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Length);
132 
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;
137  return an;
138  }
139 
140  [Pure]
141  internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T : Z3Object
142  {
143  Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
144  Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Count());
145 
146  if (a == null) return null;
147  IntPtr[] an = new IntPtr[a.Count()];
148  int i = 0;
149  foreach (var ai in a)
150  {
151  if (ai != null) an[i] = ai.NativeObject;
152  ++i;
153  }
154  return an;
155  }
156 
157  [Pure]
158  internal static uint ArrayLength(Z3Object[] a)
159  {
160  return (a == null)?0:(uint)a.Length;
161  }
162  #endregion
163  }
164 }
void Dispose()
Disposes of the underlying native Z3 object.
Definition: Z3Object.cs:46
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33