summaryrefslogtreecommitdiff
path: root/src/options/options_handler.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r--src/options/options_handler.cpp117
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback