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;
21 using System.Collections;
22 using System.Collections.Generic;
23 using System.Threading;
24 using System.Diagnostics.Contracts;
25 
26 namespace Microsoft.Z3
27 {
31  [ContractClass(typeof(DecRefQueueContracts))]
32  public abstract class IDecRefQueue
33  {
34  #region Object invariant
35 
36  [ContractInvariantMethod]
37  private void ObjectInvariant()
38  {
39  Contract.Invariant(this.m_queue != null);
40  }
41 
42  #endregion
43 
44  readonly private Object m_lock = new Object();
45  readonly private List<IntPtr> m_queue = new List<IntPtr>();
46  private uint m_move_limit;
47 
48  internal IDecRefQueue(uint move_limit = 1024)
49  {
50  m_move_limit = move_limit;
51  }
52 
57  public void SetLimit(uint l) { m_move_limit = l; }
58 
59  internal abstract void IncRef(Context ctx, IntPtr obj);
60  internal abstract void DecRef(Context ctx, IntPtr obj);
61 
62  internal void IncAndClear(Context ctx, IntPtr o)
63  {
64  Contract.Requires(ctx != null);
65 
66  IncRef(ctx, o);
67  if (m_queue.Count >= m_move_limit) Clear(ctx);
68  }
69 
70  internal void Add(IntPtr o)
71  {
72  if (o == IntPtr.Zero) return;
73 
74  lock (m_lock)
75  {
76  m_queue.Add(o);
77  }
78  }
79 
80  internal void Clear(Context ctx)
81  {
82  Contract.Requires(ctx != null);
83 
84  lock (m_lock)
85  {
86  foreach (IntPtr o in m_queue)
87  DecRef(ctx, o);
88  m_queue.Clear();
89  }
90  }
91  }
92 
93  [ContractClassFor(typeof(IDecRefQueue))]
95  {
96  internal override void IncRef(Context ctx, IntPtr obj)
97  {
98  Contract.Requires(ctx != null);
99  }
100 
101  internal override void DecRef(Context ctx, IntPtr obj)
102  {
103  Contract.Requires(ctx != null);
104  }
105  }
106 }
void SetLimit(uint l)
Sets the limit on numbers of objects that are kept back at GC collection.
Definition: IDecRefQueue.cs:57
using System
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31