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, 45 insertions, 2 deletions

diff --git a/src/util/options.h b/src/util/options.h
index be432e5a7..d9d9c8567 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -34,7 +34,7 @@ namespace CVC4 {
 class ExprStream;
 
 /** Class representing an option-parsing exception. */
-class OptionException : public CVC4::Exception {
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
 public:
     OptionException(const std::string& s) throw() :
       CVC4::Exception("Error in option parsing: " + s) {
@@ -104,6 +104,25 @@ struct CVC4_PUBLIC Options {
   /** Should we expand function definitions lazily? */
   bool lazyDefinitionExpansion;
 
+  /** Enumeration of simplification modes (when to simplify). */
+  typedef enum {
+    BATCH_MODE,
+    INCREMENTAL_MODE,
+    INCREMENTAL_LAZY_SAT_MODE
+  } SimplificationMode;
+  /** When to perform nonclausal simplifications. */
+  SimplificationMode simplificationMode;
+
+  /** Enumeration of simplification styles (how much to simplify). */
+  typedef enum {
+    AGGRESSIVE_SIMPLIFICATION_STYLE,
+    TOPLEVEL_SIMPLIFICATION_STYLE,
+    NO_SIMPLIFICATION_STYLE
+  } SimplificationStyle;
+
+  /** Style of nonclausal simplifications to perform. */
+  SimplificationStyle simplificationStyle;
+
   /** Whether we're in interactive mode or not */
   bool interactive;
 
@@ -188,6 +207,9 @@ struct CVC4_PUBLIC Options {
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,
+                                Options::UfImplementation uf) CVC4_PUBLIC;
+
+inline std::ostream& operator<<(std::ostream& out,
                                 Options::UfImplementation uf) {
   switch(uf) {
   case Options::TIM:
@@ -203,7 +225,28 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule);
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::SimplificationMode mode) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::SimplificationMode mode) {
+  switch(mode) {
+  case Options::BATCH_MODE:
+    out << "BATCH_MODE";
+    break;
+  case Options::INCREMENTAL_MODE:
+    out << "INCREMENTAL_MODE";
+    break;
+  case Options::INCREMENTAL_LAZY_SAT_MODE:
+    out << "INCREMENTAL_LAZY_SAT_MODE";
+    break;
+  default:
+    out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
+  }
+
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC;
 
 }/* CVC4 namespace */