From c6c2cb9d3cc911526266e517460b3e8ae2dab9c0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 22 Oct 2021 15:32:33 -0700 Subject: [PATCH] Remove options::X__name (#7414) This PR removes the static strings options::module::X__name that hold the primary long option name. We used them to figure out which option an handler function was called on for certain handler functions. This was always a weird way, and the past refactorings have eliminated all these cases. This also removes the need to the two arguments option and flag to all option handlers. --- src/options/mkoptions.py | 31 ++----- src/options/module_template.h | 7 -- src/options/options_handler.cpp | 107 ++++++++---------------- src/options/options_handler.h | 102 +++++++--------------- src/options/options_public_template.cpp | 29 ++----- src/smt/set_defaults.cpp | 10 +-- 6 files changed, 85 insertions(+), 201 deletions(-) diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 57f8b64e6..badfd59f0 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -295,15 +295,12 @@ def _set_handlers(option): optname = option.long_name if option.long else "" if option.handler: if option.type == 'void': - return 'opts.handler().{}("{}", name)'.format( - option.handler, optname) + return 'opts.handler().{}(name)'.format(option.handler) else: - return 'opts.handler().{}("{}", name, optionarg)'.format( - option.handler, optname) + return 'opts.handler().{}(name, optionarg)'.format(option.handler) elif option.mode: return 'stringTo{}(optionarg)'.format(option.type) - return 'handlers::handleOption<{}>("{}", name, optionarg)'.format( - option.type, optname) + return 'handlers::handleOption<{}>(name, optionarg)'.format(option.type) def _set_predicates(option): @@ -315,14 +312,14 @@ def _set_predicates(option): res = [] if option.minimum: res.append( - 'opts.handler().checkMinimum("{}", name, value, static_cast<{}>({}));' - .format(optname, option.type, option.minimum)) + 'opts.handler().checkMinimum(name, value, static_cast<{}>({}));' + .format(option.type, option.minimum)) if option.maximum: res.append( - 'opts.handler().checkMaximum("{}", name, value, static_cast<{}>({}));' - .format(optname, option.type, option.maximum)) + 'opts.handler().checkMaximum(name, value, static_cast<{}>({}));' + .format(option.type, option.maximum)) res += [ - 'opts.handler().{}("{}", name, value);'.format(x, optname) + 'opts.handler().{}(name, value);'.format(x) for x in option.predicates ] return res @@ -361,7 +358,7 @@ def generate_set_impl(modules): name=option.name, handler=_set_handlers(option))) elif option.handler: - h = ' opts.handler().{handler}("{smtname}", name' + h = ' opts.handler().{handler}(name' if option.type not in ['bool', 'void']: h += ', optionarg' h += ');' @@ -471,15 +468,6 @@ def generate_module_wrapper_functions(module): return '\n'.join(res) -def generate_module_option_names(module): - relevant = [ - o for o in module.options - if not (o.name is None or o.long_name is None) - ] - return concat_format( - 'static constexpr const char* {name}__name = "{long_name}";', relevant) - - ################################################################################ # for options/.cpp @@ -842,7 +830,6 @@ def codegen_module(module, dst_dir, tpls): 'modes_decl': generate_module_mode_decl(module), 'holder_decl': generate_module_holder_decl(module), 'wrapper_functions': generate_module_wrapper_functions(module), - 'option_names': generate_module_option_names(module), # module source 'header': module.header, 'modes_impl': generate_module_mode_impl(module), diff --git a/src/options/module_template.h b/src/options/module_template.h index d9b591f11..c613c1cba 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -52,13 +52,6 @@ ${holder_decl}$ ${wrapper_functions}$ // clang-format on -namespace ${id}$ -{ -// clang-format off -${option_names}$ -// clang-format on -} - } // namespace cvc5::options #endif /* CVC5__OPTIONS__${id_cap}$_H */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index ec6c831e4..fe0e1d961 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -71,9 +71,7 @@ std::string suggestTags(const std::vector& validTags, OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -void OptionsHandler::setErrStream(const std::string& option, - const std::string& flag, - const ManagedErr& me) +void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me) { Debug.setStream(me); Warning.setStream(me); @@ -83,8 +81,7 @@ void OptionsHandler::setErrStream(const std::string& option, Trace.setStream(me); } -Language OptionsHandler::stringToLanguage(const std::string& option, - const std::string& flag, +Language OptionsHandler::stringToLanguage(const std::string& flag, const std::string& optarg) { if (optarg == "help") @@ -114,16 +111,14 @@ Languages currently supported as arguments to the --output-lang option: } catch (OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() + throw OptionException("Error in " + flag + ": " + oe.getMessage() + "\nTry --lang help"); } Unreachable(); } -void OptionsHandler::languageIsNotAST(const std::string& option, - const std::string& flag, - Language lang) +void OptionsHandler::languageIsNotAST(const std::string& flag, Language lang) { if (lang == Language::LANG_AST) { @@ -131,16 +126,12 @@ void OptionsHandler::languageIsNotAST(const std::string& option, } } -void OptionsHandler::applyOutputLanguage(const std::string& option, - const std::string& flag, - Language lang) +void OptionsHandler::applyOutputLanguage(const std::string& flag, Language lang) { d_options->base.out << language::SetLanguage(lang); } -void OptionsHandler::setVerbosity(const std::string& option, - const std::string& flag, - int value) +void OptionsHandler::setVerbosity(const std::string& flag, int value) { if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); @@ -170,23 +161,19 @@ void OptionsHandler::setVerbosity(const std::string& option, } } -void OptionsHandler::decreaseVerbosity(const std::string& option, - const std::string& flag) +void OptionsHandler::decreaseVerbosity(const std::string& flag) { d_options->base.verbosity -= 1; - setVerbosity(option, flag, d_options->base.verbosity); + setVerbosity(flag, d_options->base.verbosity); } -void OptionsHandler::increaseVerbosity(const std::string& option, - const std::string& flag) +void OptionsHandler::increaseVerbosity(const std::string& flag) { d_options->base.verbosity += 1; - setVerbosity(option, flag, d_options->base.verbosity); + setVerbosity(flag, d_options->base.verbosity); } -void OptionsHandler::setStats(const std::string& option, - const std::string& flag, - bool value) +void OptionsHandler::setStats(const std::string& flag, bool value) { #ifndef CVC5_STATISTICS_ON if (value) @@ -206,9 +193,7 @@ void OptionsHandler::setStats(const std::string& option, } } -void OptionsHandler::setStatsDetail(const std::string& option, - const std::string& flag, - bool value) +void OptionsHandler::setStatsDetail(const std::string& flag, bool value) { #ifndef CVC5_STATISTICS_ON if (value) @@ -226,8 +211,7 @@ void OptionsHandler::setStatsDetail(const std::string& option, } } -void OptionsHandler::enableTraceTag(const std::string& option, - const std::string& flag, +void OptionsHandler::enableTraceTag(const std::string& flag, const std::string& optarg) { if(!Configuration::isTracingBuild()) @@ -249,8 +233,7 @@ void OptionsHandler::enableTraceTag(const std::string& option, Trace.on(optarg); } -void OptionsHandler::enableDebugTag(const std::string& option, - const std::string& flag, +void OptionsHandler::enableDebugTag(const std::string& flag, const std::string& optarg) { if (!Configuration::isDebugBuild()) @@ -281,17 +264,14 @@ void OptionsHandler::enableDebugTag(const std::string& option, Trace.on(optarg); } -void OptionsHandler::enableOutputTag(const std::string& option, - const std::string& flag, +void OptionsHandler::enableOutputTag(const std::string& flag, const std::string& optarg) { d_options->base.outputTagHolder.set( static_cast(stringToOutputTag(optarg))); } -void OptionsHandler::setPrintSuccess(const std::string& option, - const std::string& flag, - bool value) +void OptionsHandler::setPrintSuccess(const std::string& flag, bool value) { Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); @@ -302,21 +282,18 @@ void OptionsHandler::setPrintSuccess(const std::string& option, *d_options->base.out << Command::printsuccess(value); } -void OptionsHandler::setResourceWeight(const std::string& option, - const std::string& flag, +void OptionsHandler::setResourceWeight(const std::string& flag, const std::string& optarg) { d_options->base.resourceWeightHolder.emplace_back(optarg); } -void OptionsHandler::abcEnabledBuild(const std::string& option, - const std::string& flag, - bool value) +void OptionsHandler::abcEnabledBuild(const std::string& flag, bool value) { #ifndef CVC5_USE_ABC if(value) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires an abc-enabled build of cvc5; this binary was not built " "with abc support"; throw OptionException(ss.str()); @@ -324,14 +301,13 @@ void OptionsHandler::abcEnabledBuild(const std::string& option, #endif /* CVC5_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(const std::string& option, - const std::string& flag, +void OptionsHandler::abcEnabledBuild(const std::string& flag, const std::string& value) { #ifndef CVC5_USE_ABC if(!value.empty()) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires an abc-enabled build of cvc5; this binary was not built " "with abc support"; throw OptionException(ss.str()); @@ -339,15 +315,13 @@ void OptionsHandler::abcEnabledBuild(const std::string& option, #endif /* CVC5_USE_ABC */ } -void OptionsHandler::checkBvSatSolver(const std::string& option, - const std::string& flag, - SatSolverMode m) +void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m) { if (m == SatSolverMode::CRYPTOMINISAT && !Configuration::isBuiltWithCryptominisat()) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a CryptoMiniSat build of cvc5; this binary was not built " "with CryptoMiniSat support"; throw OptionException(ss.str()); @@ -356,7 +330,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a Kissat build of cvc5; this binary was not built with " "Kissat support"; throw OptionException(ss.str()); @@ -394,9 +368,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, } } -void OptionsHandler::setBitblastAig(const std::string& option, - const std::string& flag, - bool arg) +void OptionsHandler::setBitblastAig(const std::string& flag, bool arg) { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { @@ -410,9 +382,7 @@ void OptionsHandler::setBitblastAig(const std::string& option, } } -void OptionsHandler::setDefaultExprDepth(const std::string& option, - const std::string& flag, - int depth) +void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth) { Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); @@ -422,9 +392,7 @@ void OptionsHandler::setDefaultExprDepth(const std::string& option, Warning.getStream() << expr::ExprSetDepth(depth); } -void OptionsHandler::setDefaultDagThresh(const std::string& option, - const std::string& flag, - int dag) +void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag) { Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); @@ -448,8 +416,7 @@ 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) +void OptionsHandler::showConfiguration(const std::string& flag) { std::cout << Configuration::about() << std::endl; @@ -498,22 +465,19 @@ void OptionsHandler::showConfiguration(const std::string& option, std::exit(0); } -void OptionsHandler::showCopyright(const std::string& option, - const std::string& flag) +void OptionsHandler::showCopyright(const std::string& flag) { std::cout << Configuration::copyright() << std::endl; std::exit(0); } -void OptionsHandler::showVersion(const std::string& option, - const std::string& flag) +void OptionsHandler::showVersion(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) +void OptionsHandler::showDebugTags(const std::string& flag) { if (!Configuration::isDebugBuild()) { @@ -527,8 +491,7 @@ void OptionsHandler::showDebugTags(const std::string& option, std::exit(0); } -void OptionsHandler::showTraceTags(const std::string& option, - const std::string& flag) +void OptionsHandler::showTraceTags(const std::string& flag) { if (!Configuration::isTracingBuild()) { @@ -538,8 +501,7 @@ void OptionsHandler::showTraceTags(const std::string& option, std::exit(0); } -void OptionsHandler::setDumpMode(const std::string& option, - const std::string& flag, +void OptionsHandler::setDumpMode(const std::string& flag, const std::string& optarg) { #ifdef CVC5_DUMPING @@ -550,8 +512,7 @@ void OptionsHandler::setDumpMode(const std::string& option, #endif /* CVC5_DUMPING */ } -void OptionsHandler::setDumpStream(const std::string& option, - const std::string& flag, +void OptionsHandler::setDumpStream(const std::string& flag, const ManagedOut& mo) { #ifdef CVC5_DUMPING diff --git a/src/options/options_handler.h b/src/options/options_handler.h index c3cd8c358..077e2119d 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -46,10 +46,7 @@ class OptionsHandler OptionsHandler(Options* options); template - void checkMinimum(const std::string& option, - const std::string& flag, - T value, - T minimum) const + void checkMinimum(const std::string& flag, T value, T minimum) const { if (value < minimum) { @@ -61,10 +58,7 @@ class OptionsHandler } } template - void checkMaximum(const std::string& option, - const std::string& flag, - T value, - T maximum) const + void checkMaximum(const std::string& flag, T value, T maximum) const { if (value > maximum) { @@ -78,107 +72,69 @@ class OptionsHandler /******************************* 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); + void setErrStream(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); + Language stringToLanguage(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); + void languageIsNotAST(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); + void applyOutputLanguage(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); + void setVerbosity(const std::string& flag, int value); /** Decrease verbosity and call setVerbosity */ - void decreaseVerbosity(const std::string& option, const std::string& flag); + void decreaseVerbosity(const std::string& flag); /** Increase verbosity and call setVerbosity */ - void increaseVerbosity(const std::string& option, const std::string& flag); + void increaseVerbosity(const std::string& flag); /** If statistics are disabled, disable statistics sub-options */ - void setStats(const std::string& option, const std::string& flag, bool value); + void setStats(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); + void setStatsDetail(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); + void enableTraceTag(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); + void enableDebugTag(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); + void enableOutputTag(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); + void setPrintSuccess(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, - const std::string& optarg); + void setResourceWeight(const std::string& flag, const std::string& optarg); /******************************* bv options *******************************/ /** Check that abc is enabled */ - void abcEnabledBuild(const std::string& option, - const std::string& flag, - bool value); + void abcEnabledBuild(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); + void abcEnabledBuild(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 checkBvSatSolver(const std::string& flag, SatSolverMode m); /** Check that we use eager bitblasting for aig */ - void setBitblastAig(const std::string& option, - const std::string& flag, - bool arg); + void setBitblastAig(const std::string& flag, bool arg); /******************************* expr options *******************************/ /** Set ExprSetDepth on all output streams */ - void setDefaultExprDepth(const std::string& option, - const std::string& flag, - int depth); + void setDefaultExprDepth(const std::string& flag, int depth); /** Set ExprDag on all output streams */ - void setDefaultDagThresh(const std::string& option, - const std::string& flag, - int dag); + void setDefaultDagThresh(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); + void showConfiguration(const std::string& flag); /** Show copyright information and exit */ - void showCopyright(const std::string& option, const std::string& flag); + void showCopyright(const std::string& flag); /** Show version information and exit */ - void showVersion(const std::string& option, const std::string& flag); + void showVersion(const std::string& flag); /** Show all debug tags and exit */ - void showDebugTags(const std::string& option, const std::string& flag); + void showDebugTags(const std::string& flag); /** Show all trace tags and exit */ - void showTraceTags(const std::string& option, const std::string& flag); + void showTraceTags(const std::string& flag); /******************************* smt options *******************************/ /** Set a mode on the dumping output stream. */ - void setDumpMode(const std::string& option, - const std::string& flag, - const std::string& optarg); + void setDumpMode(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); + void setDumpStream(const std::string& flag, const ManagedOut& mo); private: /** Pointer to the containing Options object.*/ diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index df61249af..a6ab6efde 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -86,9 +86,7 @@ namespace cvc5::options /** Default handler that triggers a compiler error */ template - T handleOption(const std::string& option, - const std::string& flag, - const std::string& optionarg) + T handleOption(const std::string& flag, const std::string& optionarg) { T::unsupported_handleOption_specialization; return *static_cast(nullptr); @@ -96,17 +94,14 @@ namespace cvc5::options /** Handle a string option by returning it as is. */ template <> - std::string handleOption(const std::string& option, - const std::string& flag, + std::string handleOption(const std::string& flag, const std::string& optionarg) { return optionarg; } /** Handle a bool option, recognizing "true" or "false". */ template <> - bool handleOption(const std::string& option, - const std::string& flag, - const std::string& optionarg) + bool handleOption(const std::string& flag, const std::string& optionarg) { if (optionarg == "true") { @@ -122,8 +117,7 @@ namespace cvc5::options /** Handle a double option, using `parseNumber` with `std::stod`. */ template <> - double handleOption(const std::string& option, - const std::string& flag, + double handleOption(const std::string& flag, const std::string& optionarg) { return parseNumber( @@ -135,8 +129,7 @@ namespace cvc5::options /** Handle a int64_t option, using `parseNumber` with `std::stoll`. */ template <> - int64_t handleOption(const std::string& option, - const std::string& flag, + int64_t handleOption(const std::string& flag, const std::string& optionarg) { return parseNumber( @@ -148,8 +141,7 @@ namespace cvc5::options /** Handle a uint64_t option, using `parseNumber` with `std::stoull`. */ template <> - uint64_t handleOption(const std::string& option, - const std::string& flag, + uint64_t handleOption(const std::string& flag, const std::string& optionarg) { return parseNumber( @@ -161,8 +153,7 @@ namespace cvc5::options /** Handle a ManagedIn option. */ template <> - ManagedIn handleOption(const std::string& option, - const std::string& flag, + ManagedIn handleOption(const std::string& flag, const std::string& optionarg) { ManagedIn res; @@ -172,8 +163,7 @@ namespace cvc5::options /** Handle a ManagedErr option. */ template <> - ManagedErr handleOption(const std::string& option, - const std::string& flag, + ManagedErr handleOption(const std::string& flag, const std::string& optionarg) { ManagedErr res; @@ -183,8 +173,7 @@ namespace cvc5::options /** Handle a ManagedOut option. */ template <> - ManagedOut handleOption(const std::string& option, - const std::string& flag, + ManagedOut handleOption(const std::string& flag, const std::string& optionarg) { ManagedOut res; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6fdd45c4e..7c813cee0 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -836,15 +836,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { if (opts.arith.nlCadWasSetByUser) { - std::stringstream ss; - ss << "Cannot use " << options::arith::nlCad__name - << " without configuring with --poly."; - throw OptionException(ss.str()); + throw OptionException( + "Cannot use --nl-cad without configuring with --poly."); } else { - Notice() << "Cannot use --" << options::arith::nlCad__name - << " without configuring with --poly." << std::endl; + Notice() << "Cannot use --nl-cad without configuring with --poly." + << std::endl; opts.arith.nlCad = false; opts.arith.nlExt = options::NlExtMode::FULL; } -- 2.30.2