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 b6efb16957eea3f2bb3c6c4eae251c7ef2dbaba6..b99fbc1b662f678b7d8ba5d28a8c0d8d9603840d 100644 (file)
--- 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<options::Holder{id_cap}>()),', 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 b80e5a3b89499a607b863408356aa096e2a5ead2..a6ddbec1e3ff369af4d23a5e20bfe9a3b80c6919 100644 (file)
--- 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 9419e9914abf147d2246369a0f6221f52a5e232d..26e11a6701f34fb2dc3291d97509a9ba3ad3dd5d 100644 (file)
--- 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<std::string> 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<std::string> nonoptions;
   options->parseOptionsRecursive(argc, argv, &nonoptions);

diff --git a/src/options/options_template.h b/src/options/options_template.h
index a25ddc58c276d55233a5365decd495cd93404f57..9d5e70099bb43fc3cdcd2d073c498ef97170c823 100644 (file)
--- 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