diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-28 19:31:41 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-28 19:31:41 +0200 |
commit | b5ac06abf4b2cc6b027dedd045595187589bcc35 (patch) | |
tree | 02c1a7ebc6f41612ee92ce664b0068d45fe9b7b9 /src | |
parent | a6a63f6c46dcf83ac2dc253b66012be224391494 (diff) |
Clean up options holder class (#6458)
This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/mkoptions.py | 12 | ||||
-rw-r--r-- | src/options/options.h | 19 | ||||
-rw-r--r-- | src/options/options_holder_template.h | 9 | ||||
-rw-r--r-- | src/options/options_template.cpp | 67 |
4 files changed, 34 insertions, 73 deletions
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index fa2a39b04..13df7b8bd 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -121,8 +121,10 @@ TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});' TPL_HOLDER_MACRO = '#define ' + TPL_HOLDER_MACRO_NAME TPL_HOLDER_MACRO_ATTR = " {name}__option_t::type {name};\\\n" -TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__;" +TPL_HOLDER_MACRO_ATTR += " bool {name}__setByUser__ = false;" +TPL_HOLDER_MACRO_ATTR_DEF = " {name}__option_t::type {name} = {default};\\\n" +TPL_HOLDER_MACRO_ATTR_DEF += " bool {name}__setByUser__ = false;" TPL_OPTION_STRUCT_RW = \ """extern struct {name}__option_t @@ -450,7 +452,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): includes.update([format_include(x) for x in option.includes]) # Generate option holder macro - holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name)) + if option.default: + default = option.default + if option.mode and option.type not in default: + default = '{}::{}'.format(option.type, default) + holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(name=option.name, default=default)) + else: + holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name)) # Generate module declaration tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW diff --git a/src/options/options.h b/src/options/options.h index b249c90ed..a8fc50b68 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -19,6 +19,7 @@ #define CVC5__OPTIONS__OPTIONS_H #include <iosfwd> +#include <memory> #include <string> #include <vector> @@ -45,7 +46,7 @@ class CVC5_EXPORT Options { friend api::Solver; /** The struct that holds all option values. */ - options::OptionsHolder* d_holder; + std::unique_ptr<options::OptionsHolder> d_holder; /** The handler for the options of the theory. */ options::OptionsHandler* d_handler; @@ -252,22 +253,6 @@ public: static void printLanguageHelp(std::ostream& out); /** - * Look up long command-line option names that bear some similarity - * to the given name. Returns an empty string if there are no - * suggestions. - */ - static std::string suggestCommandLineOptions(const std::string& optionName); - - /** - * Look up SMT option names that bear some similarity to - * the given name. Don't include the initial ":". This might be - * useful in case of typos. Can return an empty vector if there are - * no suggestions. - */ - static std::vector<std::string> suggestSmtOptions( - const std::string& optionName); - - /** * Initialize the Options object options based on the given * command-line arguments given in argc and argv. The return value * is what's left of the command line (that is, the non-option diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h index 8f5a0e096..04e5eba53 100644 --- a/src/options/options_holder_template.h +++ b/src/options/options_holder_template.h @@ -24,13 +24,20 @@ ${headers_module}$ namespace cvc5 { namespace options { +#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) +# define DO_SEMANTIC_CHECKS_BY_DEFAULT false +#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ +# define DO_SEMANTIC_CHECKS_BY_DEFAULT true +#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ + struct OptionsHolder { - OptionsHolder(); ${macros_module}$ }; /* struct OptionsHolder */ +#undef DO_SEMANTIC_CHECKS_BY_DEFAULT + } // namespace options } // namespace cvc5 diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 4493f6094..49a35ab38 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -230,13 +230,11 @@ Options::Options(OptionsListener* ol) Options::~Options() { delete d_handler; - delete d_holder; } void Options::copyValues(const Options& options){ if(this != &options) { - delete d_holder; - d_holder = new options::OptionsHolder(*options.d_holder); + *d_holder = *options.d_holder; } } @@ -254,19 +252,6 @@ void Options::setListener(OptionsListener* ol) { d_olisten = ol; } ${custom_handlers}$ // clang-format on -#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) -# define DO_SEMANTIC_CHECKS_BY_DEFAULT false -#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ -# define DO_SEMANTIC_CHECKS_BY_DEFAULT true -#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ - -// clang-format off -options::OptionsHolder::OptionsHolder() : - ${module_defaults}$ -{ -} -// clang-format on - static const std::string mostCommonOptionsDescription = "\ Most commonly-used cvc5 options:\n" @@ -419,6 +404,18 @@ std::vector<std::string> Options::parseOptions(Options* options, return nonoptions; } +std::string suggestCommandLineOptions(const std::string& optionName) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); + } + + return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); +} + void Options::parseOptionsRecursive(int argc, char* argv[], std::vector<std::string>* nonoptions) @@ -531,39 +528,6 @@ ${options_handler}$ << " non-option arguments." << std::endl; } -std::string Options::suggestCommandLineOptions(const std::string& optionName) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) { - didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); - } - - return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); -} - -// clang-format off -static const char* smtOptions[] = { - ${options_smt}$ - nullptr}; -// clang-format on - -std::vector<std::string> Options::suggestSmtOptions( - const std::string& optionName) -{ - std::vector<std::string> suggestions; - - const char* opt; - for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) { - if(std::strstr(opt, optionName.c_str()) != NULL) { - suggestions.push_back(opt); - } - } - - return suggestions; -} - // clang-format off std::vector<std::vector<std::string> > Options::getOptions() const { @@ -608,8 +572,5 @@ std::string Options::getOption(const std::string& key) const } // clang-format on -#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT -#undef DO_SEMANTIC_CHECKS_BY_DEFAULT - } // namespace cvc5 -// clang-format on + |