From: Gereon Kremer Date: Wed, 26 May 2021 20:30:19 +0000 (+0200) Subject: Use references instead of getter functions (#6597) X-Git-Tag: cvc5-1.0.0~1692 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=028d657dc41bbb908b7b9ad6ba707dc2216b15ac;p=cvc5.git Use references instead of getter functions (#6597) This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules. --- diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index b6efb1695..b99fbc1b6 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -88,8 +88,8 @@ TPL_IMPL_ASSIGN = \ {{ auto parsedval = {handler}; {predicates} - {module}().{name} = parsedval; - {module}().{name}__setByUser__ = true; + {module}.{name} = parsedval; + {module}.{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" @@ -100,8 +100,8 @@ TPL_IMPL_ASSIGN_BOOL = \ bool value) {{ {predicates} - {module}().{name} = value; - {module}().{name}__setByUser__ = true; + {module}.{name} = value; + {module}.{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" @@ -138,7 +138,7 @@ TPL_DECL_SET = \ TPL_IMPL_SET = TPL_DECL_SET[:-1] + \ """ {{ - return {module}().{name}; + return {module}.{name}; }}""" @@ -149,7 +149,7 @@ TPL_DECL_OP_BRACKET = \ TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \ """ {{ - return {module}().{name}; + return {module}.{name}; }}""" @@ -159,7 +159,7 @@ TPL_DECL_WAS_SET_BY_USER = \ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ """ {{ - return {module}().{name}__setByUser__; + return {module}.{name}__setByUser__; }}""" # Option specific methods @@ -242,21 +242,19 @@ def get_holder_mem_inits(modules): return concat_format(' d_{id}(std::make_unique()),', modules) +def get_holder_ref_inits(modules): + """Render initializations of holder references of the Option class""" + return concat_format(' {id}(*d_{id}),', modules) + + def get_holder_mem_copy(modules): """Render copy operation of holder members of the Option class""" return concat_format(' *d_{id} = *options.d_{id};', modules) -def get_holder_getter_decls(modules): - """Render getter declarations for holder members of the Option class""" - return concat_format(''' const options::Holder{id_cap}& {id}() const; - options::Holder{id_cap}& {id}();''', modules) - - -def get_holder_getter_impl(modules): - """Render getter implementations for holder members of the Option class""" - return concat_format('''const options::Holder{id_cap}& Options::{id}() const {{ return *d_{id}; }} -options::Holder{id_cap}& Options::{id}() {{ return *d_{id}; }}''', modules) +def get_holder_ref_decls(modules): + """Render reference declarations for holder members of the Option class""" + return concat_format(' options::Holder{id_cap}& {id};', modules) class Module(object): @@ -930,13 +928,13 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ options_smt.append('"{}",'.format(optname)) if option.type == 'bool': - s = 'opts.push_back({{"{}", {}().{} ? "true" : "false"}});'.format( + s = 'opts.push_back({{"{}", {}.{} ? "true" : "false"}});'.format( optname, module.id, option.name) elif is_numeric_cpp_type(option.type): - s = 'opts.push_back({{"{}", std::to_string({}().{})}});'.format( + s = 'opts.push_back({{"{}", std::to_string({}.{})}});'.format( optname, module.id, option.name) else: - s = '{{ std::stringstream ss; ss << {}().{}; opts.push_back({{"{}", ss.str()}}); }}'.format( + s = '{{ std::stringstream ss; ss << {}.{}; opts.push_back({{"{}", ss.str()}}); }}'.format( module.id, option.name, optname) options_getoptions.append(s) @@ -965,16 +963,16 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ write_file(dst_dir, 'options.h', tpl_options_h.format( holder_fwd_decls=get_holder_fwd_decls(modules), - holder_getter_decls=get_holder_getter_decls(modules), holder_mem_decls=get_holder_mem_decls(modules), + holder_ref_decls=get_holder_ref_decls(modules), )) write_file(dst_dir, 'options.cpp', tpl_options_cpp.format( headers_module='\n'.join(headers_module), headers_handler='\n'.join(sorted(list(headers_handler))), - holder_getter_impl=get_holder_getter_impl(modules), holder_mem_copy=get_holder_mem_copy(modules), holder_mem_inits=get_holder_mem_inits(modules), + holder_ref_inits=get_holder_ref_inits(modules), custom_handlers='\n'.join(custom_handlers), module_defaults=',\n '.join(defaults), help_common='\n'.join(help_common), diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b80e5a3b8..a6ddbec1e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -83,7 +83,7 @@ unsigned long OptionsHandler::limitHandler(std::string option, void OptionsHandler::setResourceWeight(std::string option, std::string optarg) { - d_options->resman().resourceWeightHolder.emplace_back(optarg); + d_options->resman.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h @@ -258,24 +258,24 @@ void OptionsHandler::setStats(const std::string& option, bool value) { if (option == options::base::statisticsAll__name) { - d_options->base().statistics = true; + d_options->base.statistics = true; } else if (option == options::base::statisticsEveryQuery__name) { - d_options->base().statistics = true; + d_options->base.statistics = true; } else if (option == options::base::statisticsExpert__name) { - d_options->base().statistics = true; + d_options->base.statistics = true; } } else { if (option == options::base::statistics__name) { - d_options->base().statisticsAll = false; - d_options->base().statisticsEveryQuery = false; - d_options->base().statisticsExpert = false; + d_options->base.statisticsAll = false; + d_options->base.statisticsEveryQuery = false; + d_options->base.statisticsExpert = false; } } } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 9419e9914..26e11a670 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -225,6 +225,7 @@ Options::Options(OptionsListener* ol) : d_handler(new options::OptionsHandler(this)), // clang-format off ${holder_mem_inits}$ +${holder_ref_inits}$ // clang-format on d_olisten(ol) {} @@ -241,8 +242,6 @@ ${holder_mem_copy}$ } } -${holder_getter_impl}$ - std::string Options::formatThreadOptionException(const std::string& option) { std::stringstream ss; ss << "can't understand option `" << option @@ -395,7 +394,7 @@ std::vector Options::parseOptions(Options* options, if(x != NULL) { progName = x + 1; } - options->base().binary_name = std::string(progName); + options->base.binary_name = std::string(progName); std::vector nonoptions; options->parseOptionsRecursive(argc, argv, &nonoptions); diff --git a/src/options/options_template.h b/src/options/options_template.h index a25ddc58c..9d5e70099 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -53,6 +53,12 @@ class CVC5_EXPORT Options // clang-format off ${holder_mem_decls}$ // clang-format on + public: +// clang-format off +${holder_ref_decls}$ +// clang-format on + + private: /** The current Options in effect */ static thread_local Options* s_current; @@ -109,9 +115,6 @@ public: Options(OptionsListener* ol = nullptr); ~Options(); -// clang-format off -${holder_getter_decls}$ -// clang-format on /** * Copies the value of the options stored in OptionsHolder into the current