- 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.

5 files changed, 181 insertions, 134 deletions

diff --git a/src/context/cdlist_context_memory.h b/src/context/cdchunk_list.h
index fcb51fe20..e18d9b972 100644
--- a/src/context/cdlist_context_memory.h
+++ b/src/context/cdchunk_list.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file cdlist_context_memory.h
+/*! \file cdchunk_list.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -11,22 +11,21 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Context-dependent list class specialized for use with a
+ ** \brief Context-dependent list class designed for use with a
  ** context memory allocator.
  **
- ** Context-dependent list class specialized for use with a context
+ ** Context-dependent list class designed for use with a context
  ** memory allocator.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H
-#define __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H
+#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
+#define __CVC4__CONTEXT__CDCHUNK_LIST_H
 
 #include <iterator>
 #include <memory>
 
-#include "context/cdlist_forward.h"
 #include "context/context.h"
 #include "context/context_mm.h"
 #include "util/Assert.h"
@@ -37,17 +36,17 @@ namespace context {
 /**
  * Generic context-dependent dynamic array.  Like the usual CDList<>,
  * but allocates all memory from context memory.  Elements are kept in
- * cascading "list segments."  Access to elements is not O(1) but
+ * cascading "list segments."  Access to elements by operator[] is not O(1) but
  * O(log n).  As with CDList<>, update is not permitted, only
  * appending to the end of the list.
  */
 template <class T>
-class CDList<T, ContextMemoryAllocator<T> > : public ContextObj {
+class CDChunkList : public ContextObj {
 public:
 
-  /** The value type with which this CDList<> was instantiated. */
+  /** The value type with which this CDChunkList<> was instantiated. */
   typedef T value_type;
-  /** The allocator type with which this CDList<> was instantiated. */
+  /** The allocator type with which this CDChunkList<> was instantiated. */
   typedef ContextMemoryAllocator<T> Allocator;
 
 protected:
@@ -91,7 +90,7 @@ protected:
     const T* list() const { return d_list; }
     T& operator[](size_t i) { return d_list[i]; }
     const T& operator[](size_t i) const { return d_list[i]; }
-  };/* struct CDList<T, ContextMemoryAllocator<T> >::ListSegment */
+  };/* struct CDChunkList<T>::ListSegment */
 
   /**
    * The first segment of list memory.
@@ -126,12 +125,12 @@ protected:
   Allocator d_allocator;
 
   /**
-   * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >.
+   * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
    */
-  struct CDListSave : public ContextObj {
+  struct CDChunkListSave : public ContextObj {
     ListSegment* d_tail;
     size_t d_tailSize, d_size, d_sizeAlloc;
-    CDListSave(const CDList<T, Allocator>& list, ListSegment* tail,
+    CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
                size_t size, size_t sizeAlloc) :
       ContextObj(list),
       d_tail(tail),
@@ -139,7 +138,7 @@ protected:
       d_size(size),
       d_sizeAlloc(sizeAlloc) {
     }
-    ~CDListSave() {
+    ~CDChunkListSave() {
       this->destroy();
     }
     ContextObj* save(ContextMemoryManager* pCMM) {
@@ -152,12 +151,12 @@ protected:
       // itself saved or restored.
       Unreachable();
     }
-  };/* struct CDList<T, ContextMemoryAllocator<T> >::CDListSave */
+  };/* struct CDChunkList<T>::CDChunkListSave */
 
   /**
    * Private copy constructor undefined (no copy permitted).
    */
-  CDList(const CDList<T, Allocator>& l) CVC4_UNDEFINED;
+  CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
 
   /**
    * Allocate the first list segment.
@@ -225,7 +224,7 @@ protected:
    * The saved information is allocated using the ContextMemoryManager.
    */
   ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDListSave(*this, d_tailSegment,
+    ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment,
                                             d_size, d_totalSizeAlloc);
     Debug("cdlist:cmm") << "save " << this
                         << " at level " << this->getContext()->getLevel()
@@ -241,7 +240,7 @@ protected:
    * changed.
    */
   void restore(ContextObj* data) {
-    CDListSave* save = static_cast<CDListSave*>(data);
+    CDChunkListSave* save = static_cast<CDChunkListSave*>(data);
     Debug("cdlist:cmm") << "restore " << this
                         << " level " << this->getContext()->getLevel()
                         << " data == " << data
@@ -276,7 +275,7 @@ protected:
 
 public:
 
-  CDList(Context* context, bool callDestructor, const Allocator& alloc) :
+  CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) :
     ContextObj(context),
     d_headSegment(),
     d_tailSegment(&d_headSegment),
@@ -287,7 +286,7 @@ public:
     allocateHeadSegment();
   }
 
