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, 22 insertions, 6 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index de260dd99..3e4aec641 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -444,16 +444,32 @@ public:
   virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
 
   /**
-   * A Theory is called with presolve exactly one time per user check-sat.
-   * presolve() is called after preregistration, rewriting, and Boolean propagation,
-   * (other theories' propagation?), but the notified Theory has not yet had its check()
-   * or propagate() method called yet.
-   * A Theory may empty its assertFact() queue using get().
-   * A Theory can raise conflicts, add lemmas, and propagate literals during presolve.
+   * The theory should only add (via .operator<< or .append()) to the
+   * "learned" builder.  It is a conjunction to add to the formula at
+   * the top-level and may contain other theories' contributions.
+   */
+  virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
+
+  /**
+   * A Theory is called with presolve exactly one time per user
+   * check-sat.  presolve() is called after preregistration,
+   * rewriting, and Boolean propagation, (other theories'
+   * propagation?), but the notified Theory has not yet had its
+   * check() or propagate() method called.  A Theory may empty its
+   * assertFact() queue using get().  A Theory can raise conflicts,
+   * add lemmas, and propagate literals during presolve().
    */
   virtual void presolve() = 0;
 
   /**
+   * Notification sent to the theory wheneven the search restarts.
+   * Serves as a good time to do some clean-up work, and you can
+   * assume you're at DL 0 for the purposes of Contexts.  This function
+   * should not use the output channel.
+   */
+  virtual void notifyRestart() { }
+
+  /**
    * Identify this theory (for debugging, dynamic configuration,
    * etc..)
    */