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

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