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.

1 files changed, 162 insertions, 71 deletions

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 */