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

diff --git a/src/expr/command.h b/src/expr/command.h
index 17736ed77..d0b72c3dd 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -164,6 +164,19 @@ public:
   void toStream(std::ostream& out) const;
 };/* class QueryCommand */
 
+// this is TRANSFORM in the CVC presentation language
+class CVC4_PUBLIC SimplifyCommand : public Command {
+protected:
+  Expr d_term;
+  Expr d_result;
+public:
+  SimplifyCommand(Expr term);
+  void invoke(SmtEngine* smtEngine);
+  Expr getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
+};/* class SimplifyCommand */
+
 class CVC4_PUBLIC GetValueCommand : public Command {
 protected:
   Expr d_term;