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, 64 insertions, 1 deletions

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