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

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 0c60ec5ea..d46b9aab1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,6 +24,7 @@
 #define __CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 
@@ -50,6 +51,20 @@ public:
    */
   Node getSatValue(TNode n) const;
 
+  /**
+   * Simplify a node.  Intended to be used by a theory's simplify()
+   * function to simplify subterms (TheoryEngine will cache the
+   * results and make sure that the request is directed to the correct
+   * theory).
+   */
+  Node simplify(TNode in, Substitutions& outSubstitutions);
+
+  /**
+   * Rewrite a node.  Intended to be used by a theory to have the
+   * TheoryEngine fully rewrite a node.
+   */
+  Node rewrite(TNode in);
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */