Merge from cc-memout branch. Here are the main points

* Add ContextMemoryAllocator<T> allocator type, conforming to
  STL allocator requirements.

* Extend the CDList<> template to take an allocator (defaults
  to std::allocator<T>).

* Add a specialized version of the CDList<> template (in
  src/context/cdlist_context_memory.h) that allocates a list
  in segments, in context memory.

* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
  and cdset_forward.h.  Use these in public headers, and other
  places where you don't need the full header (just the
  forward-declaration).  These types justify their own header
  (instead of just forward-declaring yourself), because they
  are complex templated types, with default template parameters,
  specializations, etc.

* theory_engine.h no longer depends on individual theory headers.
  (Instead it forward-declares Theory implementations.)  This is
  especially important now that theory .cpp files depend on
  TheoryEngine (to implement Theory::getValue()).  Previously,
  any modification to any theory header file required *all*
  theories, and the engine, to be completely rebuilt.

* Support memory cleanup for nontrivial CONSTANT kinds.  This
  resolves an issue with arithmetic where memory leaked for
  each distinct Rational or Integer that was wrapped in a Node.

6 files changed, 780 insertions, 72 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 398de65a3..9e349a06b 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -12,6 +12,10 @@ libcontext_la_SOURCES = \
 	context_mm.h \
 	cdo.h \
 	cdlist.h \
+	cdlist_context_memory.h \
+	cdlist_forward.h \
 	cdmap.h \
+	cdmap_forward.h \
 	cdset.h \
+	cdset_forward.h \
 	cdvector.h
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 02418d3df..7edef4121 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -22,23 +22,42 @@
 #define __CVC4__CONTEXT__CDLIST_H
 
 #include <iterator>
