CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
smartcdo.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file smartcdo.h
4
*\brief Smart context-dependent object wrapper
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Fri Nov 12 17:28:58 2004
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
#ifndef _cvc3__include__smartcdo_h_
23
#define _cvc3__include__smartcdo_h_
24
25
#include "
cdo.h
"
26
27
namespace
CVC3 {
28
29
/*****************************************************************************/
30
/*!
31
*\class SmartCDO
32
*\brief SmartCDO
33
*
34
* Author: Clark Barrett
35
*
36
* Created: Fri Nov 12 17:33:31 2004
37
*
38
* Wrapper for CDO which automatically allocates and deletes a pointer to a
39
* CDO. This allows the copy constructor and operator= to be defined which are
40
* especially useful for storing CDO's in vectors. All operations are const to
41
* enable use as a member of CDLists.
42
*
43
* Be careful not to delete RefCDO during pop(), since this messes up
44
* the backtracking data structures. We delay the deletion by
45
* registering each RefCDO to be notified before and after each pop().
46
* This makes the use of SmartCDO somewhat more expensive, so use it
47
* with care.
48
*
49
*/
50
/*****************************************************************************/
51
template
<
class
T>
52
class
SmartCDO
{
53
54
template
<
class
U>
55
class
RefCDO
{
56
friend
class
SmartCDO
;
57
unsigned
d_refCount
;
58
CDO<U>
d_cdo
;
59
bool
d_delay
;
//!< Whether to delay our own deletion
60
61
class
RefNotifyObj
:
public
ContextNotifyObj
{
62
friend
class
RefCDO
;
63
RefCDO<U>
*
d_ref
;
64
//! Constructor
65
RefNotifyObj
(
RefCDO<U>
* ref,
Context
* context)
66
:
ContextNotifyObj
(context),
d_ref
(ref) { }
67
void
notifyPre
() {
d_ref
->d_delay =
true
; }
68
void
notify
() {
69
d_ref
->d_delay =
false
;
70
d_ref
->kill();
71
}
72
};
73
74
RefNotifyObj
*
d_notifyObj
;
75
76
friend
class
RefNotifyObj
;
77
78
RefCDO
(
Context
* context):
d_refCount
(0),
d_cdo
(context),
d_delay
(false),
79
d_notifyObj
(new
RefNotifyObj
(this, context)) {}
80
81
RefCDO
(
Context
* context,
const
U& cdo,
int
scope = -1)
82
:
d_refCount
(0),
d_cdo
(context, cdo, scope),
d_delay
(false),
83
d_notifyObj
(new
RefNotifyObj
(this, context)) {}
84
85
~RefCDO
() {
delete
d_notifyObj
; }
86
//! Delete itself, unless delayed (then we'll be called again later)
87
void
kill
() {
if
(
d_refCount
==0 && !
d_delay
)
delete
this
; }
88
};
89
90
RefCDO<T>*
d_data
;
91
92
public
:
93
//! Check if the SmartCDO object is Null
94
bool
isNull
()
const
{
return
(
d_data
==NULL); }
95
//! Default constructor: create a Null SmartCDO object
96
SmartCDO
():
d_data
(NULL) { }
97
//! Create and initialize SmartCDO object at the current scope
98
SmartCDO
(
Context
* context)
99
{
d_data
=
new
RefCDO<T>(context);
d_data
->
d_refCount
++; }
100
//! Create and initialize SmartCDO object at the given scope
101
SmartCDO
(
Context
* context,
const
T& data,
int
scope = -1)
102
{
d_data
=
new
RefCDO<T>(context, data, scope);
d_data
->
d_refCount
++; }
103
//! Delete
104
~SmartCDO
()
105
{
if
(
isNull
())
return
;
106
if
(--
d_data
->
d_refCount
== 0)
d_data
->
kill
(); }
107
108
SmartCDO
(
const
SmartCDO<T>
& cdo) :
d_data
(cdo.
d_data
)
109
{
if
(!
isNull
())
d_data
->
d_refCount
++; }
110
111
SmartCDO<T>
&
operator=
(
const
SmartCDO<T>
& cdo)
112
{
113
if
(
this
== &cdo)
return
*
this
;
114
if
(!
isNull
() && --(
d_data
->
d_refCount
))
d_data
->
kill
();
115
d_data
= cdo.
d_data
;
116
if
(!
isNull
()) ++(
d_data
->
d_refCount
);
117
return
*
this
;
118
}
119
120
void
set
(
const
T& data,
int
scope=-1)
const
{
121
DebugAssert
(!
isNull
(),
"SmartCDO::set: we are Null"
);
122
d_data
->
d_cdo
.set(data, scope);
123
}
124
const
T&
get
()
const
{
125
DebugAssert
(!
isNull
(),
"SmartCDO::get: we are Null"
);
126
return
d_data
->
d_cdo
.get();
127
}
128
operator
T()
const
{
return
get
(); }
129
const
SmartCDO<T>
&
operator=
(
const
T& data)
const
{
set
(data);
return
*
this
;}
130
};
131
132
}
133
134
#endif
Generated on Sat Aug 3 2013 07:58:31 for CVC3 by
1.8.4