Z3
src
api
dotnet
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
))]
94
abstract
class
DecRefQueueContracts
:
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
}
System.Diagnostics.Contracts.ContractInvariantMethod
Definition:
DummyContracts.cs:33
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:57
System.Diagnostics.Contracts.ContractClassFor
Definition:
DummyContracts.cs:28
System
System.Diagnostics
Microsoft
System.Diagnostics.Contracts
Definition:
DummyContracts.cs:21
Microsoft.Z3.IDecRefQueue
DecRefQueue interface
Definition:
IDecRefQueue.cs:32
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:32
Microsoft.Z3.DecRefQueueContracts
Definition:
IDecRefQueue.cs:94
System.Diagnostics.Contracts.ContractClass
Definition:
DummyContracts.cs:23
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12