Z3 |

IDecRefQueue.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 DecRefQueue.cs
7
8 Abstract:
9
10 Z3 Managed API: DecRef Queues
11
12 Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-16
15
16 Notes:
17
18--*/
19
20 using System.Diagnostics;
21 using System;
22 using System.Collections;
23 using System.Collections.Generic;
24 using System.Threading;
25
26 namespace Microsoft.Z3
27{
31 public abstract class IDecRefQueue
32 {
33 #region Object invariant
34
35 private void ObjectInvariant()
36 {
37 Debug.Assert(this.m_queue != null);
38 }
39
40 #endregion
41
42 readonly private Object m_lock = new Object();
43 readonly private List<IntPtr> m_queue = new List<IntPtr>();
44 private uint m_move_limit;
45
46 internal IDecRefQueue(uint move_limit = 1024)
47 {
48 m_move_limit = move_limit;
49 }
50
55 public void SetLimit(uint l) { m_move_limit = l; }
56
57 internal abstract void IncRef(Context ctx, IntPtr obj);
58 internal abstract void DecRef(Context ctx, IntPtr obj);
59
60 internal void IncAndClear(Context ctx, IntPtr o)
61 {
62 Debug.Assert(ctx != null);
63
64 IncRef(ctx, o);
65 if (m_queue.Count >= m_move_limit) Clear(ctx);
66 }
67
68 internal void Add(IntPtr o)
69 {
70 if (o == IntPtr.Zero) return;
71
72 lock (m_lock)
73 {
74 m_queue.Add(o);
75 }
76 }
77
78 internal void Clear(Context ctx)
79 {
80 Debug.Assert(ctx != null);
81
82 lock (m_lock)
83 {
84 foreach (IntPtr o in m_queue)
85 DecRef(ctx, o);
86 m_queue.Clear();
87 }
88 }
89 }
90
91 abstract class DecRefQueueContracts : IDecRefQueue
92 {
93 internal override void IncRef(Context ctx, IntPtr obj)
94 {
95 Debug.Assert(ctx != null);
96 }
97
98 internal override void DecRef(Context ctx, IntPtr obj)
99 {
100 Debug.Assert(ctx != null);
101 }
102 }
103}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.DecRefQueueContracts
Definition: IDecRefQueue.cs:92
Microsoft.Z3.IDecRefQueue
DecRefQueue interface
Definition: IDecRefQueue.cs:32
Microsoft.Z3.IDecRefQueue.SetLimit
void SetLimit(uint l)
Sets the limit on numbers of objects that are kept back at GC collection.
Definition: IDecRefQueue.cs:55
Microsoft.Z3
Definition: AlgebraicNum.cs:27