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.

7 files changed, 85 insertions, 69 deletions

diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
index 27abd8873..98a202207 100644
--- a/src/theory/arith/arith_constants.h
+++ b/src/theory/arith/arith_constants.h
@@ -31,7 +31,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class ArithConstants{
+class ArithConstants {
 public:
   Rational d_ZERO;
   Rational d_ONE;
@@ -52,10 +52,16 @@ public:
     d_ONE_NODE(nm->mkConst(d_ONE)),
     d_NEGATIVE_ONE_NODE(nm->mkConst(d_NEGATIVE_ONE))
   {}
-};
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+  ~ArithConstants() {
+    d_ZERO_NODE = Node::null();
+    d_ONE_NODE = Node::null();
+    d_NEGATIVE_ONE_NODE = Node::null();
+  }
+};/* class ArithConstants */
+
+}/* namespace CVC4::theory::arith */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
 
 #endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index 4b7dfcef5..415668b49 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -33,7 +33,7 @@ EOF
 
 template=$1; shift
 
-theoryof_table_includes=
+theoryof_table_forwards=
 theoryof_table_registers=
 
 seen_theory=false
@@ -61,7 +61,23 @@ function theory {
     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
   fi
 
-  theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\"
+  decl=
+  last=
+  num=0
+  for ns in `echo "$1" | sed 's,::, ,g'`; do
+    if [ -n "$last" ]; then
+      decl="${decl}namespace $last { "
+      let ++num
+    fi
+    last="$ns"
+  done
+  decl="${decl}class $last;"
+  while [ $num -gt 0 ]; do
+    decl="${decl} }"
+    let --num
+  done
+
+  theoryof_table_forwards="${theoryof_table_forwards}$decl // #include \"theory/$b/$2\"
 "
   theoryof_table_registers="${theoryof_table_registers}
   /* from $b */
@@ -103,7 +119,7 @@ function constant {
 
 function do_theoryof {
   check_theory_seen
-  theoryof_table_registers="${theoryof_table_registers}    d_table[::CVC4::kind::$1] = th;
+  theoryof_table_registers="${theoryof_table_registers}    d_table[::CVC4::kind::$1] = (Theory*)th;
 "
 }
 
@@ -135,7 +151,7 @@ check_builtin_theory_seen
 ## output
 
 text=$(cat "$template")
-for var in theoryof_table_includes theoryof_table_registers; do
+for var in theoryof_table_forwards theoryof_table_registers; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
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() {
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
diff --git a/src/theory/theoryof_table_template.h b/src/theory/theoryof_table_template.h
index e0d6fc8c8..5da28f2d4 100644
--- a/src/theory/theoryof_table_template.h
+++ b/src/theory/theoryof_table_template.h
@@ -25,7 +25,7 @@
 #include "expr/kind.h"
 #include "util/Assert.h"
 
-${theoryof_table_includes}
+${theoryof_table_forwards}
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index fe1f3106e..4ee698721 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -34,12 +34,10 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
   d_cc(ctxt, &d_ccChannel),
   d_unionFind(ctxt),
   d_disequalities(ctxt),
-  d_disequality(ctxt),
   d_conflict(),
   d_trueNode(),
   d_falseNode(),
-  d_trueEqFalseNode(),
-  d_activeAssertions(ctxt) {
+  d_trueEqFalseNode() {
   NodeManager* nm = NodeManager::currentNM();
   TypeNode boolType = nm->booleanType();
   d_trueNode = nm->mkVar("TRUE_UF", boolType);
@@ -51,6 +49,9 @@ TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
 }
 
 TheoryUFMorgan::~TheoryUFMorgan() {
+  d_trueNode = Node::null();
+  d_falseNode = Node::null();
+  d_trueEqFalseNode = Node::null();
 }
 
 RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
@@ -189,11 +190,6 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
 
   d_unionFind[a] = b;
 
-  if(Debug.isOn("uf") && find(d_trueNode) == find(d_falseNode)) {
-    Debug("uf") << "ok, pay attention now.." << std::endl;
-    dump();
-  }
-
   DiseqLists::iterator deq_i = d_disequalities.find(a);
   if(deq_i != d_disequalities.end()) {
     // a set of other trees we are already disequal to
@@ -268,7 +264,8 @@ void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
   DiseqLists::iterator deq_i = d_disequalities.find(of);
   DiseqList* deq;
   if(deq_i == d_disequalities.end()) {
-    deq = new(getContext()->getCMM()) DiseqList(true, getContext());
+    deq = new(getContext()->getCMM()) DiseqList(true, getContext(), false,
+                                                ContextMemoryAllocator<TNode>(getContext()->getCMM()));
     d_disequalities.insertDataFromContextMemory(of, deq);
   } else {
     deq = (*deq_i).second;
@@ -298,7 +295,7 @@ void TheoryUFMorgan::check(Effort level) {
 
     Node assertion = get();
 
-    d_activeAssertions.push_back(assertion);
+    //d_activeAssertions.push_back(assertion);
 
     Debug("uf") << "uf check(): " << assertion << std::endl;
 
@@ -349,7 +346,6 @@ void TheoryUFMorgan::check(Effort level) {
         Node b = assertion[0][1];
 
         addDisequality(assertion[0]);
-        d_disequality.push_back(assertion[0]);
 
         d_cc.addTerm(a);
         d_cc.addTerm(b);
@@ -418,14 +414,17 @@ void TheoryUFMorgan::check(Effort level) {
       Unhandled(assertion.getKind());
     }
 
+    /*
     if(Debug.isOn("uf")) {
       dump();
     }
+    */
   }
   Assert(d_conflict.isNull());
   Debug("uf") << "uf check() done = " << (done() ? "true" : "false")
               << std::endl;
 
+  /*
   for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
       diseqIter != d_disequality.end();
       ++diseqIter) {
@@ -443,6 +442,7 @@ void TheoryUFMorgan::check(Effort level) {
     Assert((debugFind(left) == debugFind(right)) ==
            d_cc.areCongruent(left, right));
   }
+  */
 
   Debug("uf") << "uf: end check(" << level << ")" << std::endl;
 }
@@ -477,6 +477,7 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
   }
 }
 
+/*
 void TheoryUFMorgan::dump() {
   if(!Debug.isOn("uf")) {
     return;
@@ -509,3 +510,4 @@ void TheoryUFMorgan::dump() {
   }
   Debug("uf") << "=======================================" << std::endl;
 }
+*/
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 7a12f216b..023e100a9 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -11,16 +11,13 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.
- **
- ** This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.  It is based on the Nelson-Oppen algorithm given in
- ** "Fast Decision Procedures Based on Congruence Closure"
- **  (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
- ** This has been extended to work in a context-dependent way.
- ** This interacts heavily with the data-structures given in ecdata.h .
+ ** \brief Implementation of the theory of uninterpreted functions with
+ ** equality
  **
+ ** Implementation of the theory of uninterpreted functions with equality,
+ ** based on CVC4's congruence closure module (which is in turn based on
+ ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and
+ ** Extensions.
  **/
 
 #include "cvc4_private.h"
@@ -35,7 +32,7 @@
 #include "theory/uf/theory_uf.h"
 
 #include "context/context.h"
-#include "context/cdo.h"
+#include "context/context_mm.h"
 #include "context/cdlist.h"
 #include "util/congruence_closure.h"
 
@@ -81,19 +78,17 @@ private:
   typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind;
   UnionFind d_unionFind;
 
-  typedef context::CDList<Node> DiseqList;
+  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList;
   typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
 
   /** List of all disequalities this theory has seen. */
   DiseqLists d_disequalities;
 
-  context::CDList<Node> d_disequality;
-
   Node d_conflict;
 
   Node d_trueNode, d_falseNode, d_trueEqFalseNode;
 
-  context::CDList<Node> d_activeAssertions;
+  //context::CDList<Node> d_activeAssertions;
 
 public: