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

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b8a72dc38..c884b2c5f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -289,6 +289,9 @@ public:
   /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
+   *
+   * @todo (design) is this meant to give an equivalent or an
+   * equisatisfiable formula?
    */
   Expr simplify(const Expr& e);