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, 4 insertions, 0 deletions

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 */