From: Tim King <taking@cs.nyu.edu>
Date: Mon, 2 Apr 2012 20:56:55 +0000 (+0000)
Subject: - Merged in the branch cdlist-cleanup.
X-Git-Tag: cvc5-1.0.0~8246
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a558a30bec496444742ed75c0a6973d9789daf7;p=cvc5.git

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

diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
new file mode 100644
index 000000000..e18d9b972
--- /dev/null
+++ b/src/context/cdchunk_list.h
@@ -0,0 +1,496 @@
+/*********************                                                        */
+/*! \file cdchunk_list.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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 list class designed for use with a
+ ** context memory allocator.
+ **
+ ** Context-dependent list class designed for use with a context
+ ** memory allocator.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
+#define __CVC4__CONTEXT__CDCHUNK_LIST_H
+
+#include <iterator>
+#include <memory>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+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 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 CDChunkList : public ContextObj {
+public:
+
+  /** The value type with which this CDChunkList<> was instantiated. */
+  typedef T value_type;
+  /** The allocator type with which this CDChunkList<> was instantiated. */
+  typedef ContextMemoryAllocator<T> Allocator;
+
+protected:
+
+  static const size_t INITIAL_SEGMENT_SIZE = 10;
+  static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
+
+  /**
+   * ListSegment is itself allocated in Context memory, but it is
+   * never updated; it serves as information about the d_list segment
+   * pointer it contains only.
+   */
+  class ListSegment {
+    ListSegment* d_nextSegment;
+    size_t d_segmentSize;
+    T* d_list;
+  public:
+    ListSegment() :
+      d_nextSegment(NULL),
+      d_segmentSize(0),
+      d_list(NULL) {
+    }
+    void initialize(T* list) {
+      Assert( d_nextSegment == NULL &&
+              d_segmentSize == 0 &&
+              d_list == NULL,
+              "Double-initialization of ListSegment not permitted" );
+      d_list = list;
+    }
+    void linkTo(ListSegment* nextSegment) {
+      Assert( d_nextSegment == NULL,
+              "Double-linking of ListSegment not permitted" );
+      d_nextSegment = nextSegment;
+    }
+    void cutLink() {
+      d_nextSegment = NULL;
+    }
+    ListSegment* getNextSegment() const { return d_nextSegment; }
+    size_t& size() { return d_segmentSize; }
+    size_t size() const { return d_segmentSize; }
+    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 CDChunkList<T>::ListSegment */
+
+  /**
+   * The first segment of list memory.
+   */
+  ListSegment d_headSegment;
+
+  /**
+   * A pointer to the final segment of list memory.
+   */
+  ListSegment* d_tailSegment;
+
+  /**
+   * 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.
+   */
+  bool d_callDestructor;
+
+  /**
+   * Number of objects in list across all segments.
+   */
+  size_t d_size;
+
+  /**
+   * Total allocated size across all segments.
+   */
+  size_t d_totalSizeAlloc;
+
+  /**
+   * Our allocator.
+   */
+  Allocator d_allocator;
+
+  /**
+   * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
+   */
+  struct CDChunkListSave : public ContextObj {
+    ListSegment* d_tail;
+    size_t d_tailSize, d_size, d_sizeAlloc;
+    CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
+               size_t size, size_t sizeAlloc) :
+      ContextObj(list),
+      d_tail(tail),
+      d_tailSize(tail->size()),
+      d_size(size),
+      d_sizeAlloc(sizeAlloc) {
+    }
+    ~CDChunkListSave() {
+      this->destroy();
+    }
+    ContextObj* save(ContextMemoryManager* pCMM) {
+      // This type of object _is_ the save/restore object.  It isn't
+      // itself saved or restored.
+      Unreachable();
+    }
+    void restore(ContextObj* data) {
+      // This type of object _is_ the save/restore object.  It isn't
+      // itself saved or restored.
+      Unreachable();
+    }
+  };/* struct CDChunkList<T>::CDChunkListSave */
+
+  /**
+   * Private copy constructor undefined (no copy permitted).
+   */
+  CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
+
+  /**
+   * Allocate the first list segment.
+   */
+  void allocateHeadSegment() {
+    Assert(d_headSegment.list() == NULL);
+    Assert(d_totalSizeAlloc == 0 && d_size == 0);
+
+    // Allocate an initial list if one does not yet exist
+    size_t newSize = INITIAL_SEGMENT_SIZE;
+    Debug("cdlist:cmm") << "initial grow of cdlist " << this
+                        << " level " << getContext()->getLevel()
+                        << " to " << newSize << std::endl;
+    if(newSize > d_allocator.max_size()) {
+      newSize = d_allocator.max_size();
+    }
+    T* newList = d_allocator.allocate(newSize);
+    if(newList == NULL) {
+      throw std::bad_alloc();
+    }
+    d_totalSizeAlloc = newSize;
+    d_headSegment.initialize(newList);
+  }
+
+  /**
+   * Allocate a new segment with more space.
+   * Throws bad_alloc if memory allocation fails.
+   */
+  void grow() {
+    Assert(d_totalSizeAlloc == d_size);
+
+    // Allocate a new segment
+    typedef typename Allocator::template rebind<ListSegment>::other
+      SegmentAllocator;
+    ContextMemoryManager* cmm = d_allocator.getCMM();
+    SegmentAllocator segAllocator = SegmentAllocator(cmm);
+    ListSegment* newSegment = segAllocator.allocate(1);
+    if(newSegment == NULL) {
+      throw std::bad_alloc();
+    }
+    segAllocator.construct(newSegment, ListSegment());
+    size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
+    if(newSize > d_allocator.max_size()) {
+      newSize = d_allocator.max_size();
+    }
+    T* newList = d_allocator.allocate(newSize);
+    Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
+                        << " level " << getContext()->getLevel()
+                        << " to " << newSize
+                        << " (from " << d_tailSegment->list()
+                        << " to " << newList << ")" << std::endl;
+    if(newList == NULL) {
+      throw std::bad_alloc();
+    }
+    d_tailSegment->linkTo(newSegment);
+    d_tailSegment = newSegment;
+    d_tailSegment->initialize(newList);
+    d_totalSizeAlloc += newSize;
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current size to a copy using the copy constructor (the pointer and the
+   * allocated size are *not* copied as they are not restored on a pop).
+   * The saved information is allocated using the ContextMemoryManager.
+   */
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment,
+                                            d_size, d_totalSizeAlloc);
+    Debug("cdlist:cmm") << "save " << this
+                        << " at level " << this->getContext()->getLevel()
+                        << " size at " << this->d_size
+                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
+                        << " data:" << data << std::endl;
+    return data;
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method restore: simply restores the
+   * previous size.  Note that the list pointer and the allocated size are not
+   * changed.
+   */
+  void restore(ContextObj* data) {
+    CDChunkListSave* save = static_cast<CDChunkListSave*>(data);
+    Debug("cdlist:cmm") << "restore " << this
+                        << " level " << this->getContext()->getLevel()
+                        << " data == " << data
+                        << " call dtor == " << this->d_callDestructor
+                        << " d_tail == " << this->d_tailSegment << std::endl;
+    if(this->d_callDestructor) {
+      ListSegment* seg = &d_headSegment;
+      size_t i = save->d_size;
+      while(i >= seg->size()) {
+        i -= seg->size();
+        seg = seg->getNextSegment();
+      }
+      do {
+        while(i < seg->size()) {
+          this->d_allocator.destroy(&(*seg)[i++]);
+        }
+        i = 0;
+      } while((seg = seg->getNextSegment()) != NULL);
+    }
+
+    this->d_size = save->d_size;
+    this->d_tailSegment = save->d_tail;
+    this->d_tailSegment->size() = save->d_tailSize;
+    this->d_tailSegment->cutLink();
+    this->d_totalSizeAlloc = save->d_sizeAlloc;
+    Debug("cdlist:cmm") << "restore " << this
+                        << " level " << this->getContext()->getLevel()
+                        << " size back to " << this->d_size
+                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
+                        << std::endl;
+  }
+
+public:
+
+  CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) :
+    ContextObj(context),
+    d_headSegment(),
+    d_tailSegment(&d_headSegment),
+    d_callDestructor(callDestructor),
+    d_size(0),
+    d_totalSizeAlloc(0),
+    d_allocator(alloc) {
+    allocateHeadSegment();
+  }
+
+  CDChunkList(Context* context, bool callDestructor = true) :
+    ContextObj(context),
+    d_headSegment(),
+    d_tailSegment(&d_headSegment),
+    d_callDestructor(callDestructor),
+    d_size(0),
+    d_totalSizeAlloc(0),
+    d_allocator(Allocator(context->getCMM())) {
+    allocateHeadSegment();
+  }
+
+  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor,
+         const Allocator& alloc) :
+    ContextObj(allocatedInCMM, context),
+    d_headSegment(),
+    d_tailSegment(&d_headSegment),
+    d_callDestructor(callDestructor),
+    d_size(0),
+    d_totalSizeAlloc(0),
+    d_allocator(alloc) {
+    allocateHeadSegment();
+  }
+
+  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+    ContextObj(allocatedInCMM, context),
+    d_headSegment(),
+    d_tailSegment(&d_headSegment),
+    d_callDestructor(callDestructor),
+    d_size(0),
+    d_totalSizeAlloc(0),
+    d_allocator(Allocator(context->getCMM())) {
+    allocateHeadSegment();
+  }
+
+  /**
+   * Destructor: delete the list
+   */
+  ~CDChunkList() throw(AssertionException) {
+    this->destroy();
+
+    if(this->d_callDestructor) {
+      for(ListSegment* segment = &d_headSegment;
+          segment != NULL;
+          segment = segment->getNextSegment()) {
+        for(size_t i = 0; i < segment->size(); ++i) {
+          this->d_allocator.destroy(&(*segment)[i]);
+        }
+      }
+    }
+  }
+
+  /**
+   * Return the current size of (i.e. valid number of objects in) the
+   * list.
+   */
+  size_t size() const {
+    return d_size;
+  }
+
+  /**
+   * Return true iff there are no valid objects in the list.
+   */
+  bool empty() const {
+    return d_size == 0;
+  }
+
+  /**
+   * Add an item to the end of the list.
+   */
+  void push_back(const T& data) {
+    Debug("cdlist:cmm") << "push_back " << this
+                        << " level " << getContext()->getLevel()
+                        << ": make-current, "
+                        << "d_list == " << d_tailSegment->list() << std::endl;
+    makeCurrent();
+
+    Debug("cdlist:cmm") << "push_back " << this
+                        << " level " << getContext()->getLevel()
+                        << ": grow? " << d_size
+                        << " size_alloc " << d_totalSizeAlloc
+                        << std::endl;
+
+    if(d_size == d_totalSizeAlloc) {
+      Debug("cdlist:cmm") << "push_back " << this
+                          << " " << getContext()->getLevel()
+                          << ": grow!\n";
+      grow();
+    }
+    Assert(d_size < d_totalSizeAlloc);
+
+    Debug("cdlist:cmm") << "push_back " << this
+                        << " " << getContext()->getLevel()
+                        << ": construct! at [" << d_size << "] == "
+                        << &(*d_tailSegment)[d_tailSegment->size()]
+                        << std::endl;
+    d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
+    Debug("cdlist:cmm") << "push_back " << this
+                        << " " << getContext()->getLevel()
+                        << ": done..." << std::endl;
+    ++d_tailSegment->size();
+    ++d_size;
+    Debug("cdlist:cmm") << "push_back " << this
+                        << " " << getContext()->getLevel()
+                        << ": size now " << d_size << std::endl;
+  }
+
+  /**
+   * 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 CDChunkList::operator[]");
+    const ListSegment* seg = &d_headSegment;
+    while(i >= seg->size()) {
+      i -= seg->size();
+      seg = seg->getNextSegment();
+    }
+    return (*seg)[i];
+  }
+
+  /**
+   * Returns the most recent item added to the list.
+   */
+  const T& back() const {
+    Assert(d_size > 0, "CDChunkList::back() called on empty list");
+    return (*d_tailSegment)[d_tailSegment->size() - 1];
+  }
+
+  /**
+   * 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
+   * create an iterator from an empty, uninitialized list, as begin()
+   * and end() will have the same value (NULL).
+   */
+  class const_iterator {
+    const ListSegment* d_segment;
+    size_t d_index;
+
+    const_iterator(const ListSegment* segment, size_t i) :
+      d_segment(segment),
+      d_index(i) {
+    }
+
+    friend class CDChunkList<T>;
+
+  public:
+
+    typedef std::input_iterator_tag iterator_category;
+    typedef T value_type;
+    typedef std::ptrdiff_t difference_type;
+    typedef const T* pointer;
+    typedef const T& reference;
+
+    const_iterator() : d_segment(NULL), d_index(0) {}
+
+    inline bool operator==(const const_iterator& i) const {
+      return d_segment == i.d_segment && d_index == i.d_index;
+    }
+
+    inline bool operator!=(const const_iterator& i) const {
+      return !(*this == i);
+    }
+
+    inline const T& operator*() const {
+      return (*d_segment)[d_index];
+    }
+
+    /** Prefix increment */
+    const_iterator& operator++() {
+      if(++d_index >= d_segment->size()) {
+        d_segment = d_segment->getNextSegment();
+        d_index = 0;
+      }
+      return *this;
+    }
+
+    /** Postfix increment: returns new iterator with the old value. */
+    const_iterator operator++(int) {
+      const_iterator i = *this;
+      ++(*this);
+      return i;
+    }
+  };/* class CDChunkList<>::const_iterator */
+
+  /**
+   * Returns an iterator pointing to the first item in the list.
+   */
+  const_iterator begin() const {
+    // This looks curious, but we have to make sure that begin() == end()
+    // for an empty list, and begin() == (head,0) for a nonempty one.
+    // Since the segment spill-over is implemented in
+    // iterator::operator++(), let's reuse it. */
+    return ++const_iterator(&d_headSegment, -1);
+  }
+
+  /**
+   * Returns an iterator pointing one past the last item in the list.
+   */
+  const_iterator end() const {
+    return const_iterator(NULL, 0);
+  }
+};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#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;
 
