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, 7 insertions, 19 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2d056af28..85e6d2cfc 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -24,18 +24,8 @@
 #include "expr/node.h"
 #include "theory/theory.h"
 #include "theory/theoryof_table.h"
-
 #include "prop/prop_engine.h"
 #include "theory/shared_term_manager.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/tim/theory_uf_tim.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
-
 #include "util/stats.h"
 
 namespace CVC4 {
@@ -119,21 +109,19 @@ class TheoryEngine {
       d_explanationNode = explanationNode;
       ++(d_engine->d_statistics.d_statExplanation);
     }
-  };
-
-
+  };/* class EngineOutputChannel */
 
   EngineOutputChannel d_theoryOut;
 
   /** Pointer to Shared Term Manager */
   SharedTermManager* d_sharedTermManager;
 
-  theory::builtin::TheoryBuiltin* d_builtin;
-  theory::booleans::TheoryBool* d_bool;
-  theory::uf::TheoryUF* d_uf;
-  theory::arith::TheoryArith* d_arith;
-  theory::arrays::TheoryArrays* d_arrays;
-  theory::bv::TheoryBV* d_bv;
+  theory::Theory* d_builtin;
+  theory::Theory* d_bool;
+  theory::Theory* d_uf;
+  theory::Theory* d_arith;
+  theory::Theory* d_arrays;
+  theory::Theory* d_bv;
 
   /**
    * Debugging flag to ensure that shutdown() is called before the