Merge from ufprop branch, including:

* Theory::staticLearning() for statically adding new T-stuff before
  normal preprocessing.  UF's staticLearning() does transitivity of
  equality/iff, solving the diamonds.

* more aggressive T-propagation for UF

* new KEEP_STATISTIC macro to hide Theories from having to
  register/deregister statistics (and also has the advantage of
  keeping the statistic type, field name, and the 'tag' used to output
  the statistic in the same place---instead of scattered in the theory
  definition and constructor initializer list.  See documentation for
  KEEP_STATISTIC in src/util/stats.h for more of an explanation).

* more statistics for UF

* restart notifications from SAT (through TheoryEngine) via
  Theory::notifyRestart()

* StackingMap and UnionFind unit tests

* build fixes/adjustments

* code cleanup; minor other improvements

1 files changed, 51 insertions, 5 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 48f983b3f..e2c42bccd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -622,15 +622,61 @@ bool TheoryEngine::presolve() {
   d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
   try {
+    /*
+    d_builtin->presolve();
+    if(!d_theoryOut.d_conflictNode.get().isNull()) {
+      return true;
+    }
+    d_bool->presolve();
+    if(!d_theoryOut.d_conflictNode.get().isNull()) {
+      return true;
+    }
+    */
     d_uf->presolve();
+    if(!d_theoryOut.d_conflictNode.get().isNull()) {
+      return true;
+    }
     d_arith->presolve();
-    //d_arrays->presolve();
-    //d_bv->presolve();
+    /*
+    if(!d_theoryOut.d_conflictNode.get().isNull()) {
+      return true;
+    }
+    d_arrays->presolve();
+    if(!d_theoryOut.d_conflictNode.get().isNull()) {
+      return true;
+    }
+    d_bv->presolve();
+    */
   } catch(const theory::Interrupted&) {
-    Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl;
+    Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
-  // Return whether we have a conflict
-  return d_theoryOut.d_conflictNode.get().isNull();
+  // return whether we have a conflict
+  return !d_theoryOut.d_conflictNode.get().isNull();
+}
+
+
+void TheoryEngine::notifyRestart() {
+  /*
+  d_builtin->notifyRestart();
+  d_bool->notifyRestart();
+  */
+  d_uf->notifyRestart();
+  /*
+  d_arith->notifyRestart();
+  d_arrays->notifyRestart();
+  d_bv->notifyRestart();
+  */
+}
+
+
+void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
+  d_builtin->staticLearning(in, learned);
+  d_bool->staticLearning(in, learned);
+  d_uf->staticLearning(in, learned);
+  d_arith->staticLearning(in, learned);
+  d_arrays->staticLearning(in, learned);
+  d_bv->staticLearning(in, learned);
 }
 
+
 }/* CVC4 namespace */