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.Diagnostics;
21 using System;
22 using System.Threading;
23 using System.Collections.Generic;
24 using System.Linq;
25
26 namespace Microsoft.Z3
27{
32 public class Z3Object : IDisposable
33 {
37 ~Z3Object()
38 {
39 Dispose();
40 }
41
45 public void Dispose()
46 {
47 if (m_n_obj != IntPtr.Zero)
48 {
49 DecRef(m_n_obj);
50 m_n_obj = IntPtr.Zero;
51 }
52
53 if (m_ctx != null)
54 {
55 if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
56 GC.ReRegisterForFinalize(m_ctx);
57 m_ctx = null;
58 }
59
60 GC.SuppressFinalize(this);
61 }
62
63 #region Object Invariant
64
65 private void ObjectInvariant()
66 {
67 Debug.Assert(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 Debug.Assert(ctx != null);
79
80 Interlocked.Increment(ref ctx.refCount);
81 m_ctx = ctx;
82 }
83
84 internal Z3Object(Context ctx, IntPtr obj)
85 {
86 Debug.Assert(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 return m_ctx;
121 }
122 }
123
124 internal static IntPtr[] ArrayToNative(Z3Object[] a)
125 {
126
127 if (a == null) return null;
128 IntPtr[] an = new IntPtr[a.Length];
129 for (uint i = 0; i < a.Length; i++)
130 if (a[i] != null) an[i] = a[i].NativeObject;
131 return an;
132 }
133
134 internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T : Z3Object
135 {
136
137 if (a == null) return null;
138 IntPtr[] an = new IntPtr[a.Count()];
139 int i = 0;
140 foreach (var ai in a)
141 {
142 if (ai != null) an[i] = ai.NativeObject;
143 ++i;
144 }
145 return an;
146 }
147
148 internal static uint ArrayLength(Z3Object[] a)
149 {
150 return (a == null)?0:(uint)a.Length;
151 }
152 #endregion
153 }
154}
IDisposable
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Microsoft.Z3.Z3Object.Dispose
void Dispose()
Disposes of the underlying native Z3 object.
Definition: Z3Object.cs:45
Microsoft.Z3
Definition: AlgebraicNum.cs:27