diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/options.h | 12 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 202 | ||||
| -rw-r--r-- | src/options/options_handler.h | 163 | ||||
| -rw-r--r-- | src/options/options_template.cpp | 11 |
4 files changed, 246 insertions, 142 deletions
diff --git a/src/options/options.h b/src/options/options.h index ce0e3c347..608b9906a 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -321,11 +321,13 @@ public: * * This function uses getopt_long() and is not thread safe. * + * Throws OptionException on failures. + * * Preconditions: options and argv must be non-null. */ static std::vector<std::string> parseOptions(Options* options, - int argc, char* argv[]) - throw(OptionException); + int argc, + char* argv[]); /** * Get the setting for all options. @@ -534,7 +536,6 @@ public: void flushOut(); private: - /** * Internal procedure for implementing the parseOptions function. * Initializes the options object based on the given command-line @@ -543,12 +544,13 @@ public: * * This is not thread safe. * + * Throws OptionException on failures. + * * Preconditions: options, extender and nonoptions are non-null. */ static void parseOptionsRecursive(Options* options, options::ArgumentExtender* extender, - std::vector<std::string>* nonoptions) - throw(OptionException); + std::vector<std::string>* nonoptions); };/* class Options */ }/* CVC4 namespace */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index e8a243448..c29cfc4d2 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -60,7 +60,6 @@ void OptionsHandler::notifyForceLogic(const std::string& option){ } void OptionsHandler::notifyBeforeSearch(const std::string& option) - throw(ModalException) { try{ d_options->d_beforeSearchListeners.notify(); @@ -89,8 +88,9 @@ void OptionsHandler::notifyRlimitPer(const std::string& option) { d_options->d_rlimitPerListeners.notify(); } - -unsigned long OptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException) { +unsigned long OptionsHandler::tlimitHandler(std::string option, + std::string optarg) +{ unsigned long ms; std::istringstream convert(optarg); if (!(convert >> ms)) { @@ -99,7 +99,9 @@ unsigned long OptionsHandler::tlimitHandler(std::string option, std::string opta return ms; } -unsigned long OptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { +unsigned long OptionsHandler::tlimitPerHandler(std::string option, + std::string optarg) +{ unsigned long ms; std::istringstream convert(optarg); @@ -109,7 +111,9 @@ unsigned long OptionsHandler::tlimitPerHandler(std::string option, std::string o return ms; } -unsigned long OptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) { +unsigned long OptionsHandler::rlimitHandler(std::string option, + std::string optarg) +{ unsigned long ms; std::istringstream convert(optarg); @@ -119,8 +123,9 @@ unsigned long OptionsHandler::rlimitHandler(std::string option, std::string opta return ms; } - -unsigned long OptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { +unsigned long OptionsHandler::rlimitPerHandler(std::string option, + std::string optarg) +{ unsigned long ms; std::istringstream convert(optarg); @@ -176,7 +181,9 @@ Heuristic pivot rules available:\n\ The variable order\n\ "; -ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) { +ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode( + std::string option, std::string optarg) +{ if(optarg == "all") { return ALL_PRESOLVE_LEMMAS; } else if(optarg == "none") { @@ -194,7 +201,9 @@ ArithUnateLemmaMode OptionsHandler::stringToArithUnateLemmaMode(std::string opti } } -ArithPropagationMode OptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) { +ArithPropagationMode OptionsHandler::stringToArithPropagationMode( + std::string option, std::string optarg) +{ if(optarg == "none") { return NO_PROP; } else if(optarg == "unate") { @@ -212,7 +221,9 @@ ArithPropagationMode OptionsHandler::stringToArithPropagationMode(std::string op } } -ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) { +ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule( + std::string option, std::string optarg) +{ if(optarg == "min") { return MINIMUM_AMOUNT; } else if(optarg == "varord") { @@ -554,7 +565,9 @@ all \n\ \n\ "; -theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode( + std::string option, std::string optarg) +{ if(optarg == "pre-full") { return theory::quantifiers::INST_WHEN_PRE_FULL; } else if(optarg == "full") { @@ -576,13 +589,17 @@ theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::stri } } -void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) { +void OptionsHandler::checkInstWhenMode(std::string option, + theory::quantifiers::InstWhenMode mode) +{ if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) { throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); } } -theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode( + std::string option, std::string optarg) +{ if(optarg == "none") { return theory::quantifiers::LITERAL_MATCH_NONE; } else if(optarg == "use") { @@ -600,11 +617,14 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s } } -void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) { - +void OptionsHandler::checkLiteralMatchMode( + std::string option, theory::quantifiers::LiteralMatchMode mode) +{ } -theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode( + std::string option, std::string optarg) +{ if(optarg == "gen-ev") { return theory::quantifiers::MBQI_GEN_EVAL; } else if(optarg == "none") { @@ -626,11 +646,14 @@ theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string optio } } +void OptionsHandler::checkMbqiMode(std::string option, + theory::quantifiers::MbqiMode mode) +{ +} -void OptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {} - - -theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode( + std::string option, std::string optarg) +{ if(optarg == "default") { return theory::quantifiers::QCF_WHEN_MODE_DEFAULT; } else if(optarg == "last-call") { @@ -648,7 +671,9 @@ theory::quantifiers::QcfWhenMode OptionsHandler::stringToQcfWhenMode(std::string } } -theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, + std::string optarg) +{ if(optarg == "conflict") { return theory::quantifiers::QCF_CONFLICT_ONLY; } else if(optarg == "default" || optarg == "prop-eq") { @@ -664,7 +689,9 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, } } -theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode( + std::string option, std::string optarg) +{ if(optarg == "use") { return theory::quantifiers::USER_PAT_MODE_USE; } else if(optarg == "default" || optarg == "trust") { @@ -684,7 +711,9 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string } } -theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode( + std::string option, std::string optarg) +{ if(optarg == "default" || optarg == "min") { return theory::quantifiers::TRIGGER_SEL_MIN; } else if(optarg == "max") { @@ -704,7 +733,10 @@ theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std:: } } -theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::TriggerActiveSelMode +OptionsHandler::stringToTriggerActiveSelMode(std::string option, + std::string optarg) +{ if(optarg == "default" || optarg == "all") { return theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL; } else if(optarg == "min") { @@ -720,7 +752,9 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS } } -theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode( + std::string option, std::string optarg) +{ if(optarg== "default" || optarg== "simple" ) { return theory::quantifiers::PRENEX_QUANT_SIMPLE; } else if(optarg == "none") { @@ -738,7 +772,9 @@ theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std } } -theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException) { +theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option, + std::string optarg) +{ if(optarg == "direct") { return theory::SYGUS_FAIR_DIRECT; } else if(optarg == "default" || optarg == "dt-size") { @@ -758,7 +794,9 @@ theory::SygusFairMode OptionsHandler::stringToSygusFairMode(std::string option, } } -theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode( + std::string option, std::string optarg) +{ if(optarg == "all" ) { return theory::quantifiers::TERM_DB_ALL; } else if(optarg == "relevant") { @@ -772,7 +810,9 @@ theory::quantifiers::TermDbMode OptionsHandler::stringToTermDbMode(std::string o } } -theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode( + std::string option, std::string optarg) +{ if(optarg == "all" ) { return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL; } else if(optarg == "simple") { @@ -789,7 +829,7 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s } theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode( - std::string option, std::string optarg) throw(OptionException) + std::string option, std::string optarg) { if (optarg == "eq-slack") { @@ -816,7 +856,10 @@ theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode( } } -theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::CegqiSingleInvMode +OptionsHandler::stringToCegqiSingleInvMode(std::string option, + std::string optarg) +{ if(optarg == "none" ) { return theory::quantifiers::CEGQI_SI_MODE_NONE; } else if(optarg == "use" || optarg == "default") { @@ -834,7 +877,10 @@ theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMo } } -theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::SygusInvTemplMode +OptionsHandler::stringToSygusInvTemplMode(std::string option, + std::string optarg) +{ if(optarg == "none" ) { return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE; } else if(optarg == "pre") { @@ -850,7 +896,9 @@ theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode } } -theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode( + std::string option, std::string optarg) +{ if(optarg == "all" ) { return theory::quantifiers::MACROS_QUANT_MODE_ALL; } else if(optarg == "ground") { @@ -866,7 +914,9 @@ theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(std } } -theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode( + std::string option, std::string optarg) +{ if(optarg == "none" ) { return theory::quantifiers::QUANT_DSPLIT_MODE_NONE; } else if(optarg == "default") { @@ -882,7 +932,9 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std } } -theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode( + std::string option, std::string optarg) +{ if(optarg == "none" ) { return theory::quantifiers::QUANT_REP_MODE_EE; } else if(optarg == "first" || optarg == "default") { @@ -898,8 +950,9 @@ theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::stri } } - -theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException) { +theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode( + std::string option, std::string optarg) +{ if(optarg == "none" ) { return theory::quantifiers::FMF_BOUND_MIN_NONE; } else if(optarg == "int" || optarg == "default") { @@ -918,7 +971,8 @@ theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode(std } // theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { +void OptionsHandler::abcEnabledBuild(std::string option, bool value) +{ #ifndef CVC4_USE_ABC if(value) { std::stringstream ss; @@ -928,7 +982,8 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(Optio #endif /* CVC4_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(std::string option, std::string value) throw(OptionException) { +void OptionsHandler::abcEnabledBuild(std::string option, std::string value) +{ #ifndef CVC4_USE_ABC if(!value.empty()) { std::stringstream ss; @@ -938,8 +993,8 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro #endif /* CVC4_USE_ABC */ } -void OptionsHandler::satSolverEnabledBuild(std::string option, - bool value) throw(OptionException) { +void OptionsHandler::satSolverEnabledBuild(std::string option, bool value) +{ #ifndef CVC4_USE_CRYPTOMINISAT if(value) { std::stringstream ss; @@ -950,7 +1005,8 @@ void OptionsHandler::satSolverEnabledBuild(std::string option, } void OptionsHandler::satSolverEnabledBuild(std::string option, - std::string value) throw(OptionException) { + std::string value) +{ #ifndef CVC4_USE_CRYPTOMINISAT if(!value.empty()) { std::stringstream ss; @@ -969,7 +1025,8 @@ cryptominisat\n\ "; theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, - std::string optarg) throw(OptionException) { + std::string optarg) +{ if(optarg == "minisat") { return theory::bv::SAT_SOLVER_MINISAT; } else if(optarg == "cryptominisat") { @@ -1015,7 +1072,9 @@ eager\n\ + Bitblast eagerly to bv SAT solver\n\ "; -theory::bv::BitblastMode OptionsHandler::stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) { +theory::bv::BitblastMode OptionsHandler::stringToBitblastMode( + std::string option, std::string optarg) +{ if(optarg == "lazy") { if (!options::bitvectorPropagate.wasSetByUser()) { options::bitvectorPropagate.set(true); @@ -1078,7 +1137,9 @@ off\n\ + Turn slicer off\n\ "; -theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) { +theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode( + std::string option, std::string optarg) +{ if(optarg == "auto") { return theory::bv::BITVECTOR_SLICER_AUTO; } else if(optarg == "on") { @@ -1094,7 +1155,8 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode(std::string option } } -void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) { +void OptionsHandler::setBitblastAig(std::string option, bool arg) +{ if(arg) { if(options::bitblastMode.wasSetByUser()) { if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) { @@ -1125,7 +1187,9 @@ none \n\ \n\ "; -theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) { +theory::uf::UfssMode OptionsHandler::stringToUfssMode(std::string option, + std::string optarg) +{ if(optarg == "default" || optarg == "full" ) { return theory::uf::UF_SS_FULL; } else if(optarg == "no-minimal") { @@ -1205,7 +1269,9 @@ szs\n\ + Print instantiations as SZS compliant proof.\n\ "; -ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) { +ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, + std::string optarg) +{ if(optarg == "default") { return MODEL_FORMAT_MODE_DEFAULT; } else if(optarg == "table") { @@ -1219,7 +1285,9 @@ ModelFormatMode OptionsHandler::stringToModelFormatMode(std::string option, std: } } -InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) { +InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, + std::string optarg) +{ if(optarg == "default") { return INST_FORMAT_MODE_DEFAULT; } else if(optarg == "szs") { @@ -1248,7 +1316,9 @@ justification-stoponly\n\ + Use the justification heuristic only to stop early, not for decisions\n\ "; -decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) { +decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option, + std::string optarg) +{ options::decisionStopOnly.set(false); if(optarg == "internal") { @@ -1267,7 +1337,9 @@ decision::DecisionMode OptionsHandler::stringToDecisionMode(std::string option, } } -decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) { +decision::DecisionWeightInternal OptionsHandler::stringToDecisionWeightInternal( + std::string option, std::string optarg) +{ if(optarg == "off") return decision::DECISION_WEIGHT_INTERNAL_OFF; else if(optarg == "max") @@ -1294,9 +1366,9 @@ none\n\ + do not perform nonclausal simplification\n\ "; - - -SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) { +SimplificationMode OptionsHandler::stringToSimplificationMode( + std::string option, std::string optarg) +{ if(optarg == "batch") { return SIMPLIFICATION_MODE_BATCH; } else if(optarg == "none") { @@ -1330,7 +1402,7 @@ sygus-standard \n\ "; SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode( - std::string option, std::string optarg) throw(OptionException) + std::string option, std::string optarg) { if (optarg == "status") { @@ -1367,8 +1439,8 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) options::interactiveMode.set(value); } - -void OptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) { +void OptionsHandler::proofEnabledBuild(std::string option, bool value) +{ #ifndef CVC4_PROOF if(value) { std::stringstream ss; @@ -1419,7 +1491,8 @@ void OptionsHandler::notifySetReplayLogFilename(std::string option) { d_options->d_setReplayFilenameListeners.notify(); } -void OptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) { +void OptionsHandler::statsEnabledBuild(std::string option, bool value) +{ #ifndef CVC4_STATISTICS_ON if(value) { std::stringstream ss; @@ -1433,7 +1506,8 @@ void OptionsHandler::threadN(std::string option) { throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); } -void OptionsHandler::notifyDumpMode(std::string option) throw(OptionException) { +void OptionsHandler::notifyDumpMode(std::string option) +{ d_options->d_setDumpModeListeners.notify(); } @@ -1655,8 +1729,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg) Trace.on(optarg); } - -OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) { +OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, + std::string optarg) +{ if(optarg == "help") { options::languageHelp.set(true); return language::output::LANG_AUTO; @@ -1672,7 +1747,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::s Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) { +InputLanguage OptionsHandler::stringToInputLanguage(std::string option, + std::string optarg) +{ if(optarg == "help") { options::languageHelp.set(true); return language::input::LANG_AUTO; @@ -1688,7 +1765,8 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::str } /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) { +void OptionsHandler::setVerbosity(std::string option, int value) +{ if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&CVC4::null_os); TraceChannel.setStream(&CVC4::null_os); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 23a6be501..e7bd87ebd 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -43,10 +43,14 @@ namespace CVC4 { namespace options { +/** + * Class that responds to command line options being set. + * + * Most functions can throw an OptionException on failure. + */ class OptionsHandler { public: OptionsHandler(Options* options); - virtual ~OptionsHandler() {} void unsignedGreater0(const std::string& option, unsigned value) { options::greater(0)(option, value); @@ -64,65 +68,76 @@ public: options::less_equal(1.0)(option, value); } - // DONE - // decision/options_handlers.h - // expr/options_handlers.h - // main/options_handlers.h - // options/base_options_handlers.h - // printer/options_handlers.h - // smt/options_handlers.h - // theory/options_handlers.h - // theory/booleans/options_handlers.h - // theory/uf/options_handlers.h - // theory/bv/options_handlers.h - // theory/quantifiers/options_handlers.h // theory/arith/options_handlers.h - - - // theory/arith/options_handlers.h - ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException); - ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException); - ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException); + 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) throw(OptionException); - void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException); - theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException); - void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException); - theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException); - void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException); - theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::TriggerActiveSelMode stringToTriggerActiveSelMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); + 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) throw(OptionException); - theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException); - theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode(std::string option, std::string optarg) throw(OptionException); - theory::SygusFairMode stringToSygusFairMode(std::string option, std::string optarg) throw(OptionException); + std::string option, std::string optarg); + theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( + std::string option, std::string optarg); + theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( + 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::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode( + std::string option, std::string optarg); + theory::SygusFairMode stringToSygusFairMode(std::string option, + std::string optarg); // theory/bv/options_handlers.h - void abcEnabledBuild(std::string option, bool value) throw(OptionException); - void abcEnabledBuild(std::string option, std::string value) throw(OptionException); - void satSolverEnabledBuild(std::string option, bool value) throw(OptionException); - void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException); + 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) throw(OptionException); - theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); - void setBitblastAig(std::string option, bool arg) throw(OptionException); + theory::bv::BitblastMode stringToBitblastMode(std::string option, + std::string optarg); + theory::bv::BvSlicerMode stringToBvSlicerMode(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::SatSolverMode stringToSatSolver(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); + theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg); // theory/options_handlers.h theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); @@ -131,23 +146,31 @@ public: // printer/options_handlers.h - ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException); - InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException); + 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) throw(OptionException); - decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException); - + decision::DecisionMode stringToDecisionMode(std::string option, + std::string optarg); + decision::DecisionWeightInternal stringToDecisionWeightInternal( + std::string option, std::string optarg); /* smt/options_handlers.h */ void notifyForceLogic(const std::string& option); - void notifyBeforeSearch(const std::string& option) throw(ModalException); - void notifyDumpMode(std::string option) throw(OptionException); - SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); - SygusSolutionOutMode stringToSygusSolutionOutMode( - std::string option, std::string optarg) throw(OptionException); + + /** + * Throws a ModalException if this option is being set after final + * initialization. + */ + void notifyBeforeSearch(const std::string& option); + void notifyDumpMode(std::string option); + SimplificationMode stringToSimplificationMode(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) throw(OptionException); + void proofEnabledBuild(std::string option, bool value); void LFSCEnabledBuild(std::string option, bool value); void notifyDumpToFile(std::string option); void notifySetRegularOutputChannel(std::string option); @@ -155,12 +178,12 @@ public: std::string checkReplayFilename(std::string option, std::string optarg); void notifySetReplayLogFilename(std::string option); - void statsEnabledBuild(std::string option, bool value) throw(OptionException); + void statsEnabledBuild(std::string option, bool value); - unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException); - unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException); - unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException); - unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException); + unsigned long tlimitHandler(std::string option, std::string optarg); + unsigned long tlimitPerHandler(std::string option, std::string optarg); + unsigned long rlimitHandler(std::string option, std::string optarg); + unsigned long rlimitPerHandler(std::string option, std::string optarg); void notifyTlimit(const std::string& option); void notifyTlimitPer(const std::string& option); @@ -183,11 +206,11 @@ public: void threadN(std::string option); /* options/base_options_handlers.h */ - void setVerbosity(std::string option, int value) throw(OptionException); + void setVerbosity(std::string option, int value); void increaseVerbosity(std::string option); void decreaseVerbosity(std::string option); - OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException); - InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException); + OutputLanguage stringToOutputLanguage(std::string option, std::string optarg); + InputLanguage stringToInputLanguage(std::string option, std::string optarg); void enableTraceTag(std::string option, std::string optarg); void enableDebugTag(std::string option, std::string optarg); void notifyPrintSuccess(std::string option); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 9de47b388..43d825488 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -551,11 +551,13 @@ public: * Parse argc/argv and put the result into a CVC4::Options. * The return value is what's left of the command line (that is, the * non-option arguments). + * + * Throws OptionException on failures. */ std::vector<std::string> Options::parseOptions(Options* options, - int argc, char* argv[]) - throw(OptionException) { - + int argc, + char* argv[]) +{ Assert(options != NULL); Assert(argv != NULL); @@ -599,8 +601,7 @@ std::vector<std::string> Options::parseOptions(Options* options, void Options::parseOptionsRecursive(Options* options, ArgumentExtender* extender, std::vector<std::string>* nonoptions) - throw(OptionException) { - +{ int argc; char** argv; |