diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-02 20:56:55 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-02 20:56:55 +0000 |
commit | 1a558a30bec496444742ed75c0a6973d9789daf7 (patch) | |
tree | 81d5f4aedc3a320c4b95945c71a1e3cf0d8e88af /src/context/cdvector.h | |
parent | f9d3552033d8214c833b58ed54d99c836de4ce37 (diff) |
- Merged in the branch cdlist-cleanup.
- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.
Diffstat (limited to 'src/context/cdvector.h')
-rw-r--r-- | src/context/cdvector.h | 131 |
1 files changed, 67 insertions, 64 deletions
diff --git a/src/context/cdvector.h b/src/context/cdvector.h index 49d1b67e9..9464f416b 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -23,86 +23,79 @@ #define __CVC4__CONTEXT__CDVECTOR_H #include "context/context.h" -#include "context/cdo.h" +#include "context/cdlist.h" #include "util/Assert.h" -#include "util/dynamic_array.h" +#include <vector> + namespace CVC4 { namespace context { -template <class T> -struct UpdatableElement { -public: - T d_data; - int d_contextLevelOfLastUpdate; - - UpdatableElement(const T& data) : - d_data(data), - d_contextLevelOfLastUpdate(0) { - } -};/* struct UpdatableElement<T> */ - -template <class T> -struct HistoryElement { -public: - UpdatableElement<T> d_cached; - unsigned d_index; - HistoryElement(const UpdatableElement<T>& cache, unsigned index) : - d_cached(cache), d_index(index) { - } -};/* struct HistoryElement<T> */ - /** * Generic context-dependent dynamic vector. + * This is quite different than CDList<T>. * It provides the ability to destructively update the i'th item. - * Note that the size of the vector never decreases. * - * This is quite different than CDList<T>. + * The back of the vector may only be popped if there have been no updates to it + * at this context level. */ template <class T> class CDVector { private: - typedef DynamicArray< UpdatableElement<T> > CurrentVector; - typedef DynamicArray< HistoryElement<T> > HistoryVector; + static const int ImpossibleLevel = -1; - Context* d_context; + struct UpdatableElement { + public: + T d_data; + int d_contextLevelOfLastUpdate; - DynamicArray< UpdatableElement<T> > d_current; - DynamicArray< HistoryElement<T> > d_history; + UpdatableElement(const T& data) : + d_data(data), + d_contextLevelOfLastUpdate(ImpossibleLevel) { + } + };/* struct CDVector<T>::UpdatableElement */ + + struct HistoryElement { + public: + UpdatableElement d_cached; + size_t d_index; + HistoryElement(const UpdatableElement& cache, size_t index) : + d_cached(cache), d_index(index) { + } + };/* struct CDVector<T>::HistoryElement */ - CDO<unsigned> d_historySize; + typedef std::vector< UpdatableElement > CurrentVector; + CurrentVector d_current; -private: - void restoreConsistency() { - Assert(d_history.size() >= d_historySize.get()); - while(d_history.size() > d_historySize.get()) { - const HistoryElement<T>& back = d_history.back(); - d_current[back.d_index] = back.d_cached; - d_history.pop_back(); - } - } - bool isConsistent() const { - return d_history.size() == d_historySize.get(); - } - void makeConsistent() { - if(!isConsistent()) { - restoreConsistency(); + class HistoryListCleanUp{ + private: + CurrentVector& d_current; + public: + HistoryListCleanUp(CurrentVector& current) + : d_current(current) + {} + + void operator()(HistoryElement* back){ + d_current[back->d_index] = back->d_cached; } - Assert(isConsistent()); - } + };/* class CDVector<T>::HistoryListCleanUp */ + + typedef CDList< HistoryElement, HistoryListCleanUp > HistoryVector; + HistoryVector d_history; + + Context* d_context; public: - CDVector(Context* c, bool callDestructor = false) : - d_context(c), - d_current(callDestructor), - d_history(callDestructor), - d_historySize(c, 0) { - } + CDVector(Context* c) : + d_current(), + d_history(c, true, HistoryListCleanUp(d_current)), + d_context(c) + {} - unsigned size() const { + size_t size() const { return d_current.size(); } @@ -118,37 +111,47 @@ public: * Assigns its state at level 0 to be equal to data. */ void push_back(const T& data) { - d_current.push_back(UpdatableElement<T>(data)); + d_current.push_back(UpdatableElement(data)); } /** * Access to the ith item in the list. */ - const T& operator[](unsigned i) { + const T& operator[](size_t i) const { return get(i); } - const T& get(unsigned i) { + const T& get(size_t i) const { Assert(i < size(), "index out of bounds in CDVector::get()"); - makeConsistent(); + //makeConsistent(); return d_current[i].d_data; } - void set(unsigned index, const T& data) { + void set(size_t index, const T& data) { Assert(index < size(), "index out of bounds in CDVector::set()"); - makeConsistent(); + //makeConsistent(); if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) { d_current[index].d_data = data; }else{ - d_history.push_back(HistoryElement<T>(d_current[index], index)); - d_historySize.set(d_historySize.get() + 1); + d_history.push_back(HistoryElement(d_current[index], index)); d_current[index].d_data = data; d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel(); } } + bool hasUpdates(size_t index) const { + Assert(index < size(), "index out of bounds in CDVector::hasUpdates()"); + return d_current[index].d_contextLevelOfLastUpdate == ImpossibleLevel; + } + + void pop_back() { + Assert(!empty(), "pop_back() on an empty CDVector"); + Assert(!hasUpdates(size() - 1), "popping an element with updates."); + d_current.pop_back(); + } + };/* class CDVector<T> */ }/* CVC4::context namespace */ |