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

3 files changed, 9 insertions, 0 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 4817ec1f5..18ed9b5da 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -986,6 +986,9 @@ lbool Solver::search(int nof_conflicts)
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
+                // [mdeters] notify theory engine of restarts for deferred
+                // theory processing
+                proxy->notifyRestart();
                 return l_Undef; }
 
             // Simplify the set of problem clauses:
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 97c5d1419..b78f20ee8 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -102,5 +102,9 @@ TNode SatSolver::getNode(SatLiteral lit) {
   return d_cnfStream->getNode(lit);
 }
 
+void SatSolver::notifyRestart() {
+  d_theoryEngine->notifyRestart();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 6e244d9d7..cc81ea5c6 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -247,6 +247,8 @@ public:
 
   TNode getNode(SatLiteral lit);
 
+  void notifyRestart();
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */