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

diff --git a/src/util/stats.h b/src/util/stats.h
index c0660bf88..d68836812 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -475,6 +475,33 @@ public:
   }
 };/* class TimerStat */
 
+/**
+ * To use a statistic, you need to declare it, initialize it in your
+ * constructor, register it in your constructor, and deregister it in
+ * your destructor.  Instead, this macro does it all for you (and
+ * therefore also keeps the statistic type, field name, and output
+ * string all in the same place in your class's header.  Its use is
+ * like in this example, which takes the place of the declaration of a
+ * statistics field "d_checkTimer":
+ *
+ *   KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::morgan::checkTime");
+ *
+ * If any args need to be passed to the constructor, you can specify
+ * them after the string.
+ *
+ * The macro works by creating a nested class type, derived from the
+ * statistic type you give it, which declares a registry-aware
+ * constructor/destructor pair.
+ */
+#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...)  \
+  struct Statistic_##_StatField : public _StatType {                    \
+    Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) {     \
+      StatisticsRegistry::registerStat(this);                           \
+    }                                                                   \
+    ~Statistic_##_StatField() {                                         \
+      StatisticsRegistry::unregisterStat(this);                         \
+    }                                                                   \
+  } _StatField
 
 #undef __CVC4_USE_STATISTICS