1 /********************* */
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_private.h"
22 #ifndef __CVC4__CONTEXT__CDVECTOR_H
23 #define __CVC4__CONTEXT__CDVECTOR_H
25 #include "context/context.h"
26 #include "context/cdo.h"
27 #include "util/Assert.h"
28 #include "util/dynamic_array.h"
34 struct UpdatableElement
{
37 int d_contextLevelOfLastUpdate
;
39 UpdatableElement(const T
& data
) :
41 d_contextLevelOfLastUpdate(0) {
43 };/* struct UpdatableElement<T> */
46 struct HistoryElement
{
48 UpdatableElement
<T
> d_cached
;
50 HistoryElement(const UpdatableElement
<T
>& cache
, unsigned index
) :
51 d_cached(cache
), d_index(index
) {
53 };/* struct HistoryElement<T> */
57 * Generic context-dependent dynamic vector.
58 * It provides the ability to destructively update the i'th item.
59 * Note that the size of the vector never decreases.
61 * This is quite different than CDList<T>.
66 typedef DynamicArray
< UpdatableElement
<T
> > CurrentVector
;
67 typedef DynamicArray
< HistoryElement
<T
> > HistoryVector
;
71 DynamicArray
< UpdatableElement
<T
> > d_current
;
72 DynamicArray
< HistoryElement
<T
> > d_history
;
74 CDO
<unsigned> d_historySize
;
77 void restoreConsistency() {
78 Assert(d_history
.size() >= d_historySize
.get());
79 while(d_history
.size() > d_historySize
.get()) {
80 const HistoryElement
<T
>& back
= d_history
.back();
81 d_current
[back
.d_index
] = back
.d_cached
;
86 bool isConsistent() const {
87 return d_history
.size() == d_historySize
.get();
90 void makeConsistent() {
94 Assert(isConsistent());
98 CDVector(Context
* c
, bool callDestructor
= false) :
100 d_current(callDestructor
),
101 d_history(callDestructor
),
102 d_historySize(c
, 0) {
105 unsigned size() const {
106 return d_current
.size();
110 * Return true iff there are no valid objects in the list.
113 return d_current
.empty();
117 * Add an item to the end of the list.
118 * Assigns its state at level 0 to be equal to data.
120 void push_back(const T
& data
) {
121 d_current
.push_back(UpdatableElement
<T
>(data
));
125 * Access to the ith item in the list.
127 const T
& operator[](unsigned i
) {
131 const T
& get(unsigned i
) {
132 Assert(i
< size(), "index out of bounds in CDVector::get()");
134 return d_current
[i
].d_data
;
137 void set(unsigned index
, const T
& data
) {
138 Assert(index
< size(), "index out of bounds in CDVector::set()");
141 if(d_current
[index
].d_contextLevelOfLastUpdate
== d_context
->getLevel()) {
142 d_current
[index
].d_data
= data
;
144 d_history
.push_back(HistoryElement
<T
>(d_current
[index
], index
));
145 d_historySize
.set(d_historySize
.get() + 1);
147 d_current
[index
].d_data
= data
;
148 d_current
[index
].d_contextLevelOfLastUpdate
= d_context
->getLevel();
152 };/* class CDVector<T> */
154 }/* CVC4::context namespace */
155 }/* CVC4 namespace */
157 #endif /* __CVC4__CONTEXT__CDVECTOR_H */