diff options
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 117 |
1 files changed, 82 insertions, 35 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1ac5ec56d..e109ab44c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -67,10 +67,11 @@ void throwLazyBBUnsupported(options::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -unsigned long OptionsHandler::limitHandler(std::string option, - std::string optarg) +uint64_t OptionsHandler::limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg) { - unsigned long ms; + uint64_t ms; std::istringstream convert(optarg); if (!(convert >> ms)) { @@ -80,14 +81,18 @@ unsigned long OptionsHandler::limitHandler(std::string option, return ms; } -void OptionsHandler::setResourceWeight(std::string option, std::string optarg) +void OptionsHandler::setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg) { d_options->base.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h -void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) +void OptionsHandler::checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode) { if (mode == InstWhenMode::PRE_FULL) { @@ -97,7 +102,9 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) } // theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(std::string option, bool value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_USE_ABC if(value) { @@ -110,7 +117,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(std::string option, std::string value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value) { #ifndef CVC5_USE_ABC if(!value.empty()) { @@ -123,7 +132,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) +void OptionsHandler::checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m) { if (m == SatSolverMode::CRYPTOMINISAT && !Configuration::isBuiltWithCryptominisat()) @@ -166,7 +177,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) } } -void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) +void OptionsHandler::checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m) { if (m == options::BitblastMode::LAZY) { @@ -185,7 +198,9 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } } -void OptionsHandler::setBitblastAig(std::string option, bool arg) +void OptionsHandler::setBitblastAig(const std::string& option, + const std::string& flag, + bool arg) { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { @@ -211,8 +226,9 @@ szs\n\ + Print instantiations as SZS compliant proof.\n\ "; -InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, - std::string optarg) +InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "default") { return InstFormatMode::DEFAULT; @@ -228,24 +244,30 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, } // decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) +void OptionsHandler::setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m) { d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); } -void OptionsHandler::setProduceAssertions(std::string option, bool value) +void OptionsHandler::setProduceAssertions(const std::string& option, + const std::string& flag, + bool value) { d_options->smt.produceAssertions = value; d_options->smt.interactiveMode = value; } -void OptionsHandler::setStats(const std::string& option, bool value) +void OptionsHandler::setStats(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_STATISTICS_ON if (value) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a statistics-enabled build of cvc5; this binary was not " "built with statistics support"; throw OptionException(ss.str()); @@ -282,18 +304,25 @@ void OptionsHandler::setStats(const std::string& option, bool value) } } -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::threadN(const std::string& option, const std::string& flag) +{ + throw OptionException(flag + " 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\""); } // expr/options_handlers.h -void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { +void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth) +{ if(depth < -1) { throw OptionException("--expr-depth requires a positive argument, or -1."); } } -void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { +void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag) +{ if(dag < 0) { throw OptionException("--dag-thresh requires a nonnegative argument."); } @@ -312,12 +341,16 @@ static void print_config_cond (const char * str, bool cond = false) { print_config(str, cond ? "yes" : "no"); } -void OptionsHandler::copyright(std::string option) { +void OptionsHandler::copyright(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::copyright() << std::endl; exit(0); } -void OptionsHandler::showConfiguration(std::string option) { +void OptionsHandler::showConfiguration(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::about() << std::endl; print_config ("version", Configuration::getVersionString()); @@ -385,7 +418,8 @@ static void printTags(unsigned ntags, char const* const* tags) std::cout << std::endl; } -void OptionsHandler::showDebugTags(std::string option) +void OptionsHandler::showDebugTags(const std::string& option, + const std::string& flag) { if (!Configuration::isDebugBuild()) { @@ -399,7 +433,8 @@ void OptionsHandler::showDebugTags(std::string option) exit(0); } -void OptionsHandler::showTraceTags(std::string option) +void OptionsHandler::showTraceTags(const std::string& option, + const std::string& flag) { if (!Configuration::isTracingBuild()) { @@ -431,7 +466,9 @@ static std::string suggestTags(char const* const* validTags, return didYouMean.getMatchAsString(inputTag); } -void OptionsHandler::enableTraceTag(std::string option, std::string optarg) +void OptionsHandler::enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(!Configuration::isTracingBuild()) { @@ -453,7 +490,9 @@ void OptionsHandler::enableTraceTag(std::string option, std::string optarg) Trace.on(optarg); } -void OptionsHandler::enableDebugTag(std::string option, std::string optarg) +void OptionsHandler::enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if (!Configuration::isDebugBuild()) { @@ -484,8 +523,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg) Trace.on(optarg); } -OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, - std::string optarg) +OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -502,8 +542,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(std::string option, - std::string optarg) +InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -520,7 +561,9 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, } /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(std::string option, int value) +void OptionsHandler::setVerbosity(const std::string& option, + const std::string& flag, + int value) { if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); @@ -550,14 +593,18 @@ void OptionsHandler::setVerbosity(std::string option, int value) } } -void OptionsHandler::increaseVerbosity(std::string option) { +void OptionsHandler::increaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity += 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } -void OptionsHandler::decreaseVerbosity(std::string option) { +void OptionsHandler::decreaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity -= 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } } // namespace options |