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

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 269f28732..7d7da35c5 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -82,8 +82,7 @@ public:
   /**
    * Propagate a theory literal.
    *
-   * @param n - a theory consequence at the current decision level.
-   *
+   * @param n - a theory consequence at the current decision level
    * @param safe - whether it is safe to be interrupted
    */
   virtual void propagate(TNode n, bool safe = false)
@@ -91,7 +90,7 @@ public:
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
-   * been detected.  (This request a split.)
+   * been detected.  (This requests a split.)
    *
    * @param n - a theory lemma valid at decision level 0
    * @param safe - whether it is safe to be interrupted