From b261b0a6031dee3210e569f75f8abdac35b7091c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 1 Oct 2021 13:40:05 -0700 Subject: [PATCH] Clean options handlers (#7201) Some cleanup on the option handlers, starting with handlers for base and main options. --- src/main/driver_unified.cpp | 10 - src/main/options.h | 3 - src/main/options_template.cpp | 22 - src/options/base_options.toml | 98 ++--- src/options/main_options.toml | 6 +- src/options/options_handler.cpp | 626 +++++++++++++-------------- src/options/options_handler.h | 120 ++--- src/options/quantifiers_options.toml | 4 - 8 files changed, 413 insertions(+), 476 deletions(-) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index ee610757b..d6a6f9331 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -100,16 +100,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) printUsage(dopts, true); exit(1); } - else if (solver->getOptionInfo("language-help").boolValue()) - { - main::printLanguageHelp(dopts.out()); - exit(1); - } - else if (solver->getOptionInfo("version").boolValue()) - { - dopts.out() << Configuration::about().c_str() << flush; - exit(0); - } segvSpin = solver->getOptionInfo("segv-spin").boolValue(); diff --git a/src/main/options.h b/src/main/options.h index a2c26273b..832abcf9d 100644 --- a/src/main/options.h +++ b/src/main/options.h @@ -39,9 +39,6 @@ void printUsage(const std::string& msg, std::ostream& os); */ void printShortUsage(const std::string& msg, std::ostream& os); -/** Print help for the --lang command line option */ -void printLanguageHelp(std::ostream& os); - /** * Initialize the Options object options based on the given * command-line arguments given in argc and argv. The return value diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp index b9a432183..138821c71 100644 --- a/src/main/options_template.cpp +++ b/src/main/options_template.cpp @@ -61,23 +61,6 @@ static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ sense of the option.\n\ "; - -static const std::string languageDescription = - "\ -Languages currently supported as arguments to the -L / --lang option:\n\ - auto attempt to automatically determine language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format (cnf, fof and tff)\n\ - sygus | sygus2 SyGuS version 2.0\n\ -\n\ -Languages currently supported as arguments to the --output-lang option:\n\ - auto match output language to input language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format\n\ - ast internal format (simple syntax trees)\n\ -"; // clang-format on void printUsage(const std::string& msg, std::ostream& os) @@ -97,11 +80,6 @@ void printShortUsage(const std::string& msg, std::ostream& os) << std::endl; } -void printLanguageHelp(std::ostream& os) -{ - os << languageDescription << std::flush; -} - /** * This is a table of long options. By policy, each short option * should have an equivalent long option (but the reverse isn't the diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 89032ba50..316810ae2 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -1,12 +1,20 @@ id = "BASE" name = "Base" +[[option]] + name = "err" + category = "undocumented" + long = "err=erroutput" + type = "ManagedErr" + alias = ["diagnostic-output-channel"] + predicates = ["setErrStream"] + includes = ["", "options/managed_streams.h"] + [[option]] name = "in" category = "undocumented" long = "in=input" type = "ManagedIn" - predicates = ["setInStream"] includes = ["", "options/managed_streams.h"] [[option]] @@ -15,16 +23,6 @@ name = "Base" long = "out=output" type = "ManagedOut" alias = ["regular-output-channel"] - predicates = ["setOutStream"] - includes = ["", "options/managed_streams.h"] - -[[option]] - name = "err" - category = "undocumented" - long = "err=erroutput" - type = "ManagedErr" - alias = ["diagnostic-output-channel"] - predicates = ["setErrStream"] includes = ["", "options/managed_streams.h"] [[option]] @@ -52,12 +50,6 @@ name = "Base" includes = ["options/language.h"] help = "force output language (default is \"auto\"; see --output-lang help)" -[[option]] - name = "languageHelp" - long = "language-help" - category = "undocumented" - type = "bool" - [[option]] name = "verbosity" long = "verbosity=N" @@ -105,7 +97,7 @@ name = "Base" long = "stats-all" category = "expert" type = "bool" - predicates = ["setStats"] + predicates = ["setStatsDetail"] help = "print unchanged (defaulted) statistics as well" [[option]] @@ -113,7 +105,7 @@ name = "Base" long = "stats-expert" category = "expert" type = "bool" - predicates = ["setStats"] + predicates = ["setStatsDetail"] help = "print expert (non-public) statistics as well" [[option]] @@ -121,7 +113,7 @@ name = "Base" long = "stats-every-query" category = "regular" type = "bool" - predicates = ["setStats"] + predicates = ["setStatsDetail"] default = "false" help = "in incremental mode, print stats after every satisfiability or validity query" @@ -155,6 +147,38 @@ name = "Base" handler = "enableDebugTag" help = "debug something (e.g. -d arith), can repeat" +[[option]] + name = "outputTag" + short = "o" + long = "output=TAG" + type = "OutputTag" + default = "NONE" + handler = "enableOutputTag" + category = "regular" + help = "Enable output tag." + help_mode = "Output tags." +[[option.mode.NONE]] + name = "none" +[[option.mode.INST]] + name = "inst" + help = "print instantiations during solving" +[[option.mode.SYGUS]] + name = "sygus" + help = "print enumerated terms and candidates generated by the sygus solver" +[[option.mode.TRIGGER]] + name = "trigger" + help = "print selected triggers for quantified formulas" +[[option.mode.RAW_BENCHMARK]] + name = "raw-benchmark" + help = "print the benchmark back on the output verbatim as it is processed" + +# Stores then enabled output tags. +[[option]] + name = "outputTagHolder" + category = "undocumented" + includes = [""] + type = "std::bitset" + [[option]] name = "printSuccess" category = "regular" @@ -210,36 +234,4 @@ name = "Base" [[option]] name = "resourceWeightHolder" category = "undocumented" - type = "std::vector" - -[[option]] - name = "outputTag" - short = "o" - long = "output=TAG" - type = "OutputTag" - default = "NONE" - handler = "enableOutputTag" - category = "regular" - help = "Enable output tag." - help_mode = "Output tags." -[[option.mode.NONE]] - name = "none" -[[option.mode.INST]] - name = "inst" - help = "print instantiations during solving" -[[option.mode.SYGUS]] - name = "sygus" - help = "print enumerated terms and candidates generated by the sygus solver" -[[option.mode.TRIGGER]] - name = "trigger" - help = "print selected triggers for quantified formulas" -[[option.mode.RAW_BENCHMARK]] - name = "raw-benchmark" - help = "print the benchmark back on the output verbatim as it is processed" - -# Stores then enabled output tags. -[[option]] - name = "outputTagHolder" - category = "undocumented" - includes = [""] - type = "std::bitset" + type = "std::vector" \ No newline at end of file diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 55bea41f0..3d78a6ebb 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -2,12 +2,10 @@ id = "DRIVER" name = "Driver" [[option]] - name = "version" category = "common" short = "V" long = "version" - type = "bool" - alternate = false + type = "void" help = "identify this cvc5 binary" [[option]] @@ -30,7 +28,7 @@ name = "Driver" category = "common" long = "copyright" type = "void" - handler = "copyright" + handler = "showCopyright" help = "show cvc5 copyright information" [[option]] 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 +#include #include #include @@ -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& 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& validTags, + std::string inputTag, + const std::vector& 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()) + { + throw OptionException("debug tags not available in non-debug builds"); + } + else if (!Configuration::isTracingBuild()) { - if (opt == options::base::statistics__name) + 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(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& 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& validTags, - std::string inputTag, - const std::vector& 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(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 diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 0d625c5da..5ced2ed48 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -75,10 +75,70 @@ public: } } - // theory/quantifiers/options_handlers.h - void checkInstWhenMode(const std::string& option, + /******************************* base options *******************************/ + /** Apply the error output stream to the different output channels */ + void setErrStream(const std::string& option, + const std::string& flag, + const ManagedErr& me); + + /** Convert option value to Language enum */ + Language stringToLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + /** Check that lang is not LANG_AST (not allowed as input language) */ + void languageIsNotAST(const std::string& option, + const std::string& flag, + Language lang); + /** Apply the output language to the default output stream */ + void applyOutputLanguage(const std::string& option, + const std::string& flag, + Language lang); + /** Apply verbosity to the different output channels */ + void setVerbosity(const std::string& option, + const std::string& flag, + int value); + /** Decrease verbosity and call setVerbosity */ + void decreaseVerbosity(const std::string& option, const std::string& flag); + /** Increase verbosity and call setVerbosity */ + void increaseVerbosity(const std::string& option, const std::string& flag); + /** If statistics are disabled, disable statistics sub-options */ + void setStats(const std::string& option, const std::string& flag, bool value); + /** If statistics sub-option is disabled, enable statistics */ + void setStatsDetail(const std::string& option, + const std::string& flag, + bool value); + /** Enable a particular trace tag */ + void enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + /** Enable a particular debug tag */ + void enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + /** Enable a particular output tag */ + void enableOutputTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + /** Apply print success flag to the different output channels */ + void setPrintSuccess(const std::string& option, + const std::string& flag, + bool value); + /** Pass the resource weight specification to the resource manager */ + void setResourceWeight(const std::string& option, const std::string& flag, - InstWhenMode mode); + const std::string& optarg); + + /******************************* main options *******************************/ + /** Show the solver build configuration and exit */ + void showConfiguration(const std::string& option, const std::string& flag); + /** Show copyright information and exit */ + void showCopyright(const std::string& option, const std::string& flag); + /** Show version information and exit */ + void showVersion(const std::string& option, const std::string& flag); + /** Show all debug tags and exit */ + void showDebugTags(const std::string& option, const std::string& flag); + /** Show all trace tags and exit */ + void showTraceTags(const std::string& option, const std::string& flag); // theory/bv/options_handlers.h void abcEnabledBuild(const std::string& option, @@ -107,15 +167,6 @@ public: const std::string& flag, bool value); - void setStats(const std::string& option, const std::string& flag, bool value); - - uint64_t limitHandler(const std::string& option, - const std::string& flag, - const std::string& optarg); - void setResourceWeight(const std::string& option, - const std::string& flag, - const std::string& optarg); - /* expr/options_handlers.h */ void setDefaultExprDepth(const std::string& option, const std::string& flag, @@ -124,60 +175,15 @@ public: const std::string& flag, int dag); - /* main/options_handlers.h */ - void copyright(const std::string& option, const std::string& flag); - void showConfiguration(const std::string& option, const std::string& flag); - void showDebugTags(const std::string& option, const std::string& flag); - void showTraceTags(const std::string& option, const std::string& flag); - void threadN(const std::string& option, const std::string& flag); /* options/base_options_handlers.h */ void setDumpStream(const std::string& option, const std::string& flag, const ManagedOut& mo); - void setErrStream(const std::string& option, - const std::string& flag, - const ManagedErr& me); - void setInStream(const std::string& option, - const std::string& flag, - const ManagedIn& mi); - void setOutStream(const std::string& option, - const std::string& flag, - const ManagedOut& mo); - void setVerbosity(const std::string& option, - const std::string& flag, - int value); - void increaseVerbosity(const std::string& option, const std::string& flag); - void decreaseVerbosity(const std::string& option, const std::string& flag); - /** Convert optarg to Language enum */ - Language stringToLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg); - /** Apply the output language to the default output stream */ - void applyOutputLanguage(const std::string& option, - const std::string& flag, - Language lang); - /** Check that lang is not LANG_AST (which is not allowed as input language). */ - void languageIsNotAST(const std::string& option, - const std::string& flag, - Language lang); - void enableTraceTag(const std::string& option, - const std::string& flag, - const std::string& optarg); - void enableDebugTag(const std::string& option, - const std::string& flag, - const std::string& optarg); - - void enableOutputTag(const std::string& option, - const std::string& flag, - const std::string& optarg); void setDumpMode(const std::string& option, const std::string& flag, const std::string& optarg); - void setPrintSuccess(const std::string& option, - const std::string& flag, - bool value); private: diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 106161305..f3c89fd74 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -407,12 +407,8 @@ name = "Quantifiers" long = "inst-when=MODE" type = "InstWhenMode" default = "FULL_LAST_CALL" - predicates = ["checkInstWhenMode"] help = "when to apply instantiation" help_mode = "Instantiation modes." -[[option.mode.PRE_FULL]] - name = "pre-full" - help = "Run instantiation round before full effort (possibly at standard effort)." [[option.mode.FULL]] name = "full" help = "Run instantiation round at full effort, before theory combination." -- 2.30.2