diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/options | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/boolean_term_conversion_mode.cpp | 17 | ||||
-rw-r--r-- | src/options/boolean_term_conversion_mode.h | 19 | ||||
-rw-r--r-- | src/options/booleans_options | 2 | ||||
-rw-r--r-- | src/options/expr_options | 3 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 35 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 |
6 files changed, 0 insertions, 80 deletions
diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp index 0673718bb..4fc9b1f8d 100644 --- a/src/options/boolean_term_conversion_mode.cpp +++ b/src/options/boolean_term_conversion_mode.cpp @@ -20,22 +20,5 @@ namespace CVC4 { -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { - switch(mode) { - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: - out << "BOOLEAN_TERM_CONVERT_NATIVE"; - break; - default: - out << "BooleanTermConversionMode!UNKNOWN"; - } - - return out; -} }/* CVC4 namespace */ diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index f2f4a51af..57e2ccaf4 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -26,28 +26,9 @@ namespace CVC4 { namespace theory { namespace booleans { -enum BooleanTermConversionMode { - /** - * Convert Boolean terms to bitvectors of size 1. - */ - BOOLEAN_TERM_CONVERT_TO_BITVECTORS, - /** - * Convert Boolean terms to enumerations in the Datatypes theory. - */ - BOOLEAN_TERM_CONVERT_TO_DATATYPES, - /** - * Convert Boolean terms to enumerations in the Datatypes theory IF - * used in a datatypes context, otherwise to a bitvector of size 1. - */ - BOOLEAN_TERM_CONVERT_NATIVE - -}; - }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; - }/* CVC4 namespace */ #endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/options/booleans_options b/src/options/booleans_options index a150c1d83..6143f4f67 100644 --- a/src/options/booleans_options +++ b/src/options/booleans_options @@ -5,7 +5,5 @@ module BOOLEANS "options/booleans_options.h" Boolean theory -option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler stringToBooleanTermConversionMode - policy for converting Boolean terms endmodule diff --git a/src/options/expr_options b/src/options/expr_options index 75354a010..d6997b2dd 100644 --- a/src/options/expr_options +++ b/src/options/expr_options @@ -26,8 +26,5 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul option typeChecking type-checking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking never type check expressions -option biasedITERemoval --biased-ites bool :default false - try the new remove ite pass that is biased against term ites appearing - endmodule diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 0dac42362..c0aa67cd4 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1061,41 +1061,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionEx } } - -// theory/booleans/options_handlers.h -const std::string OptionsHandler::s_booleanTermConversionModeHelp = "\ -Boolean term conversion modes currently supported by the\n\ ---boolean-term-conversion-mode option:\n\ -\n\ -bitvectors [default]\n\ -+ Boolean terms are converted to bitvectors of size 1.\n\ -\n\ -datatypes\n\ -+ Boolean terms are converted to enumerations in the Datatype theory.\n\ -\n\ -native\n\ -+ Boolean terms are converted in a \"natural\" way depending on where they\n\ - are used. If in a datatype context, they are converted to an enumeration.\n\ - Elsewhere, they are converted to a bitvector of size 1.\n\ -"; - -theory::booleans::BooleanTermConversionMode OptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){ - if(optarg == "bitvectors") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS; - } else if(optarg == "datatypes") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES; - } else if(optarg == "native") { - return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE; - } else if(optarg == "help") { - puts(s_booleanTermConversionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + - optarg + "'. Try --boolean-term-conversion-mode help."); - } -} - - // theory/uf/options_handlers.h const std::string OptionsHandler::s_ufssModeHelp = "\ UF strong solver options currently supported by the --uf-ss option:\n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 45aea7b79..248f15c98 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -118,10 +118,6 @@ public: theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException); - - // theory/booleans/options_handlers.h - theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); - // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException); |