diff options
| -rw-r--r-- | src/context/Makefile.am | 1 | ||||
| -rw-r--r-- | src/context/cdlist.h | 19 | ||||
| -rw-r--r-- | src/context/cdqueue2.h | 147 |
3 files changed, 161 insertions, 6 deletions
diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 7f6501332..da5d8da9e 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -15,6 +15,7 @@ libcontext_la_SOURCES = \ cdlist_context_memory.h \ cdlist_forward.h \ cdqueue.h \ + cdqueue2.h \ cdmap.h \ cdmap_forward.h \ cdset.h \ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index dea9f8be7..da101e1a6 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -174,21 +174,28 @@ protected: << " data == " << data << " call dtor == " << this->d_callDestructor << " d_list == " << this->d_list << std::endl; + removeLastUntil(((CDList<T, Allocator>*)data)->d_size); + Debug("cdlist") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size + << " sizeAlloc at " << this->d_sizeAlloc << std::endl; + } + + /** Remove the elements from the given indices to the last. + * You should use this function only when you know what you do. + */ + inline void removeLastUntil(const size_t size){ if(this->d_callDestructor) { - const size_t size = ((CDList<T, Allocator>*)data)->d_size; while(this->d_size != size) { --this->d_size; this->d_allocator.destroy(&this->d_list[this->d_size]); } } else { - this->d_size = ((CDList<T, Allocator>*)data)->d_size; + this->d_size = size; } - Debug("cdlist") << "restore " << this - << " level " << this->getContext()->getLevel() - << " size back to " << this->d_size - << " sizeAlloc at " << this->d_sizeAlloc << std::endl; } + public: /** diff --git a/src/context/cdqueue2.h b/src/context/cdqueue2.h new file mode 100644 index 000000000..bbff932d4 --- /dev/null +++ b/src/context/cdqueue2.h @@ -0,0 +1,147 @@ +/********************* */ +/*! \file cdqueue.h + ** \verbatim + ** Original author: bobot + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent queue class + ** + ** Context-dependent First-In-First-Out queue class. + ** The implementation is based on a CDList with one additional size_t + ** for tracking the next element to dequeue from the list and additional + ** size_t. + ** It can discard element which are enqueued and dequeued at the same context + ** level. + ** The implementation is try to stay simple. + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDQUEUE2_H +#define __CVC4__CONTEXT__CDQUEUE2_H + +#include "context/context.h" +#include "context/cdlist.h" + +namespace CVC4 { +namespace context { + +/** We don't define a template with Allocator for the first implementation */ +template <class T> +class CDQueue2 : public CDList<T> { +protected: + + /** Points to the next element in the current context to dequeue. */ + size_t d_iter; + + /** Points to the size at the last save. */ + size_t d_lastsave; + + /** + * Private copy constructor used only by save(). + */ + CDQueue2(const CDQueue2<T>& l): + CDList<T>(l), + d_iter(l.d_iter), + d_lastsave(l.d_lastsave) {} + + /** Implementation of mandatory ContextObj method save: + * We assume that the base class do the job inside their copy constructor. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDQueue2<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; + Debug("cdqueue2") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " iter at " << this->d_iter + << " lastsave at " << this->d_lastsave + << " sizeAlloc at " << this->d_sizeAlloc + << " d_list is " << this->d_list + << " data:" << data << std::endl; + return data; + } + + /** + * Implementation of mandatory ContextObj method restore: simply + * restores the previous size, iter and lastsave indices. Note that + * the list pointer and the allocated size are not changed. + */ + void restore(ContextObj* data) { + CDQueue2<T>* qdata = ((CDQueue2<T>*)data); + d_iter = qdata->d_iter; + d_lastsave = qdata->d_lastsave; + CDList<T>::restore(data); + } + + + +public: + + /** Creates a new CDQueue associated with the current context. */ + CDQueue2(Context* context) + : CDList<T>(context), + d_iter(0), + d_lastsave(0) + {} + + /** Returns true if the queue is empty in the current context. */ + bool empty() const{ + return d_iter >= CDList<T>::d_size; + } + + bool size() const{ + return d_iter - CDList<T>::d_size; + } + + /** Enqueues an element in the current context. */ + void push(const T& data){ + CDList<T>::push_back(data); + } + + /** Delete next element. The destructor of this object will be + called eventually but not necessarily during the call of this + function. + */ + void pop(){ + Assert(!empty(), "Attempting to pop from an empty queue."); + CDList<T>::makeCurrent(); + d_iter = d_iter + 1; + if (d_iter == CDList<T>::d_size && d_lastsave != CDList<T>::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>::removeLastUntil(d_lastsave); + d_iter = CDList<T>::d_size = d_lastsave; + } + } + + /** Returns a reference to the next element on the queue. */ + const T& front(){ + Assert(!empty(), "No front in an empty queue."); + return CDList<T>::d_list[d_iter]; + } + + /** + * Returns the most recent item added to the list. + */ + const T& back() const { + Assert(!empty(), "CDQueue2::back() called on empty list"); + return CDList<T>::d_list[CDList<T>::d_size - 1]; + } + +};/* class CDQueue<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDQUEUE_H */ |