cdlist_context_memory.h \
cdlist_forward.h \
cdqueue.h \
- cdqueue2.h \
+ cdtrail_queue.h \
cdmap.h \
cdmap_forward.h \
cdset.h \
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
*/
bool d_callDestructor;
- /**
- * Number of objects in d_list
- */
- size_t d_size;
-
/**
* Allocated size of d_list.
*/
*/
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
CDList(const CDList<T, Allocator>& 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
<< " size " << d_size << std::endl;
}
+private:
/**
* Reallocate the array with more space.
* Throws bad_alloc if memory allocation fails.
return data;
}
+protected:
/**
* Implementation of mandatory ContextObj method restore: simply
* restores the previous size. Note that the list pointer and the
<< " data == " << data
<< " call dtor == " << this->d_callDestructor
<< " d_list == " << this->d_list << std::endl;
- removeLastUntil(((CDList<T, Allocator>*)data)->d_size);
+ truncateList(((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.
+ /**
+ * 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;
}
}
const Allocator& alloc = Allocator()) :
ContextObj(context),
d_list(NULL),
- d_callDestructor(callDestructor),
d_size(0),
+ d_callDestructor(callDestructor),
d_sizeAlloc(0),
d_allocator(alloc) {
}
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) {
}
/********************* */
/*! \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.
** \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<size_t>
- ** 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.
**/
namespace CVC4 {
namespace context {
-
+/** We don't define a template with Allocator for the first implementation */
template <class T>
-class CDQueue {
-private:
-
- /** List of elements in the queue. */
- CDList<T> d_list;
+class CDQueue : public CDList<T> {
+protected:
/** Points to the next element in the current context to dequeue. */
- CDO<size_t> 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<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) 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;
+ 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<T>* qdata = ((CDQueue<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. */
CDQueue(Context* context)
- : d_list(context),
- d_iter(context, 0)
+ : 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 >= d_list.size();
+ return d_iter >= CDList<T>::d_size;
+ }
+
+ /** Returns the number of elements that have not been dequeued in the context. */
+ size_t size() const{
+ return d_iter - CDList<T>::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<T>::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<T>::makeCurrent();
d_iter = d_iter + 1;
- return d_list[front];
+ 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>::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<T>::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<T>::d_list[CDList<T>::d_size - 1];
}
};/* class CDQueue<> */
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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<size_t>
+ ** 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 T>
+class CDTrailQueue {
+private:
+
+ /** List of elements in the queue. */
+ CDList<T> d_list;
+
+ /** Points to the next element in the current context to dequeue. */
+ CDO<size_t> 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 */
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);
}
#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"
};
/** Stores the queue of assertions. This keeps the Node backing the reasons */
- context::CDQueue<LiteralsQueueElem> d_literalsQueue;
+ context::CDTrailQueue<LiteralsQueueElem> d_literalsQueue;
PropManager& d_queue;
projects / cvc5.git / commitdiff