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/cdqueue.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/cdqueue.h')
-rw-r--r-- | src/context/cdqueue.h | 45 |
1 files changed, 27 insertions, 18 deletions
diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index 16f81709e..d8f6c42f1 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -34,9 +34,15 @@ namespace CVC4 { namespace context { +template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> > +class CDQueue; + /** We don't define a template with Allocator for the first implementation */ -template <class T> -class CDQueue : public CDList<T> { +template <class T, class CleanUp, class Allocator> +class CDQueue : public CDList<T, CleanUp, Allocator> { +private: + typedef CDList<T, CleanUp, Allocator> ParentType; + protected: /** Points to the next element in the current context to dequeue. */ @@ -48,8 +54,8 @@ protected: /** * Private copy constructor used only by save(). */ - CDQueue(const CDQueue<T>& l): - CDList<T>(l), + CDQueue(const CDQueue<T, CleanUp, Allocator>& l): + ParentType(l), d_iter(l.d_iter), d_lastsave(l.d_lastsave) {} @@ -60,7 +66,7 @@ protected: ContextObj* data = new(pCMM) CDQueue<T>(*this); // We save the d_size in d_lastsave and we should never destruct below this // indices before the corresponding restore. - d_lastsave = CDList<T>::d_size; + d_lastsave = ParentType::d_size; Debug("cdqueue") << "save " << this << " at level " << this->getContext()->getLevel() << " size at " << this->d_size @@ -80,7 +86,7 @@ protected: CDQueue<T>* qdata = static_cast<CDQueue<T>*>(data); d_iter = qdata->d_iter; d_lastsave = qdata->d_lastsave; - CDList<T>::restore(data); + ParentType::restore(data); } @@ -88,26 +94,29 @@ protected: public: /** Creates a new CDQueue associated with the current context. */ - CDQueue(Context* context) - : CDList<T>(context), + CDQueue(Context* context, + bool callDestructor = true, + const CleanUp& cleanup = CleanUp(), + const Allocator& alloc = Allocator()) + : ParentType(context, callDestructor, cleanup, alloc), d_iter(0), d_lastsave(0) {} /** Returns true if the queue is empty in the current context. */ bool empty() const{ - Assert(d_iter <= CDList<T>::d_size); - return d_iter == CDList<T>::d_size; + Assert(d_iter <= ParentType::d_size); + return d_iter == ParentType::d_size; } /** Returns the number of elements that have not been dequeued in the context. */ size_t size() const{ - return CDList<T>::d_size - d_iter; + return ParentType::d_size - d_iter; } /** Enqueues an element in the current context. */ void push(const T& data){ - CDList<T>::push_back(data); + ParentType::push_back(data); } /** @@ -117,13 +126,13 @@ public: */ void pop(){ Assert(!empty(), "Attempting to pop from an empty queue."); - CDList<T>::makeCurrent(); + ParentType::makeCurrent(); d_iter = d_iter + 1; - if (empty() && d_lastsave != CDList<T>::d_size) { + if (empty() && d_lastsave != ParentType::d_size) { // Some elements have been enqueued and dequeued in the same // context and now the queue is empty we can destruct them. - CDList<T>::truncateList(d_lastsave); - Assert(CDList<T>::d_size == d_lastsave); + ParentType::truncateList(d_lastsave); + Assert(ParentType::d_size == d_lastsave); d_iter = d_lastsave; } } @@ -131,7 +140,7 @@ public: /** Returns a reference to the next element on the queue. */ const T& front() const{ Assert(!empty(), "No front in an empty queue."); - return CDList<T>::d_list[d_iter]; + return ParentType::d_list[d_iter]; } /** @@ -139,7 +148,7 @@ public: */ const T& back() const { Assert(!empty(), "CDQueue::back() called on empty list"); - return CDList<T>::d_list[CDList<T>::d_size - 1]; + return ParentType::d_list[ParentType::d_size - 1]; } };/* class CDQueue<> */ |