From 13f5ecf0f7d683c67ab9b6e0cd66777af1b0531b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 4 Oct 2021 17:16:18 -0700 Subject: [PATCH] Finish refactoring on option handlers (#7295) This PR finishes refactoring on the option handlers. --- src/options/options_handler.cpp | 374 ++++++++---------- src/options/options_handler.h | 62 ++- src/options/smt_options.toml | 9 - src/smt/dump.cpp | 6 +- .../regress1/fmf/forall_unit_data.smt2 | 2 +- 5 files changed, 208 insertions(+), 245 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 27ab63ae7..0dfeb3b2c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -47,27 +47,6 @@ namespace options { // helper functions namespace { -void throwLazyBBUnsupported(options::SatSolverMode m) -{ - std::string sat_solver; - if (m == options::SatSolverMode::CADICAL) - { - sat_solver = "CaDiCaL"; - } - else if (m == options::SatSolverMode::KISSAT) - { - sat_solver = "Kissat"; - } - else - { - Assert(m == options::SatSolverMode::CRYPTOMINISAT); - sat_solver = "CryptoMiniSat"; - } - std::string indent(25, ' '); - throw OptionException(sat_solver + " does not support lazy bit-blasting.\n" - + indent + "Try --bv-sat-solver=minisat"); -} - static void printTags(const std::vector& tags) { std::cout << "available tags:"; @@ -104,6 +83,44 @@ void OptionsHandler::setErrStream(const std::string& option, Trace.setStream(me); } +Language OptionsHandler::stringToLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ + if (optarg == "help") + { + *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; + } + + try + { + return language::toLanguage(optarg); + } + catch (OptionException& oe) + { + throw OptionException("Error in " + option + ": " + oe.getMessage() + + "\nTry --lang help"); + } + + Unreachable(); +} + void OptionsHandler::languageIsNotAST(const std::string& option, const std::string& flag, Language lang) @@ -292,116 +309,6 @@ void OptionsHandler::setResourceWeight(const std::string& option, d_options->base.resourceWeightHolder.emplace_back(optarg); } -static void print_config (const char * str, std::string config) { - std::string s(str); - unsigned sz = 14; - if (s.size() < sz) s.resize(sz, ' '); - std::cout << s << ": " << config << std::endl; -} - -static void print_config_cond (const char * str, bool cond = false) { - print_config(str, cond ? "yes" : "no"); -} - -void OptionsHandler::showConfiguration(const std::string& option, - const std::string& flag) -{ - std::cout << Configuration::about() << std::endl; - - print_config ("version", Configuration::getVersionString()); - - if(Configuration::isGitBuild()) { - const char* branchName = Configuration::getGitBranchName(); - if(*branchName == '\0') { branchName = "-"; } - std::stringstream ss; - ss << "git [" - << branchName << " " - << std::string(Configuration::getGitCommit()).substr(0, 8) - << (Configuration::hasGitModifications() ? " (with modifications)" : "") - << "]"; - print_config("scm", ss.str()); - } else { - print_config_cond("scm", false); - } - - std::cout << std::endl; - - std::stringstream ss; - ss << Configuration::getVersionMajor() << "." - << Configuration::getVersionMinor() << "." - << Configuration::getVersionRelease(); - print_config("library", ss.str()); - - std::cout << std::endl; - - print_config_cond("debug code", Configuration::isDebugBuild()); - print_config_cond("statistics", Configuration::isStatisticsBuild()); - print_config_cond("tracing", Configuration::isTracingBuild()); - print_config_cond("dumping", Configuration::isDumpingBuild()); - print_config_cond("muzzled", Configuration::isMuzzledBuild()); - print_config_cond("assertions", Configuration::isAssertionBuild()); - print_config_cond("coverage", Configuration::isCoverageBuild()); - print_config_cond("profiling", Configuration::isProfilingBuild()); - print_config_cond("asan", Configuration::isAsanBuild()); - print_config_cond("ubsan", Configuration::isUbsanBuild()); - print_config_cond("tsan", Configuration::isTsanBuild()); - print_config_cond("competition", Configuration::isCompetitionBuild()); - - std::cout << std::endl; - - print_config_cond("abc", Configuration::isBuiltWithAbc()); - print_config_cond("cln", Configuration::isBuiltWithCln()); - print_config_cond("glpk", Configuration::isBuiltWithGlpk()); - print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); - print_config_cond("gmp", Configuration::isBuiltWithGmp()); - print_config_cond("kissat", Configuration::isBuiltWithKissat()); - print_config_cond("poly", Configuration::isBuiltWithPoly()); - print_config_cond("editline", Configuration::isBuiltWithEditline()); - - std::exit(0); -} - -void OptionsHandler::showCopyright(const std::string& option, - const std::string& flag) -{ - 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, - const std::string& flag) -{ - if (!Configuration::isDebugBuild()) - { - throw OptionException("debug tags not available in non-debug builds"); - } - else if (!Configuration::isTracingBuild()) - { - throw OptionException("debug tags not available in non-tracing builds"); - } - printTags(Configuration::getDebugTags()); - std::exit(0); -} - -void OptionsHandler::showTraceTags(const std::string& option, - const std::string& flag) -{ - if (!Configuration::isTracingBuild()) - { - throw OptionException("trace tags not available in non-tracing build"); - } - printTags(Configuration::getTraceTags()); - std::exit(0); -} - -// theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(const std::string& option, const std::string& flag, bool value) @@ -462,29 +369,24 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, if (d_options->bv.bitblastMode == options::BitblastMode::LAZY && d_options->bv.bitblastModeWasSetByUser) { - throwLazyBBUnsupported(m); - } - options::bv::setDefaultBitvectorToBool(*d_options, true); - } -} - -void OptionsHandler::checkBitblastMode(const std::string& option, - const std::string& flag, - BitblastMode m) -{ - 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); + std::string sat_solver; + if (m == options::SatSolverMode::CADICAL) + { + sat_solver = "CaDiCaL"; + } + else if (m == options::SatSolverMode::KISSAT) + { + sat_solver = "Kissat"; + } + else + { + Assert(m == options::SatSolverMode::CRYPTOMINISAT); + sat_solver = "CryptoMiniSat"; + } + throw OptionException(sat_solver + + " does not support lazy bit-blasting.\n" + + "Try --bv-sat-solver=minisat"); } - } - else if (m == BitblastMode::EAGER) - { options::bv::setDefaultBitvectorToBool(*d_options, true); } } @@ -500,22 +402,11 @@ void OptionsHandler::setBitblastAig(const std::string& option, throw OptionException("bitblast-aig must be used with eager bitblaster"); } } else { - options::BitblastMode mode = stringToBitblastMode("eager"); - d_options->bv.bitblastMode = mode; + d_options->bv.bitblastMode = options::BitblastMode::EAGER; } } } -void OptionsHandler::setProduceAssertions(const std::string& option, - const std::string& flag, - bool value) -{ - 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) @@ -541,40 +432,132 @@ void OptionsHandler::setDefaultDagThresh(const std::string& option, Dump.getStream() << expr::ExprDag(dag); } -// main/options_handlers.h +static void print_config(const char* str, std::string config) +{ + std::string s(str); + unsigned sz = 14; + if (s.size() < sz) s.resize(sz, ' '); + std::cout << s << ": " << config << std::endl; +} -Language OptionsHandler::stringToLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg) +static void print_config_cond(const char* str, bool cond = false) { - if(optarg == "help") { - *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 + print_config(str, cond ? "yes" : "no"); +} -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; +void OptionsHandler::showConfiguration(const std::string& option, + const std::string& flag) +{ + std::cout << Configuration::about() << std::endl; + + print_config("version", Configuration::getVersionString()); + + if (Configuration::isGitBuild()) + { + const char* branchName = Configuration::getGitBranchName(); + if (*branchName == '\0') + { + branchName = "-"; + } + std::stringstream ss; + ss << "git [" << branchName << " " + << std::string(Configuration::getGitCommit()).substr(0, 8) + << (Configuration::hasGitModifications() ? " (with modifications)" : "") + << "]"; + print_config("scm", ss.str()); + } + else + { + print_config_cond("scm", false); } - try { - return language::toLanguage(optarg); - } catch(OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() - + "\nTry --lang help"); + std::cout << std::endl; + + std::stringstream ss; + ss << Configuration::getVersionMajor() << "." + << Configuration::getVersionMinor() << "." + << Configuration::getVersionRelease(); + print_config("library", ss.str()); + + std::cout << std::endl; + + print_config_cond("debug code", Configuration::isDebugBuild()); + print_config_cond("statistics", Configuration::isStatisticsBuild()); + print_config_cond("tracing", Configuration::isTracingBuild()); + print_config_cond("dumping", Configuration::isDumpingBuild()); + print_config_cond("muzzled", Configuration::isMuzzledBuild()); + print_config_cond("assertions", Configuration::isAssertionBuild()); + print_config_cond("coverage", Configuration::isCoverageBuild()); + print_config_cond("profiling", Configuration::isProfilingBuild()); + print_config_cond("asan", Configuration::isAsanBuild()); + print_config_cond("ubsan", Configuration::isUbsanBuild()); + print_config_cond("tsan", Configuration::isTsanBuild()); + print_config_cond("competition", Configuration::isCompetitionBuild()); + + std::cout << std::endl; + + print_config_cond("abc", Configuration::isBuiltWithAbc()); + print_config_cond("cln", Configuration::isBuiltWithCln()); + print_config_cond("glpk", Configuration::isBuiltWithGlpk()); + print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); + print_config_cond("gmp", Configuration::isBuiltWithGmp()); + print_config_cond("kissat", Configuration::isBuiltWithKissat()); + print_config_cond("poly", Configuration::isBuiltWithPoly()); + print_config_cond("editline", Configuration::isBuiltWithEditline()); + + std::exit(0); +} + +void OptionsHandler::showCopyright(const std::string& option, + const std::string& flag) +{ + 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, + const std::string& flag) +{ + if (!Configuration::isDebugBuild()) + { + throw OptionException("debug tags not available in non-debug builds"); + } + else if (!Configuration::isTracingBuild()) + { + throw OptionException("debug tags not available in non-tracing builds"); } + printTags(Configuration::getDebugTags()); + std::exit(0); +} - Unreachable(); +void OptionsHandler::showTraceTags(const std::string& option, + const std::string& flag) +{ + if (!Configuration::isTracingBuild()) + { + throw OptionException("trace tags not available in non-tracing build"); + } + printTags(Configuration::getTraceTags()); + std::exit(0); +} + +void OptionsHandler::setDumpMode(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ +#ifdef CVC5_DUMPING + Dump.setDumpFromString(optarg); +#else /* CVC5_DUMPING */ + throw OptionException( + "The dumping feature was disabled in this build of cvc5."); +#endif /* CVC5_DUMPING */ } void OptionsHandler::setDumpStream(const std::string& option, @@ -588,13 +571,6 @@ void OptionsHandler::setDumpStream(const std::string& option, "The dumping feature was disabled in this build of cvc5."); #endif /* CVC5_DUMPING */ } -/* options/base_options_handlers.h */ -void OptionsHandler::setDumpMode(const std::string& option, - const std::string& flag, - const std::string& optarg) -{ - Dump.setDumpFromString(optarg); -} } // namespace options } // namespace cvc5 diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 5ced2ed48..c3cd8c358 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -40,8 +40,9 @@ namespace options { * * Most functions can throw an OptionException on failure. */ -class OptionsHandler { -public: +class OptionsHandler +{ + public: OptionsHandler(Options* options); template @@ -128,65 +129,58 @@ public: const std::string& flag, 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); + /******************************* bv options *******************************/ - // theory/bv/options_handlers.h + /** Check that abc is enabled */ void abcEnabledBuild(const std::string& option, const std::string& flag, bool value); + /** Check that abc is enabled */ void abcEnabledBuild(const std::string& option, const std::string& flag, const std::string& value); - + /** Check that the sat solver mode is compatible with other bv options */ void checkBvSatSolver(const std::string& option, const std::string& flag, SatSolverMode m); - void checkBitblastMode(const std::string& option, - const std::string& flag, - BitblastMode m); - + /** Check that we use eager bitblasting for aig */ void setBitblastAig(const std::string& option, const std::string& flag, bool arg); - /** - * Throws a ModalException if this option is being set after final - * initialization. - */ - void setProduceAssertions(const std::string& option, - const std::string& flag, - bool value); - - /* expr/options_handlers.h */ + /******************************* expr options *******************************/ + /** Set ExprSetDepth on all output streams */ void setDefaultExprDepth(const std::string& option, const std::string& flag, int depth); + /** Set ExprDag on all output streams */ void setDefaultDagThresh(const std::string& option, const std::string& flag, int dag); + /******************************* 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); - /* options/base_options_handlers.h */ - void setDumpStream(const std::string& option, - const std::string& flag, - const ManagedOut& mo); - + /******************************* smt options *******************************/ + /** Set a mode on the dumping output stream. */ void setDumpMode(const std::string& option, const std::string& flag, const std::string& optarg); + /** Set the dumping output stream. */ + void setDumpStream(const std::string& option, + const std::string& flag, + const ManagedOut& mo); private: - /** Pointer to the containing Options object.*/ Options* d_options; }; /* class OptionHandler */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 95cc79a0d..19862cab2 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -254,20 +254,11 @@ name = "SMT Layer" default = "false" help = "support the get-assignment command" -[[option]] - name = "interactiveMode" - long = "interactive-mode" - category = "undocumented" - type = "bool" - predicates = ["setProduceAssertions"] - help = "deprecated name for produce-assertions" - [[option]] name = "produceAssertions" category = "common" long = "produce-assertions" type = "bool" - predicates = ["setProduceAssertions"] help = "keep an assertions list (enables get-assertions command)" [[option]] diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index d74668433..ab6144e02 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -57,7 +57,8 @@ CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc) DumpC DumpChannel; -std::ostream& DumpC::setStream(std::ostream* os) { +std::ostream& DumpC::setStream(std::ostream* os) +{ ::cvc5::DumpOutChannel.setStream(os); return *os; } @@ -67,7 +68,8 @@ std::ostream* DumpC::getStreamPointer() return ::cvc5::DumpOutChannel.getStreamPointer(); } -void DumpC::setDumpFromString(const std::string& optarg) { +void DumpC::setDumpFromString(const std::string& optarg) +{ if (Configuration::isDumpingBuild()) { // Make a copy of optarg for strtok_r to use. diff --git a/test/regress/regress1/fmf/forall_unit_data.smt2 b/test/regress/regress1/fmf/forall_unit_data.smt2 index 411c03c8a..b942f1165 100644 --- a/test/regress/regress1/fmf/forall_unit_data.smt2 +++ b/test/regress/regress1/fmf/forall_unit_data.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat (set-option :produce-models true) -(set-option :interactive-mode true) +(set-option :produce-assertions true) (set-logic ALL) (declare-sort a 0) (declare-datatypes ((w 0)) (((Wrap (unw a))))) -- 2.30.2