Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

1 files changed, 30 insertions, 3 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 19374d6db..e571c2bbd 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -22,15 +22,20 @@
 #define __CVC4__THEORY_ENGINE_H
 
 #include <deque>
+#include <vector>
+#include <utility>
 
 #include "expr/node.h"
 #include "prop/prop_engine.h"
 #include "theory/shared_term_manager.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
+#include "theory/substitutions.h"
 #include "theory/valuation.h"
 #include "util/options.h"
 #include "util/stats.h"
+#include "util/hash.h"
+#include "util/cache.h"
 
 namespace CVC4 {
 
@@ -69,6 +74,16 @@ class TheoryEngine {
   size_t d_activeTheories;
 
   /**
+   * The type of the simplification cache.
+   */
+  typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
+
+  /**
+   * A cache for simplification.
+   */
+  SimplifyCache d_simplifyCache;
+
+  /**
    * An output channel for Theory that passes messages
    * back to a TheoryEngine.
    */
@@ -273,11 +288,17 @@ public:
   }
 
   /**
-   * Preprocess a node.  This involves theory-specific rewriting, then
-   * calling preRegister() on what's left over.
+   * Preprocess a node.  This involves ITE removal and theory-specific
+   * rewriting.
+   *
    * @param n the node to preprocess
    */
   Node preprocess(TNode n);
+
+  /**
+   * Preregister a Theory atom with the responsible theory (or
+   * theories).
+   */
   void preRegister(TNode preprocessed);
 
   /**
@@ -325,12 +346,18 @@ public:
   bool check(theory::Theory::Effort effort);
 
   /**
-   * Calls staticLearning() on all active theories, accumulating their
+   * Calls staticLearning() on all theories, accumulating their
    * combined contributions in the "learned" builder.
    */
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   /**
+   * Calls simplify() on all theories, accumulating their combined
+   * contributions in the "outSubstitutions" vector.
+   */
+  Node simplify(TNode in, theory::Substitutions& outSubstitutions);
+
+  /**
    * Calls presolve() on all active theories and returns true
    * if one of the theories discovers a conflict.
    */