diff options
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 47 |
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 */ |