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, 9 insertions, 5 deletions

diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index cc18a3305..db9d5bc65 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -28,9 +28,11 @@
 
 #include "expr/node_manager.h"
 #include "expr/node.h"
+#include "context/context_mm.h"
+#include "context/cdo.h"
 #include "context/cdmap.h"
 #include "context/cdset.h"
-#include "context/cdlist.h"
+#include "context/cdlist_context_memory.h"
 #include "util/exception.h"
 
 namespace CVC4 {
@@ -102,9 +104,9 @@ class CongruenceClosure {
 
   // typedef all of these so that iterators are easy to define
   typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap;
-  typedef context::CDList<Node> ClassList;
+  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
   typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
-  typedef context::CDList<Node> UseList;
+  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
   typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists;
   typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap;
 
@@ -348,7 +350,8 @@ private:
     UseLists::iterator usei = d_useList.find(of);
     UseList* ul;
     if(usei == d_useList.end()) {
-      ul = new(d_context->getCMM()) UseList(true, d_context);
+      ul = new(d_context->getCMM()) UseList(true, d_context, false,
+                                            context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
       d_useList.insertDataFromContextMemory(of, ul);
     } else {
       ul = (*usei).second;
@@ -549,7 +552,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
         ClassLists::iterator cl_bpi = d_classList.find(bp);
         ClassList* cl_bp;
         if(cl_bpi == d_classList.end()) {
-          cl_bp = new(d_context->getCMM()) ClassList(true, d_context);
+          cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false,
+                                                     context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
           d_classList.insertDataFromContextMemory(bp, cl_bp);
           Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
         } else {