@@ -83,6 +88,11 @@ private:
    */
   size_t d_sizeAlloc;
 
+  /**
+   * The CleanUp functor.
+   */
+  CleanUp d_cleanUp;
+
   /**
    * Our 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_context_memory.h b/src/context/cdlist_context_memory.h
deleted file mode 100644
index fcb51fe20..000000000
--- a/src/context/cdlist_context_memory.h
+++ /dev/null
@@ -1,497 +0,0 @@
-/*********************                                                        */
-/*! \file cdlist_context_memory.h
- ** \verbatim
- ** Original author: mdeters
- ** 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 list class specialized for use with a
- ** context memory allocator.
- **
- ** Context-dependent list class specialized 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
-
-#include <iterator>
-#include <memory>
-
-#include "context/cdlist_forward.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "util/Assert.h"
-
-namespace CVC4 {
-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
- * 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 {
-public:
-
-  /** The value type with which this CDList<> was instantiated. */
-  typedef T value_type;
-  /** The allocator type with which this CDList<> was instantiated. */
-  typedef ContextMemoryAllocator<T> Allocator;
-
-protected:
-
-  static const size_t INITIAL_SEGMENT_SIZE = 10;
-  static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
-
-  /**
-   * ListSegment is itself allocated in Context memory, but it is
-   * never updated; it serves as information about the d_list segment
-   * pointer it contains only.
-   */
-  class ListSegment {
-    ListSegment* d_nextSegment;
-    size_t d_segmentSize;
-    T* d_list;
-  public:
-    ListSegment() :
-      d_nextSegment(NULL),
-      d_segmentSize(0),
-      d_list(NULL) {
-    }
-    void initialize(T* list) {
-      Assert( d_nextSegment == NULL &&
-              d_segmentSize == 0 &&
-              d_list == NULL,
-              "Double-initialization of ListSegment not permitted" );
-      d_list = list;
-    }
-    void linkTo(ListSegment* nextSegment) {
-      Assert( d_nextSegment == NULL,
-              "Double-linking of ListSegment not permitted" );
-      d_nextSegment = nextSegment;
-    }
-    void cutLink() {
-      d_nextSegment = NULL;
-    }
-    ListSegment* getNextSegment() const { return d_nextSegment; }
-    size_t& size() { return d_segmentSize; }
-    size_t size() const { return d_segmentSize; }
-    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 */
-
-  /**
-   * The first segment of list memory.
-   */
-  ListSegment d_headSegment;
-
-  /**
-   * A pointer to the final segment of list memory.
-   */
-  ListSegment* d_tailSegment;
-
-  /**
-   * 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.
-   */
-  bool d_callDestructor;
-
-  /**
-   * Number of objects in list across all segments.
-   */
-  size_t d_size;
-
-  /**
-   * Total allocated size across all segments.
-   */
-  size_t d_totalSizeAlloc;
-
-  /**
-   * Our allocator.
-   */
-  Allocator d_allocator;
-
-  /**
-   * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >.
-   */
-  struct CDListSave : public ContextObj {
-    ListSegment* d_tail;
-    size_t d_tailSize, d_size, d_sizeAlloc;
-    CDListSave(const CDList<T, Allocator>& list, ListSegment* tail,
-               size_t size, size_t sizeAlloc) :
-      ContextObj(list),
-      d_tail(tail),
-      d_tailSize(tail->size()),
-      d_size(size),
-      d_sizeAlloc(sizeAlloc) {
-    }
-    ~CDListSave() {
-      this->destroy();
-    }
-    ContextObj* save(ContextMemoryManager* pCMM) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-    void restore(ContextObj* data) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-  };/* struct CDList<T, ContextMemoryAllocator<T> >::CDListSave */
-
-  /**
-   * Private copy constructor undefined (no copy permitted).
-   */
-  CDList(const CDList<T, Allocator>& l) CVC4_UNDEFINED;
-
-  /**
-   * Allocate the first list segment.
-   */
-  void allocateHeadSegment() {
-    Assert(d_headSegment.list() == NULL);
-    Assert(d_totalSizeAlloc == 0 && d_size == 0);
-
-    // Allocate an initial list if one does not yet exist
-    size_t newSize = INITIAL_SEGMENT_SIZE;
-    Debug("cdlist:cmm") << "initial grow of cdlist " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize << std::endl;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_totalSizeAlloc = newSize;
-    d_headSegment.initialize(newList);
-  }
-
-  /**
-   * Allocate a new segment with more space.
-   * Throws bad_alloc if memory allocation fails.
-   */
-  void grow() {
-    Assert(d_totalSizeAlloc == d_size);
-
-    // Allocate a new segment
-    typedef typename Allocator::template rebind<ListSegment>::other
-      SegmentAllocator;
-    ContextMemoryManager* cmm = d_allocator.getCMM();
-    SegmentAllocator segAllocator = SegmentAllocator(cmm);
-    ListSegment* newSegment = segAllocator.allocate(1);
-    if(newSegment == NULL) {
-      throw std::bad_alloc();
-    }
-    segAllocator.construct(newSegment, ListSegment());
-    size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize
-                        << " (from " << d_tailSegment->list()
-                        << " to " << newList << ")" << std::endl;
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_tailSegment->linkTo(newSegment);
-    d_tailSegment = newSegment;
-    d_tailSegment->initialize(newList);
-    d_totalSizeAlloc += newSize;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current size to a copy using the copy constructor (the pointer and the
-   * allocated size are *not* copied as they are not restored on a pop).
-   * The saved information is allocated using the ContextMemoryManager.
-   */
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDListSave(*this, d_tailSegment,
-                                            d_size, d_totalSizeAlloc);
-    Debug("cdlist:cmm") << "save " << this
-                        << " at level " << this->getContext()->getLevel()
-                        << " size at " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << " data:" << data << std::endl;
-    return data;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply restores the
-   * previous size.  Note that the list pointer and the allocated size are not
-   * changed.
-   */
-  void restore(ContextObj* data) {
-    CDListSave* save = static_cast<CDListSave*>(data);
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " data == " << data
-                        << " call dtor == " << this->d_callDestructor
-                        << " d_tail == " << this->d_tailSegment << std::endl;
-    if(this->d_callDestructor) {
-      ListSegment* seg = &d_headSegment;
-      size_t i = save->d_size;
-      while(i >= seg->size()) {
-        i -= seg->size();
-        seg = seg->getNextSegment();
-      }
-      do {
-        while(i < seg->size()) {
-          this->d_allocator.destroy(&(*seg)[i++]);
-        }
-        i = 0;
-      } while((seg = seg->getNextSegment()) != NULL);
-    }
-
-    this->d_size = save->d_size;
-    this->d_tailSegment = save->d_tail;
-    this->d_tailSegment->size() = save->d_tailSize;
-    this->d_tailSegment->cutLink();
-    this->d_totalSizeAlloc = save->d_sizeAlloc;
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " size back to " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << std::endl;
-  }
-
-public:
-
-  CDList(Context* context, bool callDestructor, const Allocator& alloc) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDList(Context* context, bool callDestructor = true) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor,
-         const Allocator& alloc) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  /**
-   * Destructor: delete the list
-   */
-  ~CDList() throw(AssertionException) {
-    this->destroy();
-
-    if(this->d_callDestructor) {
-      for(ListSegment* segment = &d_headSegment;
-          segment != NULL;
-          segment = segment->getNextSegment()) {
-        for(size_t i = 0; i < segment->size(); ++i) {
-          this->d_allocator.destroy(&(*segment)[i]);
-        }
-      }
-    }
-  }
-
-  /**
-   * Return the current size of (i.e. valid number of objects in) the
-   * list.
-   */
-  size_t size() const {
-    return d_size;
-  }
-
-  /**
-   * Return true iff there are no valid objects in the list.
-   */
-  bool empty() const {
-    return d_size == 0;
-  }
-
-  /**
-   * Add an item to the end of the list.
-   */
-  void push_back(const T& data) {
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": make-current, "
-                        << "d_list == " << d_tailSegment->list() << std::endl;
-    makeCurrent();
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": grow? " << d_size
-                        << " size_alloc " << d_totalSizeAlloc
-                        << std::endl;
-
-    if(d_size == d_totalSizeAlloc) {
-      Debug("cdlist:cmm") << "push_back " << this
-                          << " " << getContext()->getLevel()
-                          << ": grow!\n";
-      grow();
-    }
-    Assert(d_size < d_totalSizeAlloc);
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": construct! at [" << d_size << "] == "
-                        << &(*d_tailSegment)[d_tailSegment->size()]
-                        << std::endl;
-    d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": done..." << std::endl;
-    ++d_tailSegment->size();
-    ++d_size;
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": size now " << d_size << std::endl;
-  }
-
-  /**
-   * Access to the ith item in the list.
-   */
-  const T& operator[](size_t i) const {
-    Assert(i < d_size, "index out of bounds in CDList::operator[]");
-    const ListSegment* seg = &d_headSegment;
-    while(i >= seg->size()) {
-      i -= seg->size();
-      seg = seg->getNextSegment();
-    }
-    return (*seg)[i];
-  }
-
-  /**
-   * Returns the most recent item added to the list.
-   */
-  const T& back() const {
-    Assert(d_size > 0, "CDList::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
-   * 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
-   * create an iterator from an empty, uninitialized list, as begin()
-   * and end() will have the same value (NULL).
-   */
-  class const_iterator {
-    const ListSegment* d_segment;
-    size_t d_index;
-
-    const_iterator(const ListSegment* segment, size_t i) :
-      d_segment(segment),
-      d_index(i) {
-    }
-
-    friend class CDList<T, Allocator>;
-
-  public:
-
-    typedef std::input_iterator_tag iterator_category;
-    typedef T value_type;
-    typedef std::ptrdiff_t difference_type;
-    typedef const T* pointer;
-    typedef const T& reference;
-
-    const_iterator() : d_segment(NULL), d_index(0) {}
-
-    inline bool operator==(const const_iterator& i) const {
-      return d_segment == i.d_segment && d_index == i.d_index;
-    }
-
-    inline bool operator!=(const const_iterator& i) const {
-      return !(*this == i);
-    }
-
-    inline const T& operator*() const {
-      return (*d_segment)[d_index];
-    }
-
-    /** Prefix increment */
-    const_iterator& operator++() {
-      if(++d_index >= d_segment->size()) {
-        d_segment = d_segment->getNextSegment();
-        d_index = 0;
-      }
-      return *this;
-    }
-
-    /** Postfix increment: returns new iterator with the old value. */
-    const_iterator operator++(int) {
-      const_iterator i = *this;
-      ++(*this);
-      return i;
-    }
-  };/* class CDList<>::const_iterator */
-
-  /**
-   * Returns an iterator pointing to the first item in the list.
-   */
-  const_iterator begin() const {
-    // This looks curious, but we have to make sure that begin() == end()
-    // for an empty list, and begin() == (head,0) for a nonempty one.
-    // Since the segment spill-over is implemented in
-    // iterator::operator++(), let's reuse it. */
-    return ++const_iterator(&d_headSegment, -1);
-  }
-
-  /**
-   * Returns an iterator pointing one past the last item in the list.
-   */
-  const_iterator end() const {
-    return const_iterator(NULL, 0);
-  }
-};/* class CDList<T, ContextMemoryAllocator<T> > */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */
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 */
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 7a2a97726..7e2211595 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -74,10 +74,10 @@ public:
     d_hasSafeAssignment(),
     d_assignment(),
     d_safeAssignment(),
-    d_upperBound(c, true),
-    d_lowerBound(c, true),
-    d_upperConstraint(c,true),
-    d_lowerConstraint(c,true),
+    d_upperBound(c),
+    d_lowerBound(c),
+    d_upperConstraint(c),
+    d_lowerConstraint(c),
     d_deltaIsSafe(false),
     d_delta(-1,1),
     d_history(),
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index fcb6ee382..dcae47dc7 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -151,7 +151,7 @@ private:
   void notifyCongruent(TNode a, TNode b);
 
 
-  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
+  typedef context::CDChunkList<TNode> CTNodeListAlloc;
   typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
   typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 921df028e..281b11a93 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -39,9 +39,9 @@ namespace datatypes {
 
 class TheoryDatatypes : public Theory {
 private:
-  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList;
+  typedef context::CDChunkList<TNode> EqList;
   typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists;
-  typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN;
+  typedef context::CDChunkList<Node> EqListN;
   typedef context::CDHashMap<Node, EqListN*, NodeHashFunction> EqListsN;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index ed1cecd7b..d7b8b0a22 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -32,7 +32,7 @@
 #include "context/cdo.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
-#include "context/cdlist_context_memory.h"
+#include "context/cdchunk_list.h"
 #include "util/exception.h"
 #include "context/stacking_map.h"
 #include "util/stats.h"
@@ -140,9 +140,9 @@ class CongruenceClosure {
 
   // typedef all of these so that iterators are easy to define
   typedef context::StackingMap<Node, Node, NodeHashFunction> RepresentativeMap;
-  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
+  typedef context::CDChunkList<TNode> ClassList;
   typedef context::CDHashMap<Node, ClassList*, NodeHashFunction> ClassLists;
-  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
+  typedef context::CDChunkList<TNode> UseList;
   typedef context::CDHashMap<TNode, UseList*, TNodeHashFunction> UseLists;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> LookupMap;
 
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index fcc6a7e55..ccdbb210b 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -28,7 +28,6 @@
 #include "util/exception.h"
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdlist_context_memory.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -58,12 +57,12 @@ public:
 
   // test at different sizes.  this triggers grow() behavior differently.
   // grow() was completely broken in revision 256
-  void testCDList10() { listTest(10); }
-  void testCDList15() { listTest(15); }
-  void testCDList20() { listTest(20); }
-  void testCDList35() { listTest(35); }
-  void testCDList50() { listTest(50); }
-  void testCDList99() { listTest(99); }
+  void testCDList_BE10() { listTest(10); }
+  void testCDList_BE15() { listTest(15); }
+  void testCDList_BE20() { listTest(20); }
+  void testCDList_BE35() { listTest(35); }
+  void testCDList_BE50() { listTest(50); }
+  void testCDList_BE99() { listTest(99); }
 
   void listTest(int N) {
     listTest(N, true);
@@ -71,7 +70,7 @@ public:
   }
 
   void listTest(int N, bool callDestructor) {
-    CDList<int> list(d_context, callDestructor);
+    CDList_BE<int> list(d_context, callDestructor);
 
     TS_ASSERT(list.empty());
     for(int i = 0; i < N; ++i) {
@@ -80,7 +79,7 @@ public:
       TS_ASSERT(!list.empty());
       TS_ASSERT_EQUALS(list.back(), i);
       int i2 = 0;
-      for(CDList<int>::const_iterator j = list.begin();
+      for(CDList_BE<int>::const_iterator j = list.begin();
           j != list.end();
           ++j) {
         TS_ASSERT_EQUALS(*j, i2++);
@@ -100,8 +99,8 @@ public:
     bool shouldAlsoRemainFalse = false;
     bool aThirdFalse = false;
 
-    CDList<DtorSensitiveObject> listT(d_context, true);
-    CDList<DtorSensitiveObject> listF(d_context, false);
+    CDList_BE<DtorSensitiveObject> listT(d_context, true);
+    CDList_BE<DtorSensitiveObject> listF(d_context, false);
 
     DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
     DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
@@ -136,15 +135,10 @@ public:
     TS_ASSERT_EQUALS(aThirdFalse, false);
   }
 
-  void testEmptyIterators() {
-    CDList<int>* list1 = new(true) CDList<int>(d_context);
-    CDList< int, ContextMemoryAllocator<int> >* list2 =
-      new(d_context->getCMM())
-        CDList< int, ContextMemoryAllocator<int> >(true, d_context, false,
-                                                   ContextMemoryAllocator<int>(d_context->getCMM()));
-    TS_ASSERT_EQUALS(list1->begin(), list1->end());
-    TS_ASSERT_EQUALS(list2->begin(), list2->end());
-    list1->deleteSelf();
+  void testEmptyIterator() {
+    CDList_BE<int>* list = new(true) CDList_BE<int>(d_context);
+    TS_ASSERT_EQUALS(list->begin(), list->end());
+    list->deleteSelf();
   }
 
   /* setrlimit() totally broken on Mac OS X */
@@ -155,7 +149,7 @@ public:
 
 #else /* __APPLE__ */
 
-    CDList<unsigned> list(d_context);
+    CDList_BE<unsigned> list(d_context);
     WithLimitedMemory wlm(1);
 
     TS_ASSERT_THROWS({
diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h
index a57fd131d..83fb20fd8 100644
--- a/test/unit/context/cdlist_context_memory_black.h
+++ b/test/unit/context/cdlist_context_memory_black.h
@@ -26,7 +26,7 @@
 #include "memory.h"
 
 #include "context/context.h"
-#include "context/cdlist_context_memory.h"
+#include "context/cdchunk_list.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -55,12 +55,12 @@ public:
 
   // test at different sizes.  this triggers grow() behavior differently.
   // grow() was completely broken in revision 256
-  void testCDList10() { listTest(10); }
-  void testCDList15() { listTest(15); }
-  void testCDList20() { listTest(20); }
-  void testCDList35() { listTest(35); }
-  void testCDList50() { listTest(50); }
-  void testCDList99() { listTest(99); }
+  void testCDChunkList10() { listTest(10); }
+  void testCDChunkList15() { listTest(15); }
+  void testCDChunkList20() { listTest(20); }
+  void testCDChunkList35() { listTest(35); }
+  void testCDChunkList50() { listTest(50); }
+  void testCDChunkList99() { listTest(99); }
 
   void listTest(int N) {
     listTest(N, true);
@@ -68,7 +68,7 @@ public:
   }
 
   void listTest(int N, bool callDestructor) {
-    CDList<int, ContextMemoryAllocator<int> >
+    CDChunkList<int>
       list(d_context, callDestructor, ContextMemoryAllocator<int>(d_context->getCMM()));
 
     TS_ASSERT(list.empty());
@@ -78,7 +78,7 @@ public:
       TS_ASSERT(!list.empty());
       TS_ASSERT_EQUALS(list.back(), i);
       int i2 = 0;
-      for(CDList<int, ContextMemoryAllocator<int> >::const_iterator j = list.begin();
+      for(CDChunkList<int>::const_iterator j = list.begin();
           j != list.end();
           ++j) {
         TS_ASSERT_EQUALS(*j, i2++);
@@ -91,6 +91,14 @@ public:
     }
   }
 
+  void testEmptyIterator() {
+    CDChunkList< int>* list =
+      new(d_context->getCMM())
+        CDChunkList< int >(true, d_context, false,
+                                                   ContextMemoryAllocator<int>(d_context->getCMM()));
+    TS_ASSERT_EQUALS(list->begin(), list->end());
+  }
+
   void testDtorCalled() {
     bool shouldRemainFalse = false;
     bool shouldFlipToTrue = false;
@@ -98,8 +106,8 @@ public:
     bool shouldAlsoRemainFalse = false;
     bool aThirdFalse = false;
 
-    CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listT(d_context, true, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
-    CDList<DtorSensitiveObject, ContextMemoryAllocator<DtorSensitiveObject> > listF(d_context, false, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+    CDChunkList<DtorSensitiveObject> listT(d_context, true, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
+    CDChunkList<DtorSensitiveObject> listF(d_context, false, ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
 
     DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
     DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
@@ -142,7 +150,7 @@ public:
 
 #else /* __APPLE__ */
 
-    CDList<unsigned, ContextMemoryAllocator<unsigned> > list(d_context);
+    CDChunkList<unsigned> list(d_context);
     WithLimitedMemory wlm(1);
 
     TS_ASSERT_THROWS({
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 0358d1edd..281d814aa 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -933,9 +933,9 @@ public:
     //Debug.on("gc");
     //Debug.on("context");
 
-    CDHashMap<int, CDList<myint>*, int_hasher> map(d_context);
+    CDHashMap<int, CDList_BE<myint>*, int_hasher> map(d_context);
 
-    CDList<myint> *list1, *list2, *list3, *list4;
+    CDList_BE<myint> *list1, *list2, *list3, *list4;
 
     TS_ASSERT(map.find(1) == map.end());
     TS_ASSERT(map.find(2) == map.end());
@@ -947,10 +947,10 @@ public:
 
       int* x = (int*) d_context->getCMM()->newData(sizeof(int));
 
-      list1 = new(d_context->getCMM()) CDList<myint>(true, d_context);
-      list2 = new(d_context->getCMM()) CDList<myint>(true, d_context);
-      list3 = new(d_context->getCMM()) CDList<myint>(true, d_context);
-      list4 = new(d_context->getCMM()) CDList<myint>(true, d_context);
+      list1 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+      list2 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+      list3 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
+      list4 = new(d_context->getCMM()) CDList_BE<myint>(true, d_context);
 
       list1->push_back(1);
       list2->push_back(2);
diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h
index b49186dd0..0f13d957e 100644
--- a/test/unit/context/cdvector_black.h
+++ b/test/unit/context/cdvector_black.h
@@ -68,8 +68,8 @@ public:
 
   void vectorTest(unsigned P, unsigned m){
     for(unsigned g=2; g< P; g++){
-      vectorTest(P, g, m, 1, false);
-      vectorTest(P, g, m, 3, false);
+      vectorTest(P, g, m, 1);
+      vectorTest(P, g, m, 3);
     }
   }
   vector<unsigned> copy(CDVector<unsigned>& v){
@@ -87,8 +87,8 @@ public:
     }
   }
 
-  void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r, bool callDestructor) {
-    CDVector<unsigned> vec(d_context, callDestructor);
+  void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r) {
+    CDVector<unsigned> vec(d_context);
     vector< vector<unsigned> > copies;
 
     copies.push_back( copy(vec) );