CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
cdlist.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file cdlist.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Wed Feb 12 18:45:26 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__include__cdlist_h_
22
#define _cvc3__include__cdlist_h_
23
24
#include "
context.h
"
25
#include <deque>
26
27
namespace
CVC3 {
28
29
///////////////////////////////////////////////////////////////////////////////
30
// //
31
// Class: CDList (Context Dependent List) //
32
// Author: Clark Barrett //
33
// Created: Wed Feb 12 17:28:25 2003 //
34
// Description: Generic templated class for list which grows monotonically //
35
// over time (if the context is not popped) but must also be //
36
// saved and restored as contexts are pushed and popped. //
37
// //
38
///////////////////////////////////////////////////////////////////////////////
39
// TODO: more efficient implementation
40
template
<
class
T>
41
class
CDList
:
public
ContextObj
{
42
//! The actual data.
43
/*! Use deque because it doesn't create/destroy data on resize.
44
This pointer is only non-NULL in the master copy. */
45
std::deque<T>*
d_list
;
//
46
unsigned
d_size
;
47
48
virtual
ContextObj
*
makeCopy
(
ContextMemoryManager
* cmm) {
return
new
(cmm)
CDList<T>
(*
this
); }
49
virtual
void
restoreData
(
ContextObj
* data)
50
{
d_size
= ((
CDList<T>
*)data)->d_size;
51
while
(
d_list
->size() >
d_size
)
d_list
->pop_back(); }
52
virtual
void
setNull
(
void
)
53
{
while
(
d_list
->size())
d_list
->pop_back();
d_size
= 0; }
54
55
// Copy constructor (private). Do NOT copy d_list. It's not used
56
// in restore, and it will be deleted in destructor.
57
CDList
(
const
CDList<T>
& l):
ContextObj
(l),
d_list
(NULL),
d_size
(l.
d_size
) { }
58
public
:
59
CDList
(
Context
* context) :
ContextObj
(context),
d_size
(0) {
60
d_list
=
new
std::deque<T>();
61
IF_DEBUG
(setName(
"CDList"
);)
62
}
63
virtual
~
CDList
() {
if
(
d_list
!= NULL)
delete
d_list
; }
64
unsigned
size
()
const
{
return
d_size
; }
65
bool
empty
()
const
{
return
d_size
== 0; }
66
T&
push_back
(
const
T& data,
int
scope = -1)
67
{
makeCurrent
(scope);
d_list
->push_back(data); ++
d_size
;
return
d_list
->back(); }
68
void
pop_back
()
69
{
DebugAssert
(
isCurrent
() &&
getRestore
() &&
70
d_size
> ((
CDList<T>
*)
getRestore
())->
d_size
,
"pop_back precond violated"
);
71
d_list
->pop_back(); --
d_size
; }
72
const
T&
operator[]
(
unsigned
i)
const
{
73
DebugAssert
(i <
size
(),
74
"CDList["
+
int2string
(i)+
"]: i < size="
+
int2string
(
size
()));
75
return
(*
d_list
)[i];
76
}
77
const
T&
at
(
unsigned
i)
const
{
78
DebugAssert
(i <
size
(),
79
"CDList["
+
int2string
(i)+
"]: i < size="
+
int2string
(
size
()));
80
return
(*
d_list
)[i];
81
}
82
const
T&
back
()
const
{
83
DebugAssert
(
size
() > 0,
84
"CDList::back(): size="
+
int2string
(
size
()));
85
return
d_list
->back();
86
}
87
typedef
typename
std::deque<T>::const_iterator
const_iterator
;
88
const_iterator
begin
()
const
{
89
return
d_list
->begin();
90
}
91
const_iterator
end
()
const
{
92
return
begin
() +
d_size
;
93
}
94
};
95
96
}
97
98
#endif
Generated on Sun Aug 5 2012 13:18:31 for CVC3 by
1.8.1.2