diff options
Diffstat (limited to 'src/options/options_handler.h')
-rw-r--r-- | src/options/options_handler.h | 181 |
1 files changed, 20 insertions, 161 deletions
diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 2e372a00c..a395bb453 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -23,24 +23,14 @@ #include <string> #include "base/modal_exception.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" -#include "options/bool_to_bv_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/datatypes_modes.h" -#include "options/decision_mode.h" +#include "options/bv_options.h" +#include "options/decision_options.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" #include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/smt_modes.h" -#include "options/strings_modes.h" -#include "options/sygus_out_mode.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" +#include "options/quantifiers_options.h" namespace CVC4 { namespace options { @@ -70,117 +60,29 @@ public: options::less_equal(1.0)(option, value); } - // theory/arith/options_handlers.h - ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, - std::string optarg); - ArithPropagationMode stringToArithPropagationMode(std::string option, - std::string optarg); - ErrorSelectionRule stringToErrorSelectionRule(std::string option, - std::string optarg); - // theory/quantifiers/options_handlers.h - theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, - std::string optarg); - void checkInstWhenMode(std::string option, - theory::quantifiers::InstWhenMode mode); - theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode( - std::string option, std::string optarg); - void checkLiteralMatchMode(std::string option, - theory::quantifiers::LiteralMatchMode mode); - theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, - std::string optarg); - void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode); - theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, - std::string optarg); - theory::quantifiers::QcfMode stringToQcfMode(std::string option, - std::string optarg); - theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, - std::string optarg); - theory::quantifiers::TriggerSelMode stringToTriggerSelMode( - std::string option, std::string optarg); - theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode( - std::string option, std::string optarg); - theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode( - std::string option, std::string optarg); - theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, - std::string optarg); - theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode( - std::string option, std::string optarg); - theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode( - std::string option, std::string optarg); - theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( - std::string option, std::string optarg); - theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode( - std::string option, std::string optarg); - theory::quantifiers::CegisSampleMode stringToCegisSampleMode( - std::string option, std::string optarg); - theory::quantifiers::SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode( - std::string option, std::string optarg); - theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode( - std::string option, std::string optarg); - theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( - std::string option, std::string optarg); - theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( - std::string option, std::string optarg); - theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode( - std::string option, std::string optarg); - theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode( - std::string option, std::string optarg); - theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode( - std::string option, std::string optarg); - theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode( - std::string option, std::string optarg); - theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, - std::string optarg); - theory::SygusFairMode stringToSygusFairMode(std::string option, - std::string optarg); + void checkInstWhenMode(std::string option, InstWhenMode mode); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value); void abcEnabledBuild(std::string option, std::string value); - void satSolverEnabledBuild(std::string option, bool value); - void satSolverEnabledBuild(std::string option, std::string optarg); - - theory::bv::BitblastMode stringToBitblastMode(std::string option, - std::string optarg); - theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, - std::string optarg); - preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option, - std::string optarg); - void setBitblastAig(std::string option, bool arg); - - theory::bv::SatSolverMode stringToSatSolver(std::string option, - std::string optarg); - theory::bv::BvProofFormat stringToBvProofFormat(std::string option, - std::string optarg); - theory::bv::BvOptimizeSatProof stringToBvOptimizeSatProof(std::string option, - std::string optarg); + template<class T> void checkSatSolverEnabled(std::string option, T m); - theory::strings::ProcessLoopMode stringToStringsProcessLoopMode( - std::string option, std::string optarg); - theory::strings::RegExpInterMode stringToRegExpInterMode(std::string option, - std::string optarg); + void checkBvSatSolver(std::string option, SatSolverMode m); + void checkBitblastMode(std::string option, BitblastMode m); - // theory/uf/options_handlers.h - theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); + void setBitblastAig(std::string option, bool arg); // theory/options_handlers.h - theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); void notifyUseTheoryList(std::string option); std::string handleUseTheoryList(std::string option, std::string optarg); - // printer/options_handlers.h - ModelFormatMode stringToModelFormatMode(std::string option, - std::string optarg); InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); // decision/options_handlers.h - decision::DecisionMode stringToDecisionMode(std::string option, - std::string optarg); - decision::DecisionWeightInternal stringToDecisionWeightInternal( - std::string option, std::string optarg); + void setDecisionModeStopOnly(std::string option, DecisionMode m); /** * Throws a ModalException if this option is being set after final @@ -188,13 +90,6 @@ public: */ void notifyBeforeSearch(const std::string& option); void notifyDumpMode(std::string option); - SimplificationMode stringToSimplificationMode(std::string option, - std::string optarg); - ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg); - BlockModelsMode stringToBlockModelsMode(std::string option, - std::string optarg); - SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option, - std::string optarg); void setProduceAssertions(std::string option, bool value); void proofEnabledBuild(std::string option, bool value); void LFSCEnabledBuild(std::string option, bool value); @@ -244,56 +139,20 @@ public: Options* d_options; /* Help strings */ - static const std::string s_bitblastingModeHelp; - static const std::string s_bvSatSolverHelp; - static const std::string s_bvProofFormatHelp; - static const std::string s_bvOptimizeSatProofHelp; - static const std::string s_booleanTermConversionModeHelp; - static const std::string s_bvSlicerModeHelp; - static const std::string s_stringsProcessLoopModeHelp; - static const std::string s_regExpInterModeHelp; - static const std::string s_boolToBVModeHelp; - static const std::string s_cegqiFairModeHelp; - static const std::string s_decisionModeHelp; - static const std::string s_instFormatHelp ; - static const std::string s_instWhenHelp; - static const std::string s_iteLiftQuantHelp; - static const std::string s_literalMatchHelp; - static const std::string s_macrosQuantHelp; - static const std::string s_quantDSplitHelp; - static const std::string s_quantRepHelp; - static const std::string s_mbqiModeHelp; - static const std::string s_modelFormatHelp; - static const std::string s_prenexQuantModeHelp; - static const std::string s_qcfModeHelp; - static const std::string s_qcfWhenModeHelp; - static const std::string s_simplificationHelp; - static const std::string s_modelCoresHelp; - static const std::string s_blockModelsHelp; - static const std::string s_sygusSolutionOutModeHelp; - static const std::string s_cbqiBvIneqModeHelp; - static const std::string s_cegqiSingleInvHelp; - static const std::string s_cegqiSingleInvRconsHelp; - static const std::string s_cegisSampleHelp; - static const std::string s_sygusQueryDumpFileHelp; - static const std::string s_sygusFilterSolHelp; - static const std::string s_sygusInvTemplHelp; - static const std::string s_sygusActiveGenHelp; - static const std::string s_sygusUnifPiHelp; - static const std::string s_sygusGrammarConsHelp; - static const std::string s_termDbModeHelp; - static const std::string s_theoryOfModeHelp; - static const std::string s_triggerSelModeHelp; - static const std::string s_triggerActiveSelModeHelp; - static const std::string s_ufssModeHelp; - static const std::string s_userPatModeHelp; - static const std::string s_fmfBoundMinModeModeHelp; - static const std::string s_errorSelectionRulesHelp; - static const std::string s_arithPropagationModeHelp; - static const std::string s_arithUnateLemmasHelp; + static const std::string s_instFormatHelp; }; /* class OptionHandler */ +template<class T> +void OptionsHandler::checkSatSolverEnabled(std::string option, T m) +{ +#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) + std::stringstream ss; + ss << "option `" << option + << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL"; + throw OptionException(ss.str()); +#endif +} }/* CVC4::options namespace */ }/* CVC4 namespace */ |