Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function names and documentation.

5 files changed, 219 insertions, 189 deletions

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,15 +56,22 @@ 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
    * second argument in the constructor to false.
@@ -72,11 +79,6 @@ protected:
   bool d_callDestructor;
 
   /**
-   * Number of objects in d_list
-   */
-  size_t d_size;
-
-  /**
    * Allocated size of d_list.
    */
   size_t d_sizeAlloc;
@@ -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<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
@@ -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<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;
     }
   }
 
@@ -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<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.
  **/
 
 
@@ -31,42 +34,111 @@
 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<> */
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 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 */
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<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 */