Add non-templated method to set option defaults (#6540)

This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.

6 files changed, 47 insertions, 30 deletions

diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 796fd26fa..840eaa08f 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -33,7 +33,7 @@ name   = "Decision Heuristics"
   name       = "decisionThreshold"
   category   = "expert"
   long       = "decision-threshold=N"
-  type       = "decision::DecisionWeight"
+  type       = "cvc5::decision::DecisionWeight"
   default    = "0"
   includes   = ["options/decision_weight.h"]
   help       = "ignore all nodes greater than threshold in first attempt to pick decision"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index b99fbc1b6..9277fa8d9 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -89,7 +89,7 @@ TPL_IMPL_ASSIGN = \
   auto parsedval = {handler};
   {predicates}
   {module}.{name} = parsedval;
-  {module}.{name}__setByUser__ = true;
+  {module}.{name}__setByUser = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
@@ -101,7 +101,7 @@ TPL_IMPL_ASSIGN_BOOL = \
 {{
   {predicates}
   {module}.{name} = value;
-  {module}.{name}__setByUser__ = true;
+  {module}.{name}__setByUser = true;
   Trace("options") << "user assigned option {name}" << std::endl;
 }}"""
 
@@ -116,11 +116,19 @@ TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},'
 
 TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});'
 
-TPL_HOLDER_MACRO_ATTR = "  {type} {name};\\\n"
-TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__ = false;"
+TPL_HOLDER_MACRO_ATTR = '''  {type} {name};
+  bool {name}__setByUser = false;'''
 
-TPL_HOLDER_MACRO_ATTR_DEF = "  {type} {name} = {default};\\\n"
-TPL_HOLDER_MACRO_ATTR_DEF += "  bool {name}__setByUser__ = false;"
+TPL_HOLDER_MACRO_ATTR_DEF = '''  {type} {name} = {default};
+  bool {name}__setByUser = false;'''
+
+TPL_DECL_SET_DEFAULT = 'void setDefault{funcname}(Options& opts, {type} value);'
+TPL_IMPL_SET_DEFAULT = TPL_DECL_SET_DEFAULT[:-1] + '''
+{{
+    if (!opts.{module}.{name}__setByUser) {{
+        opts.{module}.{name} = value;
+    }}
+}}'''
 
 TPL_NAME_DECL = 'static constexpr const char* {name}__name = "{long_name}";'
 
@@ -152,14 +160,13 @@ TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \
   return {module}.{name};
 }}"""
 
-
 TPL_DECL_WAS_SET_BY_USER = \
 """template <> bool Options::wasSetByUser(options::{name}__option_t) const;"""
 
 TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
 """
 {{
-  return {module}.{name}__setByUser__;
+  return {module}.{name}__setByUser;
 }}"""
 
 # Option specific methods
@@ -566,6 +573,8 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
     decls = []
     specs = []
     inls = []
+    default_decl = []
+    default_impl = []
     mode_decl = []
     mode_impl = []
 
@@ -599,7 +608,10 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name))
         option_names.append(TPL_NAME_DECL.format(name=option.name, type=option.type, long_name = long_name))
 
+        capoptionname = option.name[0].capitalize() + option.name[1:]
+
         # Generate module specialization
+        default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
         specs.append(TPL_DECL_SET.format(name=option.name))
         specs.append(TPL_DECL_OP_BRACKET.format(name=option.name))
         specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
@@ -622,6 +634,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         ### Generate code for {module.name}_options.cpp
 
         # Accessors
+        default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
         accs.append(TPL_IMPL_SET.format(module=module.id, name=option.name))
         accs.append(TPL_IMPL_OP_BRACKET.format(module=module.id, name=option.name))
         accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name))
@@ -674,11 +687,14 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         specs='\n'.join(specs),
         option_names='\n'.join(option_names),
         inls='\n'.join(inls),
+        defaults='\n'.join(default_decl),
         modes=''.join(mode_decl)))
 
     write_file(dst_dir, '{}.cpp'.format(filename), tpl_module_cpp.format(
         header=module.header,
+        id=module.id,
         accs='\n'.join(accs),
+        defaults='\n'.join(default_impl),
         defs='\n'.join(defs),
         modes=''.join(mode_impl)))
 
@@ -959,7 +975,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                 if option.mode and option.type not in default:
                     default = '{}::{}'.format(option.type, default)
                 defaults.append('{}({})'.format(option.name, default))
-                defaults.append('{}__setByUser__(false)'.format(option.name))
+                defaults.append('{}__setByUser(false)'.format(option.name))
 
     write_file(dst_dir, 'options.h', tpl_options_h.format(
         holder_fwd_decls=get_holder_fwd_decls(modules),
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index c79656e4b..bc953b952 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -33,6 +33,14 @@ ${defs}$
 
 ${modes}$
 
+
+namespace ${id}$
+{
+// clang-format off
+${defaults}$
+// clang-format on
+}
+
 }  // namespace options
 }  // namespace cvc5
 // clang-format on
diff --git a/src/options/module_template.h b/src/options/module_template.h
index 219775dd6..722490948 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -71,6 +71,13 @@ namespace options {
 ${inls}$
 // clang-format on
 
+namespace ${id}$
+{
+// clang-format off
+${defaults}$
+// clang-format on
+}
+
 }  // namespace options
 }  // namespace cvc5
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a6ddbec1e..7d9fcffab 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -163,7 +163,7 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
     {
       throwLazyBBUnsupported(m);
     }
-    Options::current().setDefault(options::bitvectorToBool, true);
+    options::bv::setDefaultBitvectorToBool(*d_options, true);
   }
 }
 
@@ -171,10 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
 {
   if (m == options::BitblastMode::LAZY)
   {
-    Options::current().setDefault(options::bitvectorPropagate, true);
-    Options::current().setDefault(options::bitvectorEqualitySolver, true);
-    Options::current().setDefault(options::bitvectorInequalitySolver, true);
-    Options::current().setDefault(options::bitvectorAlgebraicSolver, true);
+    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 (options::bvSatSolver() != options::SatSolverMode::MINISAT)
     {
       throwLazyBBUnsupported(options::bvSatSolver());
@@ -182,7 +182,7 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
   }
   else if (m == BitblastMode::EAGER)
   {
-    Options::current().setDefault(options::bitvectorToBool, true);
+    options::bv::setDefaultBitvectorToBool(*d_options, true);
   }
 }
 
diff --git a/src/options/options_template.h b/src/options/options_template.h
index 9d5e70099..f5ea87c54 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -133,20 +133,6 @@ public:
   }
 
   /**
-   * Set the default value of the given option. Is equivalent to calling `set()`
-   * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time
-   * error if the given option is read-only.
-   */
-  template <class T>
-  void setDefault(T t, const typename T::type& val)
-  {
-    if (!wasSetByUser(t))
-    {
-      ref(t) = val;
-    }
-  }
-
-  /**
    * Get a non-const reference to the value of the given option. Causes a
    * compile-time error if the given option is read-only. Writeable options
    * specialize this template with a real implementation.