+#include <memory>
+#include <string>
+#include <sstream>
 
 #include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdlist_forward.h"
 #include "util/Assert.h"
 
 namespace CVC4 {
 namespace context {
 
 /**
- * Generic context-dependent dynamic array.  Note that for efficiency, this
- * implementation makes the following assumptions:
+ * Generic context-dependent dynamic array.  Note that for efficiency,
+ * this implementation makes the following assumptions:
+ *
  * 1. Over time, objects are only added to the list.  Objects are only
  *    removed when a pop restores the list to a previous state.
+ *
  * 2. T objects can safely be copied using their copy constructor,
  *    operator=, and memcpy.
  */
-template <class T>
+template <class T, class AllocatorT>
 class CDList : 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 AllocatorT Allocator;
+
+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.
    */
@@ -54,55 +73,33 @@ class CDList : public ContextObj {
   /**
    * Number of objects in d_list
    */
-  unsigned d_size;
+  size_t d_size;
 
   /**
    * Allocated size of d_list.
    */
-  unsigned d_sizeAlloc;
-
-protected:
+  size_t d_sizeAlloc;
 
   /**
-   * 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.
+   * Our allocator.
    */
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDList<T>(*this);
-  }
-
-  /**
-   * 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) {
-    if(d_callDestructor) {
-      unsigned size = ((CDList<T>*)data)->d_size;
-      while(d_size != size) {
-        --d_size;
-        d_list[d_size].~T();
-      }
-    } else {
-      d_size = ((CDList<T>*)data)->d_size;
-    }
-  }
-
-private:
+  Allocator d_allocator;
 
   /**
-   * Private copy constructor used only by save above.  d_list and d_sizeAlloc
-   * are not copied: only the base class information and d_size are needed in
-   * restore.
+   * Private copy constructor used only by save().  d_list and
+   * d_sizeAlloc are not copied: only the base class information and
+   * d_size are needed in restore.
    */
-  CDList(const CDList<T>& l) :
+  CDList(const CDList<T, Allocator>& l) :
     ContextObj(l),
     d_list(NULL),
-    d_callDestructor(l.d_callDestructor),
+    d_callDestructor(false),
     d_size(l.d_size),
-    d_sizeAlloc(0) {
+    d_sizeAlloc(0),
+    d_allocator(l.d_allocator) {
+    Debug("cdlist") << "copy ctor: " << this
+                    << " from " << &l
+                    << " size " << d_size << std::endl;
   }
 
   /**
@@ -112,64 +109,133 @@ private:
   void grow() {
     if(d_list == NULL) {
       // Allocate an initial list if one does not yet exist
-      d_sizeAlloc = 10;
-      d_list = (T*) malloc(sizeof(T) * d_sizeAlloc);
+      d_sizeAlloc = INITIAL_SIZE;
+      Debug("cdlist") << "initial grow of cdlist " << this
+                      << " level " << getContext()->getLevel()
+                      << " to " << d_sizeAlloc << std::endl;
+      if(d_sizeAlloc > d_allocator.max_size()) {
+        d_sizeAlloc = d_allocator.max_size();
+      }
+      d_list = d_allocator.allocate(d_sizeAlloc);
       if(d_list == NULL) {
         throw std::bad_alloc();
       }
     } else {
       // Allocate a new array with double the size
-      d_sizeAlloc *= 2;
-      T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc);
-      if(tmpList == NULL) {
+      size_t newSize = GROWTH_FACTOR * d_sizeAlloc;
+      if(newSize > d_allocator.max_size()) {
+        newSize = d_allocator.max_size();
+        Assert(newSize > d_sizeAlloc,
+               "cannot request larger list due to allocator limits");
+      }
+      T* newList = d_allocator.allocate(newSize);
+      Debug("cdlist") << "2x grow of cdlist " << this
+                      << " level " << getContext()->getLevel()
+                      << " to " << newSize
+                      << " (from " << d_list
+                      << " to " << newList << ")" << std::endl;
+      if(newList == NULL) {
         throw std::bad_alloc();
       }
-      d_list = tmpList;
+      std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc);
+      d_allocator.deallocate(d_list, d_sizeAlloc);
+      d_list = newList;
+      d_sizeAlloc = 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) CDList<T, Allocator>(*this);
+    Debug("cdlist") << "save " << this
+                    << " at level " << this->getContext()->getLevel()
+                    << " size at " << this->d_size
+                    << " 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.  Note that the list pointer and the
+   * allocated size are not changed.
+   */
+  void restore(ContextObj* data) {
+    Debug("cdlist") << "restore " << this
+                    << " level " << this->getContext()->getLevel()
+                    << " data == " << data
+                    << " call dtor == " << this->d_callDestructor
+                    << " d_list == " << this->d_list << std::endl;
+    if(this->d_callDestructor) {
+      const size_t size = ((CDList<T, Allocator>*)data)->d_size;
+      while(this->d_size != size) {
+        --this->d_size;
+        this->d_allocator.destroy(&this->d_list[this->d_size]);
+      }
+    } else {
+      this->d_size = ((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;
   }
 
 public:
+
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
-  CDList(Context* context, bool callDestructor = true) :
+  CDList(Context* context, bool callDestructor = true,
+         const Allocator& alloc = Allocator()) :
     ContextObj(context),
     d_list(NULL),
     d_callDestructor(callDestructor),
     d_size(0),
-    d_sizeAlloc(0) {
+    d_sizeAlloc(0),
+    d_allocator(alloc) {
   }
 
   /**
    * Main constructor: d_list starts as NULL, size is 0
    */
-  CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
+  CDList(bool allocatedInCMM, Context* context, bool callDestructor = true,
+         const Allocator& alloc = Allocator()) :
     ContextObj(allocatedInCMM, context),
     d_list(NULL),
     d_callDestructor(callDestructor),
     d_size(0),
-    d_sizeAlloc(0) {
+    d_sizeAlloc(0),
+    d_allocator(alloc) {
   }
 
   /**
    * Destructor: delete the list
    */
   ~CDList() throw(AssertionException) {
-    destroy();
+    this->destroy();
 
-    if(d_callDestructor) {
-      for(unsigned i = 0; i < d_size; ++i) {
-        d_list[i].~T();
+    if(this->d_callDestructor) {
+      for(size_t i = 0; i < this->d_size; ++i) {
+        this->d_allocator.destroy(&this->d_list[i]);
       }
     }
 
-    free(d_list);
+    this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
   }
 
   /**
-   * Return the current size of (i.e. valid number of objects in) the list
+   * Return the current size of (i.e. valid number of objects in) the
+   * list.
    */
-  unsigned size() const {
+  size_t size() const {
     return d_size;
   }
 
@@ -184,20 +250,43 @@ public:
    * Add an item to the end of the list.
    */
   void push_back(const T& data) {
+    Debug("cdlist") << "push_back " << this
+                    << " " << getContext()->getLevel()
+                    << ": make-current, "
+                    << "d_list == " << d_list << std::endl;
     makeCurrent();
 
+    Debug("cdlist") << "push_back " << this
+                    << " " << getContext()->getLevel()
+                    << ": grow? " << d_size
+                    << " " << d_sizeAlloc << std::endl;
     if(d_size == d_sizeAlloc) {
+      Debug("cdlist") << "push_back " << this
+                      << " " << getContext()->getLevel()
+                      << ": grow!" << std::endl;
       grow();
     }
-
-    ::new((void*)(d_list + d_size)) T(data);
+    Assert(d_size < d_sizeAlloc);
+
+    Debug("cdlist") << "push_back " << this
+                    << " " << getContext()->getLevel()
+                    << ": construct! at " << d_list
+                    << "[" << d_size << "] == " << &d_list[d_size]
+                    << std::endl;
+    d_allocator.construct(&d_list[d_size], data);
+    Debug("cdlist") << "push_back " << this
+                    << " " << getContext()->getLevel()
+                    << ": done..." << std::endl;
     ++d_size;
+    Debug("cdlist") << "push_back " << this
+                    << " " << getContext()->getLevel()
+                    << ": size now " << d_size << std::endl;
   }
 
   /**
    * Access to the ith item in the list.
    */
-  const T& operator[](unsigned i) const {
+  const T& operator[](size_t i) const {
     Assert(i < d_size, "index out of bounds in CDList::operator[]");
     return d_list[i];
   }
@@ -211,21 +300,24 @@ public:
   }
 
   /**
-   * 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).
+   * 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 {
-    T* d_it;
+    T const* d_it;
 
-    const_iterator(T* it) : d_it(it) {}
+    const_iterator(T const* it) : d_it(it) {}
 
-    friend class CDList<T>;
+    friend class CDList<T, Allocator>;
 
   public:
 
+    // FIXME we support operator--, but do we satisfy all the
+    // requirements of a bidirectional iterator ?
     typedef std::input_iterator_tag iterator_category;
     typedef T value_type;
     typedef ptrdiff_t difference_type;
@@ -289,17 +381,16 @@ public:
    * Returns an iterator pointing to the first item in the list.
    */
   const_iterator begin() const {
-    return const_iterator(d_list);
+    return const_iterator(static_cast<T const*>(d_list));
   }
 
   /**
    * Returns an iterator pointing one past the last item in the list.
    */
   const_iterator end() const {
-    return const_iterator(d_list + d_size);
+    return const_iterator(static_cast<T const*>(d_list) + d_size);
   }
-
-};/* class CDList */
+};/* class CDList<> */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h
new file mode 100644
index 000000000..f85d3b79e
--- /dev/null
+++ b/src/context/cdlist_context_memory.h
@@ -0,0 +1,493 @@
+/*********************                                                        */
+/*! \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  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);
+
+  /**
+   * 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 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 {
+    return const_iterator(&d_headSegment, 0);
+  }
+
+  /**
+   * 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
new file mode 100644
index 000000000..82bc9cc15
--- /dev/null
+++ b/src/context/cdlist_forward.h
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file cdlist_forward.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  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 This is a forward declaration header to declare the
+ ** CDList<> template
+ **
+ ** This is a forward declaration header to declare the CDList<>
+ ** template.  It's useful if you want to forward-declare CDList<>
+ ** without including the full cdlist.h or cdlist_context_memory.h
+ ** header, for example, in a public header context, or to keep
+ ** compile times low when only a forward declaration is needed.
+ **
+ ** Note that all specializations of the template should be listed
+ ** here as well, since different specializations are defined in
+ ** different headers (cdlist.h and cdlist_context_memory.h).
+ ** Explicitly declaring both specializations here ensure that if you
+ ** define one, you'll get an error if you didn't include the correct
+ ** header (avoiding different, incompatible instantiations in
+ ** different compilation units).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_FORWARD_H
+#define __CVC4__CONTEXT__CDLIST_FORWARD_H
+
+#include <memory>
+
+namespace __gnu_cxx {
+  template <class Key> class hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+  namespace context {
+    template <class T>
+    class ContextMemoryAllocator;
+
+    template <class T, class Allocator = std::allocator<T> >
+    class CDList;
+
+    template <class T>
+    class CDList<T, ContextMemoryAllocator<T> >;
+  }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 5a1e52d66..fde69a149 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -23,6 +23,7 @@
 #include <new>
 #include "context/context_mm.h"
 #include "util/Assert.h"
+#include "util/output.h"
 
 namespace CVC4 {
 namespace context {
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 1eb452113..71f7041c7 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -103,7 +103,14 @@ class ContextMemoryManager {
    */
   void newChunk();
 
- public:
+public:
+
+  /**
+   * Get the maximum allocation size for this memory manager.
+   */
+  static unsigned getMaxAllocationSize() {
+    return chunkSizeBytes;
+  }
 
   /**
    * Constructor - creates an initial region and an empty stack
@@ -133,6 +140,62 @@ class ContextMemoryManager {
 
 };/* class ContextMemoryManager */
 
+/**
+ * An STL-like allocator class for allocating from context memory.
+ */
+template <class T>
+class ContextMemoryAllocator {
+  ContextMemoryManager* d_mm;
+
+public:
+
+  typedef size_t size_type;
+  typedef ptrdiff_t difference_type;
+  typedef T* pointer;
+  typedef T const* const_pointer;
+  typedef T& reference;
+  typedef T const& const_reference;
+  typedef T value_type;
+  template <class U> struct rebind {
+    typedef ContextMemoryAllocator<U> other;
+  };
+
+  ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {}
+  ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {}
+  ~ContextMemoryAllocator() throw() {}
+
+  ContextMemoryManager* getCMM() { return d_mm; }
+  T* address(T& v) const { return &v; }
+  T const* address(T const& v) const { return &v; }
+  size_t max_size() const throw() {
+    return ContextMemoryManager::getMaxAllocationSize() / sizeof(T);
+  }
+  T* allocate(size_t n, const void* = 0) const {
+    return static_cast<T*>(d_mm->newData(n * sizeof(T)));
+  }
+  void deallocate(T* p, size_t n) const {
+    /* no explicit delete */
+  }
+  void construct(T* p, T const& v) const {
+    ::new(reinterpret_cast<void*>(p)) T(v);
+  }
+  void destroy(T* p) const {
+    p->~T();
+  }
+};/* class ContextMemoryAllocator<T> */
+
+template <class T>
+inline bool operator==(const ContextMemoryAllocator<T>& a1,
+                       const ContextMemoryAllocator<T>& a2) {
+  return a1.d_mm == a2.d_mm;
+}
+
+template <class T>
+inline bool operator!=(const ContextMemoryAllocator<T>& a1,
+                       const ContextMemoryAllocator<T>& a2) {
+  return a1.d_mm != a2.d_mm;
+}
+
 }/* CVC4::context namespace */
 }/* CVC4 namespace */