From 71842aa75ca106b14ded148a73ac856f3ecf5912 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 19 Oct 2021 12:33:25 -0700
Subject: [PATCH] Remove setDefaults methods (#7413)

This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.
---
 src/options/mkoptions.py        | 34 ---------------------------------
 src/options/module_template.cpp |  7 -------
 src/options/module_template.h   |  2 --
 src/options/options_handler.cpp |  5 ++++-
 4 files changed, 4 insertions(+), 44 deletions(-)

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index a8f631de6..57f8b64e6 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -480,17 +480,6 @@ def generate_module_option_names(module):
         'static constexpr const char* {name}__name = "{long_name}";', relevant)
 
 
-def generate_module_setdefaults_decl(module):
-    res = []
-    for option in module.options:
-        if option.name is None:
-            continue
-        funcname = option.name[0].capitalize() + option.name[1:]
-        res.append('void setDefault{}(Options& opts, {} value);'.format(
-            funcname, option.type))
-    return '\n'.join(res)
-
-
 ################################################################################
 # for options/<module>.cpp
 
@@ -581,27 +570,6 @@ def generate_module_mode_impl(module):
     return '\n'.join(res)
 
 
-TPL_SETDEFAULT_IMPL = '''void setDefault{capname}(Options& opts, {type} value)
-{{
-    if (!opts.{module}.{name}WasSetByUser) opts.{module}.{name} = value;
-}}'''
-
-
-def generate_module_setdefaults_impl(module):
-    res = []
-    for option in module.options:
-        if option.name is None:
-            continue
-        fmt = {
-            'capname': option.name[0].capitalize() + option.name[1:],
-            'type': option.type,
-            'module': module.id,
-            'name': option.name,
-        }
-        res.append(TPL_SETDEFAULT_IMPL.format(**fmt))
-    return '\n'.join(res)
-
-
 ################################################################################
 # for main/options.cpp
 
@@ -875,11 +843,9 @@ def codegen_module(module, dst_dir, tpls):
         'holder_decl': generate_module_holder_decl(module),
         'wrapper_functions': generate_module_wrapper_functions(module),
         'option_names': generate_module_option_names(module),
-        'setdefaults_decl': generate_module_setdefaults_decl(module),
         # module source
         'header': module.header,
         'modes_impl': generate_module_mode_impl(module),
-        'setdefaults_impl': generate_module_setdefaults_impl(module),
     }
     for tpl in tpls:
         filename = tpl['output'].replace('module', module.filename)
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index ee5260f34..d2ece3f13 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -28,11 +28,4 @@ namespace cvc5::options {
 ${modes_impl}$
 // clang-format on
 
-namespace ${id}$
-{
-// clang-format off
-${setdefaults_impl}$
-// clang-format on
-}
-
 }  // namespace cvc5::options
diff --git a/src/options/module_template.h b/src/options/module_template.h
index 61d689b72..d9b591f11 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -56,8 +56,6 @@ namespace ${id}$
 {
 // clang-format off
 ${option_names}$
-
-${setdefaults_decl}$
 // clang-format on
 }
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 93b08a858..ec6c831e4 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -387,7 +387,10 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
                             + " does not support lazy bit-blasting.\n"
                             + "Try --bv-sat-solver=minisat");
     }
-    options::bv::setDefaultBitvectorToBool(*d_options, true);
+    if (!d_options->bv.bitvectorToBoolWasSetByUser)
+    {
+      d_options->bv.bitvectorToBool = true;
+    }
   }
 }
 
-- 
2.30.2