diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-10-01 13:40:05 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-01 20:40:05 +0000 |
commit | b261b0a6031dee3210e569f75f8abdac35b7091c (patch) | |
tree | 765138ffac47751431d25aaad4b8feb4fb680839 /src/options/options_handler.cpp | |
parent | a673f93d1fe80c5a3198d586fd73f08c92246beb (diff) |
Clean options handlers (#7201)
Some cleanup on the option handlers, starting with handlers for base and main options.
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 626 |
1 files changed, 303 insertions, 323 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index bf2def05b..27ab63ae7 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -16,6 +16,7 @@ #include "options/options_handler.h" #include <cerrno> +#include <iostream> #include <ostream> #include <string> @@ -67,155 +68,103 @@ void throwLazyBBUnsupported(options::SatSolverMode m) + indent + "Try --bv-sat-solver=minisat"); } -} // namespace - -OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } - -uint64_t OptionsHandler::limitHandler(const std::string& option, - const std::string& flag, - const std::string& optarg) +static void printTags(const std::vector<std::string>& tags) { - uint64_t ms; - std::istringstream convert(optarg); - if (!(convert >> ms)) + std::cout << "available tags:"; + for (const auto& t : tags) { - throw OptionException("option `" + option - + "` requires a number as an argument"); + std::cout << " " << t << std::endl; } - return ms; + std::cout << std::endl; } -void OptionsHandler::setResourceWeight(const std::string& option, - const std::string& flag, - const std::string& optarg) +std::string suggestTags(const std::vector<std::string>& validTags, + std::string inputTag, + const std::vector<std::string>& additionalTags) { - d_options->base.resourceWeightHolder.emplace_back(optarg); + DidYouMean didYouMean; + didYouMean.addWords(validTags); + didYouMean.addWords(additionalTags); + return didYouMean.getMatchAsString(inputTag); } -// theory/quantifiers/options_handlers.h - -void OptionsHandler::checkInstWhenMode(const std::string& option, - const std::string& flag, - InstWhenMode mode) -{ - if (mode == InstWhenMode::PRE_FULL) - { - throw OptionException(std::string("Mode pre-full for ") + option - + " is not supported in this release."); - } -} +} // namespace -// theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(const std::string& option, - const std::string& flag, - bool value) -{ -#ifndef CVC5_USE_ABC - if(value) { - std::stringstream ss; - ss << "option `" << option - << "' requires an abc-enabled build of cvc5; this binary was not built " - "with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC5_USE_ABC */ -} +OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -void OptionsHandler::abcEnabledBuild(const std::string& option, - const std::string& flag, - const std::string& value) +void OptionsHandler::setErrStream(const std::string& option, + const std::string& flag, + const ManagedErr& me) { -#ifndef CVC5_USE_ABC - if(!value.empty()) { - std::stringstream ss; - ss << "option `" << option - << "' requires an abc-enabled build of cvc5; this binary was not built " - "with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC5_USE_ABC */ + Debug.setStream(me); + Warning.setStream(me); + CVC5Message.setStream(me); + Notice.setStream(me); + Chat.setStream(me); + Trace.setStream(me); } -void OptionsHandler::checkBvSatSolver(const std::string& option, +void OptionsHandler::languageIsNotAST(const std::string& option, const std::string& flag, - SatSolverMode m) + Language lang) { - if (m == SatSolverMode::CRYPTOMINISAT - && !Configuration::isBuiltWithCryptominisat()) - { - std::stringstream ss; - ss << "option `" << option - << "' requires a CryptoMiniSat build of cvc5; this binary was not built " - "with CryptoMiniSat support"; - throw OptionException(ss.str()); - } - - if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) - { - std::stringstream ss; - ss << "option `" << option - << "' requires a Kissat build of cvc5; this binary was not built with " - "Kissat support"; - throw OptionException(ss.str()); - } - - if (d_options->bv.bvSolver != options::BVSolver::BITBLAST - && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL - || m == SatSolverMode::KISSAT)) + if (lang == Language::LANG_AST) { - if (d_options->bv.bitblastMode == options::BitblastMode::LAZY - && d_options->bv.bitblastModeWasSetByUser) - { - throwLazyBBUnsupported(m); - } - options::bv::setDefaultBitvectorToBool(*d_options, true); + throw OptionException("Language LANG_AST is not allowed for " + flag); } } -void OptionsHandler::checkBitblastMode(const std::string& option, - const std::string& flag, - BitblastMode m) +void OptionsHandler::applyOutputLanguage(const std::string& option, + const std::string& flag, + Language lang) { - if (m == options::BitblastMode::LAZY) - { - options::bv::setDefaultBitvectorPropagate(*d_options, true); - options::bv::setDefaultBitvectorEqualitySolver(*d_options, true); - options::bv::setDefaultBitvectorInequalitySolver(*d_options, true); - options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true); - if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT) - { - throwLazyBBUnsupported(d_options->bv.bvSatSolver); - } - } - else if (m == BitblastMode::EAGER) - { - options::bv::setDefaultBitvectorToBool(*d_options, true); - } + d_options->base.out << language::SetLanguage(lang); } -void OptionsHandler::setBitblastAig(const std::string& option, - const std::string& flag, - bool arg) +void OptionsHandler::setVerbosity(const std::string& option, + const std::string& flag, + int value) { - if(arg) { - if (d_options->bv.bitblastModeWasSetByUser) { - if (d_options->bv.bitblastMode != options::BitblastMode::EAGER) - { - throw OptionException("bitblast-aig must be used with eager bitblaster"); - } + if(Configuration::isMuzzledBuild()) { + DebugChannel.setStream(&cvc5::null_os); + TraceChannel.setStream(&cvc5::null_os); + NoticeChannel.setStream(&cvc5::null_os); + ChatChannel.setStream(&cvc5::null_os); + MessageChannel.setStream(&cvc5::null_os); + WarningChannel.setStream(&cvc5::null_os); + } else { + if(value < 2) { + ChatChannel.setStream(&cvc5::null_os); } else { - options::BitblastMode mode = stringToBitblastMode("eager"); - d_options->bv.bitblastMode = mode; + ChatChannel.setStream(&std::cout); + } + if(value < 1) { + NoticeChannel.setStream(&cvc5::null_os); + } else { + NoticeChannel.setStream(&std::cout); + } + if(value < 0) { + MessageChannel.setStream(&cvc5::null_os); + WarningChannel.setStream(&cvc5::null_os); + } else { + MessageChannel.setStream(&std::cout); + WarningChannel.setStream(&std::cerr); } } } -void OptionsHandler::setProduceAssertions(const std::string& option, - const std::string& flag, - bool value) +void OptionsHandler::decreaseVerbosity(const std::string& option, + const std::string& flag) { - d_options->smt.produceAssertions = value; - d_options->smt.interactiveMode = value; + d_options->base.verbosity -= 1; + setVerbosity(option, flag, d_options->base.verbosity); +} + +void OptionsHandler::increaseVerbosity(const std::string& option, + const std::string& flag) +{ + d_options->base.verbosity += 1; + setVerbosity(option, flag, d_options->base.verbosity); } void OptionsHandler::setStats(const std::string& option, @@ -232,70 +181,117 @@ void OptionsHandler::setStats(const std::string& option, throw OptionException(ss.str()); } #endif /* CVC5_STATISTICS_ON */ - std::string opt = option; - if (option.substr(0, 2) == "--") + if (!value) { - opt = opt.substr(2); + d_options->base.statisticsAll = false; + d_options->base.statisticsEveryQuery = false; + d_options->base.statisticsExpert = false; } +} + +void OptionsHandler::setStatsDetail(const std::string& option, + const std::string& flag, + bool value) +{ +#ifndef CVC5_STATISTICS_ON if (value) { - if (opt == options::base::statisticsAll__name) - { - d_options->base.statistics = true; - } - else if (opt == options::base::statisticsEveryQuery__name) - { - d_options->base.statistics = true; - } - else if (opt == options::base::statisticsExpert__name) + std::stringstream ss; + ss << "option `" << flag + << "' requires a statistics-enabled build of cvc5; this binary was not " + "built with statistics support"; + throw OptionException(ss.str()); + } +#endif /* CVC5_STATISTICS_ON */ + if (value) + { + d_options->base.statistics = true; + } +} + +void OptionsHandler::enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ + if(!Configuration::isTracingBuild()) + { + throw OptionException("trace tags not available in non-tracing builds"); + } + else if(!Configuration::isTraceTag(optarg.c_str())) + { + if (optarg == "help") { - d_options->base.statistics = true; + printTags(Configuration::getTraceTags()); + std::exit(0); } + + throw OptionException( + std::string("trace tag ") + optarg + std::string(" not available.") + + suggestTags(Configuration::getTraceTags(), optarg, {})); } - else + Trace.on(optarg); +} + +void OptionsHandler::enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ + if (!Configuration::isDebugBuild()) { - if (opt == options::base::statistics__name) + throw OptionException("debug tags not available in non-debug builds"); + } + else if (!Configuration::isTracingBuild()) + { + throw OptionException("debug tags not available in non-tracing builds"); + } + + if (!Configuration::isDebugTag(optarg.c_str()) + && !Configuration::isTraceTag(optarg.c_str())) + { + if (optarg == "help") { - d_options->base.statisticsAll = false; - d_options->base.statisticsEveryQuery = false; - d_options->base.statisticsExpert = false; + printTags(Configuration::getDebugTags()); + std::exit(0); } + + throw OptionException(std::string("debug tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getDebugTags(), + optarg, + Configuration::getTraceTags())); } + Debug.on(optarg); + Trace.on(optarg); } -void OptionsHandler::threadN(const std::string& option, const std::string& flag) +void OptionsHandler::enableOutputTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { - 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\""); + d_options->base.outputTagHolder.set( + static_cast<size_t>(stringToOutputTag(optarg))); } -// expr/options_handlers.h -void OptionsHandler::setDefaultExprDepth(const std::string& option, - const std::string& flag, - int depth) +void OptionsHandler::setPrintSuccess(const std::string& option, + const std::string& flag, + bool value) { - Debug.getStream() << expr::ExprSetDepth(depth); - Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); - Chat.getStream() << expr::ExprSetDepth(depth); - CVC5Message.getStream() << expr::ExprSetDepth(depth); - Warning.getStream() << expr::ExprSetDepth(depth); + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + CVC5Message.getStream() << Command::printsuccess(value); + Warning.getStream() << Command::printsuccess(value); + *d_options->base.out << Command::printsuccess(value); } -void OptionsHandler::setDefaultDagThresh(const std::string& option, - const std::string& flag, - int dag) +void OptionsHandler::setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg) { - Debug.getStream() << expr::ExprDag(dag); - Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); - Chat.getStream() << expr::ExprDag(dag); - CVC5Message.getStream() << expr::ExprDag(dag); - Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); + d_options->base.resourceWeightHolder.emplace_back(optarg); } -// main/options_handlers.h - static void print_config (const char * str, std::string config) { std::string s(str); unsigned sz = 14; @@ -307,13 +303,6 @@ static void print_config_cond (const char * str, bool cond = false) { print_config(str, cond ? "yes" : "no"); } -void OptionsHandler::copyright(const std::string& option, - const std::string& flag) -{ - std::cout << Configuration::copyright() << std::endl; - exit(0); -} - void OptionsHandler::showConfiguration(const std::string& option, const std::string& flag) { @@ -369,17 +358,21 @@ void OptionsHandler::showConfiguration(const std::string& option, print_config_cond("poly", Configuration::isBuiltWithPoly()); print_config_cond("editline", Configuration::isBuiltWithEditline()); - exit(0); + std::exit(0); } -static void printTags(const std::vector<std::string>& tags) +void OptionsHandler::showCopyright(const std::string& option, + const std::string& flag) { - std::cout << "available tags:"; - for (const auto& t : tags) - { - std::cout << " " << t << std::endl; - } - std::cout << std::endl; + std::cout << Configuration::copyright() << std::endl; + std::exit(0); +} + +void OptionsHandler::showVersion(const std::string& option, + const std::string& flag) +{ + d_options->base.out << Configuration::about() << std::endl; + std::exit(0); } void OptionsHandler::showDebugTags(const std::string& option, @@ -408,84 +401,169 @@ void OptionsHandler::showTraceTags(const std::string& option, std::exit(0); } -static std::string suggestTags(const std::vector<std::string>& validTags, - std::string inputTag, - const std::vector<std::string>& additionalTags) +// theory/bv/options_handlers.h +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value) { - DidYouMean didYouMean; - didYouMean.addWords(validTags); - didYouMean.addWords(additionalTags); - return didYouMean.getMatchAsString(inputTag); +#ifndef CVC5_USE_ABC + if(value) { + std::stringstream ss; + ss << "option `" << option + << "' requires an abc-enabled build of cvc5; this binary was not built " + "with abc support"; + throw OptionException(ss.str()); + } +#endif /* CVC5_USE_ABC */ } -void OptionsHandler::enableTraceTag(const std::string& option, - const std::string& flag, - const std::string& optarg) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value) { - if(!Configuration::isTracingBuild()) +#ifndef CVC5_USE_ABC + if(!value.empty()) { + std::stringstream ss; + ss << "option `" << option + << "' requires an abc-enabled build of cvc5; this binary was not built " + "with abc support"; + throw OptionException(ss.str()); + } +#endif /* CVC5_USE_ABC */ +} + +void OptionsHandler::checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m) +{ + if (m == SatSolverMode::CRYPTOMINISAT + && !Configuration::isBuiltWithCryptominisat()) { - throw OptionException("trace tags not available in non-tracing builds"); + std::stringstream ss; + ss << "option `" << option + << "' requires a CryptoMiniSat build of cvc5; this binary was not built " + "with CryptoMiniSat support"; + throw OptionException(ss.str()); } - else if (!Configuration::isTraceTag(optarg)) + + if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) { - if (optarg == "help") + std::stringstream ss; + ss << "option `" << option + << "' requires a Kissat build of cvc5; this binary was not built with " + "Kissat support"; + throw OptionException(ss.str()); + } + + if (d_options->bv.bvSolver != options::BVSolver::BITBLAST + && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL + || m == SatSolverMode::KISSAT)) + { + if (d_options->bv.bitblastMode == options::BitblastMode::LAZY + && d_options->bv.bitblastModeWasSetByUser) { - printTags(Configuration::getTraceTags()); - std::exit(0); + throwLazyBBUnsupported(m); } - - throw OptionException( - std::string("trace tag ") + optarg + std::string(" not available.") - + suggestTags(Configuration::getTraceTags(), optarg, {})); + options::bv::setDefaultBitvectorToBool(*d_options, true); } - Trace.on(optarg); } -void OptionsHandler::enableDebugTag(const std::string& option, - const std::string& flag, - const std::string& optarg) +void OptionsHandler::checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m) { - if (!Configuration::isDebugBuild()) + if (m == options::BitblastMode::LAZY) { - throw OptionException("debug tags not available in non-debug builds"); + options::bv::setDefaultBitvectorPropagate(*d_options, true); + options::bv::setDefaultBitvectorEqualitySolver(*d_options, true); + options::bv::setDefaultBitvectorInequalitySolver(*d_options, true); + options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true); + if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT) + { + throwLazyBBUnsupported(d_options->bv.bvSatSolver); + } } - else if (!Configuration::isTracingBuild()) + else if (m == BitblastMode::EAGER) { - throw OptionException("debug tags not available in non-tracing builds"); + options::bv::setDefaultBitvectorToBool(*d_options, true); } +} - if (!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) - { - if (optarg == "help") - { - printTags(Configuration::getDebugTags()); - std::exit(0); +void OptionsHandler::setBitblastAig(const std::string& option, + const std::string& flag, + bool arg) +{ + if(arg) { + if (d_options->bv.bitblastModeWasSetByUser) { + if (d_options->bv.bitblastMode != options::BitblastMode::EAGER) + { + throw OptionException("bitblast-aig must be used with eager bitblaster"); + } + } else { + options::BitblastMode mode = stringToBitblastMode("eager"); + d_options->bv.bitblastMode = mode; } - - throw OptionException(std::string("debug tag ") + optarg - + std::string(" not available.") - + suggestTags(Configuration::getDebugTags(), - optarg, - Configuration::getTraceTags())); } - Debug.on(optarg); - Trace.on(optarg); } -void OptionsHandler::enableOutputTag(const std::string& option, - const std::string& flag, - const std::string& optarg) +void OptionsHandler::setProduceAssertions(const std::string& option, + const std::string& flag, + bool value) { - d_options->base.outputTagHolder.set( - static_cast<size_t>(stringToOutputTag(optarg))); + d_options->smt.produceAssertions = value; + d_options->smt.interactiveMode = value; } + +// expr/options_handlers.h +void OptionsHandler::setDefaultExprDepth(const std::string& option, + const std::string& flag, + int depth) +{ + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + CVC5Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); +} + +void OptionsHandler::setDefaultDagThresh(const std::string& option, + const std::string& flag, + int dag) +{ + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + CVC5Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); +} + +// main/options_handlers.h + Language OptionsHandler::stringToLanguage(const std::string& option, const std::string& flag, const std::string& optarg) { if(optarg == "help") { - d_options->base.languageHelp = true; + *d_options->base.out << R"FOOBAR( +Languages currently supported as arguments to the -L / --lang option: + auto attempt to automatically determine language + smt | smtlib | smt2 | + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard + tptp TPTP format (cnf, fof and tff) + sygus | sygus2 SyGuS version 2.0 + +Languages currently supported as arguments to the --output-lang option: + auto match output language to input language + smt | smtlib | smt2 | + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard + tptp TPTP format + ast internal format (simple syntax trees) +)FOOBAR" << std::endl; + std::exit(1); return Language::LANG_AUTO; } @@ -499,23 +577,6 @@ Language OptionsHandler::stringToLanguage(const std::string& option, Unreachable(); } -void OptionsHandler::applyOutputLanguage(const std::string& option, - const std::string& flag, - Language lang) -{ - d_options->base.out << language::SetLanguage(lang); -} - -void OptionsHandler::languageIsNotAST(const std::string& option, - const std::string& flag, - Language lang) -{ - if (lang == Language::LANG_AST) - { - throw OptionException("Language LANG_AST is not allowed for " + flag); - } -} - void OptionsHandler::setDumpStream(const std::string& option, const std::string& flag, const ManagedOut& mo) @@ -527,75 +588,7 @@ void OptionsHandler::setDumpStream(const std::string& option, "The dumping feature was disabled in this build of cvc5."); #endif /* CVC5_DUMPING */ } -void OptionsHandler::setErrStream(const std::string& option, - const std::string& flag, - const ManagedErr& me) -{ - Debug.setStream(me); - Warning.setStream(me); - CVC5Message.setStream(me); - Notice.setStream(me); - Chat.setStream(me); - Trace.setStream(me); -} -void OptionsHandler::setInStream(const std::string& option, - const std::string& flag, - const ManagedIn& mi) -{ -} -void OptionsHandler::setOutStream(const std::string& option, - const std::string& flag, - const ManagedOut& mo) -{ -} - /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(const std::string& option, - const std::string& flag, - int value) -{ - if(Configuration::isMuzzledBuild()) { - DebugChannel.setStream(&cvc5::null_os); - TraceChannel.setStream(&cvc5::null_os); - NoticeChannel.setStream(&cvc5::null_os); - ChatChannel.setStream(&cvc5::null_os); - MessageChannel.setStream(&cvc5::null_os); - WarningChannel.setStream(&cvc5::null_os); - } else { - if(value < 2) { - ChatChannel.setStream(&cvc5::null_os); - } else { - ChatChannel.setStream(&std::cout); - } - if(value < 1) { - NoticeChannel.setStream(&cvc5::null_os); - } else { - NoticeChannel.setStream(&std::cout); - } - if(value < 0) { - MessageChannel.setStream(&cvc5::null_os); - WarningChannel.setStream(&cvc5::null_os); - } else { - MessageChannel.setStream(&std::cout); - WarningChannel.setStream(&std::cerr); - } - } -} - -void OptionsHandler::increaseVerbosity(const std::string& option, - const std::string& flag) -{ - d_options->base.verbosity += 1; - setVerbosity(option, flag, d_options->base.verbosity); -} - -void OptionsHandler::decreaseVerbosity(const std::string& option, - const std::string& flag) -{ - d_options->base.verbosity -= 1; - setVerbosity(option, flag, d_options->base.verbosity); -} - void OptionsHandler::setDumpMode(const std::string& option, const std::string& flag, const std::string& optarg) @@ -603,18 +596,5 @@ void OptionsHandler::setDumpMode(const std::string& option, Dump.setDumpFromString(optarg); } -void OptionsHandler::setPrintSuccess(const std::string& option, - const std::string& flag, - bool value) -{ - Debug.getStream() << Command::printsuccess(value); - Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); - Chat.getStream() << Command::printsuccess(value); - CVC5Message.getStream() << Command::printsuccess(value); - Warning.getStream() << Command::printsuccess(value); - *d_options->base.out << Command::printsuccess(value); -} - } // namespace options } // namespace cvc5 |