From 730c6a6baa994a646af08c32151ba487d957d383 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 2 Mar 2012 16:32:16 +0000 Subject: Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function names and documentation. --- src/context/Makefile.am | 2 +- src/context/cdlist.h | 52 ++++++----- src/context/cdqueue.h | 114 ++++++++++++++++++++----- src/context/cdqueue2.h | 147 -------------------------------- src/context/cdtrail_queue.h | 93 ++++++++++++++++++++ src/theory/arith/difference_manager.cpp | 3 +- src/theory/arith/difference_manager.h | 4 +- 7 files changed, 223 insertions(+), 192 deletions(-) delete mode 100644 src/context/cdqueue2.h create mode 100644 src/context/cdtrail_queue.h (limited to 'src') diff --git a/src/context/Makefile.am b/src/context/Makefile.am index da5d8da9e..e40eac099 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -15,7 +15,7 @@ libcontext_la_SOURCES = \ cdlist_context_memory.h \ cdlist_forward.h \ cdqueue.h \ - cdqueue2.h \ + cdtrail_queue.h \ cdmap.h \ cdmap_forward.h \ cdset.h \ diff --git a/src/context/cdlist.h b/src/context/cdlist.h index da101e1a6..cb9be07d3 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -56,14 +56,21 @@ public: protected: - static const size_t INITIAL_SIZE = 10; - static const size_t GROWTH_FACTOR = 2; - /** * d_list is a dynamic array of objects of type T. */ T* d_list; + /** + * Number of objects in d_list + */ + size_t d_size; + +private: + + static const size_t INITIAL_SIZE = 10; + static const size_t GROWTH_FACTOR = 2; + /** * Whether to call the destructor when items are popped from the * list. True by default, but can be set to false by setting the @@ -71,11 +78,6 @@ protected: */ bool d_callDestructor; - /** - * Number of objects in d_list - */ - size_t d_size; - /** * Allocated size of d_list. */ @@ -86,6 +88,7 @@ protected: */ Allocator d_allocator; +protected: /** * Private copy constructor used only by save(). d_list and * d_sizeAlloc are not copied: only the base class information and @@ -94,8 +97,8 @@ protected: CDList(const CDList& l) : ContextObj(l), d_list(NULL), - d_callDestructor(false), d_size(l.d_size), + d_callDestructor(false), d_sizeAlloc(0), d_allocator(l.d_allocator) { Debug("cdlist") << "copy ctor: " << this @@ -103,6 +106,7 @@ protected: << " size " << d_size << std::endl; } +private: /** * Reallocate the array with more space. * Throws bad_alloc if memory allocation fails. @@ -163,6 +167,7 @@ protected: return data; } +protected: /** * Implementation of mandatory ContextObj method restore: simply * restores the previous size. Note that the list pointer and the @@ -174,24 +179,31 @@ protected: << " data == " << data << " call dtor == " << this->d_callDestructor << " d_list == " << this->d_list << std::endl; - removeLastUntil(((CDList*)data)->d_size); + truncateList(((CDList*)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. + /** + * Given a size parameter smaller than d_size, truncateList() + * removes the elements from the end of the list until d_size equals size. + * + * WARNING! You should only use this function when you know what you are doing. + * This is a primitive operation with strange context dependent behavior! + * It is up to the user of the function to ensure that the saved d_size values + * at lower context levels are less than or equal to size. */ - inline void removeLastUntil(const size_t size){ - if(this->d_callDestructor) { - while(this->d_size != size) { - --this->d_size; - this->d_allocator.destroy(&this->d_list[this->d_size]); + void truncateList(const size_t size){ + Assert(size <= d_size); + if(d_callDestructor) { + while(d_size != size) { + --d_size; + d_allocator.destroy(&d_list[d_size]); } } else { - this->d_size = size; + d_size = size; } } @@ -205,8 +217,8 @@ public: const Allocator& alloc = Allocator()) : ContextObj(context), d_list(NULL), - d_callDestructor(callDestructor), d_size(0), + d_callDestructor(callDestructor), d_sizeAlloc(0), d_allocator(alloc) { } @@ -218,8 +230,8 @@ public: const Allocator& alloc = Allocator()) : ContextObj(allocatedInCMM, context), d_list(NULL), - d_callDestructor(callDestructor), d_size(0), + d_callDestructor(callDestructor), d_sizeAlloc(0), d_allocator(alloc) { } diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index 8e8c5c0d7..f84b66349 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -1,7 +1,7 @@ /********************* */ /*! \file cdqueue.h ** \verbatim - ** Original author: taking + ** Original author: bobot ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. @@ -14,9 +14,12 @@ ** \brief Context-dependent queue class ** ** Context-dependent First-In-First-Out queue class. - ** The implementation is based on a combination of CDList and a CDO - ** for tracking the next element to dequeue from the list. - ** The implementation is currently very simple. + ** This implementation may discard elements which are enqueued and dequeued + ** at the same context level. + ** + ** 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 for tracking the previous size of the list. **/ @@ -31,42 +34,111 @@ namespace CVC4 { namespace context { - +/** We don't define a template with Allocator for the first implementation */ template -class CDQueue { -private: - - /** List of elements in the queue. */ - CDList d_list; +class CDQueue : public CDList { +protected: /** Points to the next element in the current context to dequeue. */ - CDO d_iter; + size_t d_iter; + + /** Points to the size at the last save. */ + size_t d_lastsave; + + /** + * Private copy constructor used only by save(). + */ + CDQueue(const CDQueue& l): + CDList(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) CDQueue(*this); + // We save the d_size in d_lastsave and we should never destruct below this + // indices before the corresponding restore. + d_lastsave = CDList::d_size; + Debug("cdqueue") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " iter at " << this->d_iter + << " lastsave at " << this->d_lastsave + << " 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) { + CDQueue* qdata = ((CDQueue*)data); + d_iter = qdata->d_iter; + d_lastsave = qdata->d_lastsave; + CDList::restore(data); + } + public: /** Creates a new CDQueue associated with the current context. */ CDQueue(Context* context) - : d_list(context), - d_iter(context, 0) + : CDList(context), + d_iter(0), + d_lastsave(0) {} /** Returns true if the queue is empty in the current context. */ bool empty() const{ - return d_iter >= d_list.size(); + return d_iter >= CDList::d_size; + } + + /** Returns the number of elements that have not been dequeued in the context. */ + size_t size() const{ + return d_iter - CDList::d_size; } /** Enqueues an element in the current context. */ - void enqueue(const T& data){ - d_list.push_back(data); + void push(const T& data){ + CDList::push_back(data); } - /** Returns a reference to the next element on the queue. */ - const T& dequeue(){ - Assert(!empty(), "Attempting to queue from an empty queue."); - size_t front = d_iter; + /** + * 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::makeCurrent(); d_iter = d_iter + 1; - return d_list[front]; + if (d_iter == CDList::d_size && d_lastsave != CDList::d_size) { + // Some elements have been enqueued and dequeued in the same + // context and now the queue is empty we can destruct them. + CDList::truncateList(d_lastsave); + Assert(d_size == d_lastsave); + d_iter = 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::d_list[d_iter]; + } + + /** + * Returns the most recent item added to the list. + */ + const T& back() const { + Assert(!empty(), "CDQueue::back() called on empty list"); + return CDList::d_list[CDList::d_size - 1]; } };/* class CDQueue<> */ diff --git a/src/context/cdqueue2.h b/src/context/cdqueue2.h deleted file mode 100644 index bbff932d4..000000000 --- a/src/context/cdqueue2.h +++ /dev/null @@ -1,147 +0,0 @@ -/********************* */ -/*! \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 CDQueue2 : public CDList { -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& l): - CDList(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(*this); - // We save the d_size in d_lastsave and we should never destruct below this - // indices before the corresponding restore. - d_lastsave = CDList::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* qdata = ((CDQueue2*)data); - d_iter = qdata->d_iter; - d_lastsave = qdata->d_lastsave; - CDList::restore(data); - } - - - -public: - - /** Creates a new CDQueue associated with the current context. */ - CDQueue2(Context* context) - : CDList(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::d_size; - } - - bool size() const{ - return d_iter - CDList::d_size; - } - - /** Enqueues an element in the current context. */ - void push(const T& data){ - CDList::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::makeCurrent(); - d_iter = d_iter + 1; - if (d_iter == CDList::d_size && d_lastsave != CDList::d_size) { - // Some elements have been enqueued and dequeued in the same - // context and now the queue is empty we can destruct them. - CDList::removeLastUntil(d_lastsave); - d_iter = CDList::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::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::d_list[CDList::d_size - 1]; - } - -};/* class CDQueue<> */ - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__CONTEXT__CDQUEUE_H */ diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h new file mode 100644 index 000000000..3f6887d29 --- /dev/null +++ b/src/context/cdtrail_queue.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file cdtrail_queue.h + ** \verbatim + ** Original author: taking + ** 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 with an explicit trail of elements + ** + ** Context-dependent First-In-First-Out queue class. + ** The implementation is based on a combination of CDList and a CDO + ** for tracking the next element to dequeue from the list. + ** The implementation is currently not full featured. + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDTRAIL_QUEUE_H +#define __CVC4__CONTEXT__CDTRAIL_QUEUE_H + +#include "context/context.h" +#include "context/cdlist.h" + +namespace CVC4 { +namespace context { + + +template +class CDTrailQueue { +private: + + /** List of elements in the queue. */ + CDList d_list; + + /** Points to the next element in the current context to dequeue. */ + CDO d_iter; + + +public: + + /** Creates a new CDTrailQueue associated with the current context. */ + CDTrailQueue(Context* context) + : d_list(context), + d_iter(context, 0) + {} + + /** Returns true if the queue is empty in the current context. */ + bool empty() const{ + return d_iter >= d_list.size(); + } + + /** + * Enqueues an element in the current context. + * Returns its index in the queue. + */ + size_t enqueue(const T& data){ + size_t res = d_list.size(); + d_list.push_back(data); + return res; + } + + size_t frontIndex() const{ + return d_iter; + } + + const T& front() const{ + return d_list[frontIndex()]; + } + + /** Moves the iterator for the queue forward. */ + void dequeue(){ + Assert(!empty(), "Attempting to queue from an empty queue."); + d_iter = d_iter + 1; + } + + const T& operator[](size_t index){ + Assert(index < d_list.size()); + return d_list[index]; + } + +};/* class CDTrailQueue<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDTRAIL_QUEUE_H */ diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp index b0ea55dec..b67240d4c 100644 --- a/src/theory/arith/difference_manager.cpp +++ b/src/theory/arith/difference_manager.cpp @@ -91,7 +91,8 @@ void DifferenceManager::addAssertionToEqualityEngine(bool eq, ArithVar s, TNode void DifferenceManager::dequeueLiterals(){ Assert(d_hasSharedTerms); while(!d_literalsQueue.empty()){ - const LiteralsQueueElem& front = d_literalsQueue.dequeue(); + const LiteralsQueueElem& front = d_literalsQueue.front(); + d_literalsQueue.dequeue(); addAssertionToEqualityEngine(front.d_eq, front.d_var, front.d_reason); } diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h index d8a0e2c1c..46b070651 100644 --- a/src/theory/arith/difference_manager.h +++ b/src/theory/arith/difference_manager.h @@ -10,7 +10,7 @@ #include "context/cdo.h" #include "context/cdlist.h" #include "context/context.h" -#include "context/cdqueue.h" +#include "context/cdtrail_queue.h" #include "util/stats.h" #include "theory/arith/arith_prop_manager.h" @@ -62,7 +62,7 @@ private: }; /** Stores the queue of assertions. This keeps the Node backing the reasons */ - context::CDQueue d_literalsQueue; + context::CDTrailQueue d_literalsQueue; PropManager& d_queue; -- cgit v1.2.3