-  CDList(Context* context, bool callDestructor = true) :
+  CDChunkList(Context* context, bool callDestructor = true) :
     ContextObj(context),
     d_headSegment(),
     d_tailSegment(&d_headSegment),
@@ -298,7 +297,7 @@ public:
     allocateHeadSegment();
   }
 
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor,
+  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor,
          const Allocator& alloc) :
     ContextObj(allocatedInCMM, context),
     d_headSegment(),
@@ -310,7 +309,7 @@ public:
     allocateHeadSegment();
   }
 
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
     ContextObj(allocatedInCMM, context),
     d_headSegment(),
     d_tailSegment(&d_headSegment),
@@ -324,7 +323,7 @@ public:
   /**
    * Destructor: delete the list
    */
-  ~CDList() throw(AssertionException) {
+  ~CDChunkList() throw(AssertionException) {
     this->destroy();
 
     if(this->d_callDestructor) {
@@ -394,10 +393,10 @@ public:
   }
 
   /**
-   * Access to the ith item in the list.
+   * Access to the ith item in the list in O(log n).
    */
   const T& operator[](size_t i) const {
-    Assert(i < d_size, "index out of bounds in CDList::operator[]");
+    Assert(i < d_size, "index out of bounds in CDChunkList::operator[]");
     const ListSegment* seg = &d_headSegment;
     while(i >= seg->size()) {
       i -= seg->size();
@@ -410,12 +409,12 @@ public:
    * Returns the most recent item added to the list.
    */
   const T& back() const {
-    Assert(d_size > 0, "CDList::back() called on empty list");
+    Assert(d_size > 0, "CDChunkList::back() called on empty list");
     return (*d_tailSegment)[d_tailSegment->size() - 1];
   }
 
   /**
-   * Iterator for CDList class.  It has to be const because we don't
+   * Iterator for CDChunkList class.  It has to be const because we don't
    * allow items in the list to be changed.  It's a straightforward
    * wrapper around a pointer.  Note that for efficiency, we implement
    * only prefix increment and decrement.  Also note that it's OK to
@@ -431,7 +430,7 @@ public:
       d_index(i) {
     }
 
-    friend class CDList<T, Allocator>;
+    friend class CDChunkList<T>;
 
   public:
 
@@ -470,7 +469,7 @@ public:
       ++(*this);
       return i;
     }
-  };/* class CDList<>::const_iterator */
+  };/* class CDChunkList<>::const_iterator */
 
   /**
    * Returns an iterator pointing to the first item in the list.
@@ -489,9 +488,9 @@ public:
   const_iterator end() const {
     return const_iterator(NULL, 0);
   }
-};/* class CDList<T, ContextMemoryAllocator<T> > */
+};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */
+#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index cb9be07d3..c22d617b0 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -32,6 +32,8 @@
 #include "context/cdlist_forward.h"
 #include "util/Assert.h"
 
+#include <boost/static_assert.hpp>
+
 namespace CVC4 {
 namespace context {
 
@@ -45,12 +47,15 @@ namespace context {
  * 2. T objects can safely be copied using their copy constructor,
  *    operator=, and memcpy.
  */
-template <class T, class AllocatorT>
+template <class T, class CleanUpT, class AllocatorT>
 class CDList : public ContextObj {
 public:
 
   /** The value type with which this CDList<> was instantiated. */
   typedef T value_type;
+
+  typedef CleanUpT CleanUp;
+
   /** The allocator type with which this CDList<> was instantiated. */
   typedef AllocatorT Allocator;
 
@@ -84,6 +89,11 @@ private:
   size_t d_sizeAlloc;
 
   /**
+   * The CleanUp functor.
+   */
+  CleanUp d_cleanUp;
+
+  /**
    * Our allocator.
    */
   Allocator d_allocator;
@@ -94,12 +104,13 @@ protected:
    * d_sizeAlloc are not copied: only the base class information and
    * d_size are needed in restore.
    */
-  CDList(const CDList<T, Allocator>& l) :
+  CDList(const CDList<T, CleanUp, Allocator>& l) :
     ContextObj(l),
     d_list(NULL),
     d_size(l.d_size),
     d_callDestructor(false),
     d_sizeAlloc(0),
+    d_cleanUp(l.d_cleanUp),
     d_allocator(l.d_allocator) {
     Debug("cdlist") << "copy ctor: " << this
                     << " from " << &l
@@ -157,7 +168,7 @@ private:
    * ContextMemoryManager.
    */
   ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDList<T, Allocator>(*this);
+    ContextObj* data = new(pCMM) CDList<T, CleanUp, Allocator>(*this);
     Debug("cdlist") << "save " << this
                     << " at level " << this->getContext()->getLevel()
                     << " size at " << this->d_size
@@ -179,7 +190,7 @@ protected:
                     << " data == " << data
                     << " call dtor == " << this->d_callDestructor
                     << " d_list == " << this->d_list << std::endl;
-    truncateList(((CDList<T, Allocator>*)data)->d_size);
+    truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
     Debug("cdlist") << "restore " << this
                     << " level " << this->getContext()->getLevel()
                     << " size back to " << this->d_size
@@ -200,6 +211,7 @@ protected:
     if(d_callDestructor) {
       while(d_size != size) {
         --d_size;
+        d_cleanUp(&d_list[d_size]);
         d_allocator.destroy(&d_list[d_size]);
       }
     } else {
@@ -213,26 +225,33 @@ public:
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
-  CDList(Context* context, bool callDestructor = true,
-         const Allocator& alloc = Allocator()) :
+  CDList(Context* context,
+            bool callDestructor = true,
+            const CleanUp& cleanup = CleanUp(),
+            const Allocator& alloc = Allocator()) :
     ContextObj(context),
     d_list(NULL),
     d_size(0),
     d_callDestructor(callDestructor),
     d_sizeAlloc(0),
+    d_cleanUp(cleanup),
     d_allocator(alloc) {
   }
 
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor = true,
-         const Allocator& alloc = Allocator()) :
+  CDList(bool allocatedInCMM,
+            Context* context,
+            bool callDestructor = true,
+            const CleanUp& cleanup = CleanUp(),
+            const Allocator& alloc = Allocator()) :
     ContextObj(allocatedInCMM, context),
     d_list(NULL),
     d_size(0),
     d_callDestructor(callDestructor),
     d_sizeAlloc(0),
+    d_cleanUp(cleanup),
     d_allocator(alloc) {
   }
 
@@ -243,9 +262,7 @@ public:
     this->destroy();
 
     if(this->d_callDestructor) {
-      for(size_t i = 0; i < this->d_size; ++i) {
-        this->d_allocator.destroy(&this->d_list[i]);
-      }
+      truncateList(0);
     }
 
     this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
@@ -332,7 +349,7 @@ public:
 
     const_iterator(T const* it) : d_it(it) {}
 
-    friend class CDList<T, Allocator>;
+    friend class CDList<T, CleanUp, Allocator>;
 
   public:
 
@@ -412,6 +429,23 @@ public:
   }
 };/* class CDList<> */
 
+
+template <class T, class CleanUp>
+class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
+  /* CDList is incompatible for use with a ContextMemoryAllocator.
+   * Consider using CDChunkList<T> instead.
+   *
+   * Explanation:
+   * If ContextMemoryAllocator is used and d_list grows at a deeper context level
+   * the reallocated will be reallocated in a context memory regaion that can be
+   * detroyed on pop. To support this, a full copy of d_list would have to be made.
+   * As this is unacceptable for performance in other situations, we do not do
+   * this.
+   */
+
+  BOOST_STATIC_ASSERT(sizeof(T) == 0);
+};
+
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index 90c439085..78557afd2 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -41,16 +41,18 @@ namespace __gnu_cxx {
 }/* __gnu_cxx namespace */
 
 namespace CVC4 {
-  namespace context {
-    template <class T>
-    class ContextMemoryAllocator;
+namespace context {
 
-    template <class T, class Allocator = std::allocator<T> >
-    class CDList;
+template <class T>
+class DefaultCleanUp {
+public:
+  inline void operator()(T* t) const{}
+};
 
-    template <class T>
-    class CDList<T, ContextMemoryAllocator<T> >;
-  }/* CVC4::context namespace */
+template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
+class CDList;
+
+}/* CVC4::context namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */
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<> */
diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index 49d1b67e9..9464f416b 100644
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -23,86 +23,79 @@
 #define __CVC4__CONTEXT__CDVECTOR_H
 
 #include "context/context.h"
-#include "context/cdo.h"
+#include "context/cdlist.h"
 #include "util/Assert.h"
-#include "util/dynamic_array.h"
+#include <vector>
+
 
 namespace CVC4 {
 namespace context {
 
-template <class T>
-struct UpdatableElement {
-public:
-  T d_data;
-  int d_contextLevelOfLastUpdate;
-
-  UpdatableElement(const T& data) :
-    d_data(data),
-    d_contextLevelOfLastUpdate(0) {
-  }
-};/* struct UpdatableElement<T> */
-
-template <class T>
-struct HistoryElement {
-public:
-  UpdatableElement<T> d_cached;
-  unsigned d_index;
-  HistoryElement(const UpdatableElement<T>& cache, unsigned index) :
-    d_cached(cache), d_index(index) {
-  }
-};/* struct HistoryElement<T> */
-
 
 /**
  * Generic context-dependent dynamic vector.
+ * This is quite different than CDList<T>.
  * It provides the ability to destructively update the i'th item.
- * Note that the size of the vector never decreases.
  *
- * This is quite different than CDList<T>.
+ * The back of the vector may only be popped if there have been no updates to it
+ * at this context level.
  */
 template <class T>
 class CDVector {
 private:
-  typedef DynamicArray< UpdatableElement<T> > CurrentVector;
-  typedef DynamicArray< HistoryElement<T> > HistoryVector;
+  static const int ImpossibleLevel = -1;
 
-  Context* d_context;
+  struct UpdatableElement {
+  public:
+    T d_data;
+    int d_contextLevelOfLastUpdate;
 
-  DynamicArray< UpdatableElement<T> > d_current;
-  DynamicArray< HistoryElement<T> > d_history;
+    UpdatableElement(const T& data) :
+      d_data(data),
+      d_contextLevelOfLastUpdate(ImpossibleLevel) {
+    }
+  };/* struct CDVector<T>::UpdatableElement */
+
+  struct HistoryElement {
+  public:
+    UpdatableElement d_cached;
+    size_t d_index;
+    HistoryElement(const UpdatableElement& cache, size_t index) :
+      d_cached(cache), d_index(index) {
+    }
+  };/* struct CDVector<T>::HistoryElement */
 
-  CDO<unsigned> d_historySize;
+  typedef std::vector< UpdatableElement > CurrentVector;
+  CurrentVector d_current;
 
-private:
-  void restoreConsistency() {
-    Assert(d_history.size() >= d_historySize.get());
-    while(d_history.size() > d_historySize.get()) {
-      const HistoryElement<T>& back = d_history.back();
-      d_current[back.d_index] = back.d_cached;
-      d_history.pop_back();
-    }
-  }
 
-  bool isConsistent() const {
-    return d_history.size() == d_historySize.get();
-  }
 
-  void makeConsistent() {
-    if(!isConsistent()) {
-      restoreConsistency();
+  class HistoryListCleanUp{
+  private:
+    CurrentVector& d_current;
+  public:
+    HistoryListCleanUp(CurrentVector& current)
+      : d_current(current)
+    {}
+
+    void operator()(HistoryElement* back){
+      d_current[back->d_index] = back->d_cached;
     }
-    Assert(isConsistent());
-  }
+  };/* class CDVector<T>::HistoryListCleanUp */
+
+  typedef CDList< HistoryElement,  HistoryListCleanUp > HistoryVector;
+  HistoryVector d_history;
+
+  Context* d_context;
 
 public:
-  CDVector(Context* c, bool callDestructor = false) :
-    d_context(c),
-    d_current(callDestructor),
-    d_history(callDestructor),
-    d_historySize(c, 0) {
-  }
+  CDVector(Context* c) :
+    d_current(),
+    d_history(c, true, HistoryListCleanUp(d_current)),
+    d_context(c)
+  {}
 
-  unsigned size() const {
+  size_t size() const {
     return d_current.size();
   }
 
@@ -118,37 +111,47 @@ public:
    * Assigns its state at level 0 to be equal to data.
    */
   void push_back(const T& data) {
-    d_current.push_back(UpdatableElement<T>(data));
+    d_current.push_back(UpdatableElement(data));
   }
 
   /**
    * Access to the ith item in the list.
    */
-  const T& operator[](unsigned i) {
+  const T& operator[](size_t i) const {
     return get(i);
   }
 
-  const T& get(unsigned i) {
+  const T& get(size_t i) const {
     Assert(i < size(), "index out of bounds in CDVector::get()");
-    makeConsistent();
+    //makeConsistent();
     return d_current[i].d_data;
   }
 
-  void set(unsigned index, const T& data) {
+  void set(size_t index, const T& data) {
     Assert(index < size(), "index out of bounds in CDVector::set()");
-    makeConsistent();
+    //makeConsistent();
 
     if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) {
       d_current[index].d_data = data;
     }else{
-      d_history.push_back(HistoryElement<T>(d_current[index], index));
-      d_historySize.set(d_historySize.get() + 1);
+      d_history.push_back(HistoryElement(d_current[index], index));
 
       d_current[index].d_data = data;
       d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel();
     }
   }
 
+  bool hasUpdates(size_t index) const {
+    Assert(index < size(), "index out of bounds in CDVector::hasUpdates()");
+    return d_current[index].d_contextLevelOfLastUpdate == ImpossibleLevel;
+  }
+
+  void pop_back() {
+    Assert(!empty(), "pop_back() on an empty CDVector");
+    Assert(!hasUpdates(size() - 1), "popping an element with updates.");
+    d_current.pop_back();
+  }
+
 };/* class CDVector<T> */
 
 }/* CVC4::context namespace */