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, 24 insertions, 15 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 384e2fdd6..29aed8426 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -16,6 +16,9 @@
  ** The theory engine.
  **/
 
+#include <vector>
+#include <list>
+
 #include "theory/theory_engine.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
@@ -23,8 +26,14 @@
 #include "expr/node_builder.h"
 #include "smt/options.h"
 
-#include <vector>
-#include <list>
+#include "theory/builtin/theory_builtin.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/morgan/theory_uf_morgan.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arrays/theory_arrays.h"
+#include "theory/bv/theory_bv.h"
 
 using namespace std;
 
@@ -141,19 +150,19 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) :
   d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
   d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
 
-  d_sharedTermManager->registerTheory(d_builtin);
-  d_sharedTermManager->registerTheory(d_bool);
-  d_sharedTermManager->registerTheory(d_uf);
-  d_sharedTermManager->registerTheory(d_arith);
-  d_sharedTermManager->registerTheory(d_arrays);
-  d_sharedTermManager->registerTheory(d_bv);
-
-  d_theoryOfTable.registerTheory(d_builtin);
-  d_theoryOfTable.registerTheory(d_bool);
-  d_theoryOfTable.registerTheory(d_uf);
-  d_theoryOfTable.registerTheory(d_arith);
-  d_theoryOfTable.registerTheory(d_arrays);
-  d_theoryOfTable.registerTheory(d_bv);
+  d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+  d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
+  d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
+  d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
+  d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
+  d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
+
+  d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
+  d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
+  d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
+  d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
+  d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
+  d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
 }
 
 TheoryEngine::~TheoryEngine() {