Remove options::getAll() (#7111)

options::getAll() returns a list of all options and their current values as strings. The same functionality can be obtained by using options::getNames() and options::get(). This PR does exactly this replacement, getting rid of a large chunk of generated code. Calling getInfo("all-options") may suffer a minor performance hit, but not noticeable in practice.

4 files changed, 11 insertions, 39 deletions

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 30c2fc1c3..289fa95db 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -214,22 +214,6 @@ def get_predicates(option):
     return res
 
 
-def get_getall(module, option):
-    """Render snippet to add option to result of getAll()"""
-    if option.type == 'bool':
-        return 'res.push_back({{"{}", opts.{}.{} ? "true" : "false"}});'.format(
-            option.long_name, module.id, option.name)
-    elif option.type == 'std::string':
-        return 'res.push_back({{"{}", opts.{}.{}}});'.format(
-            option.long_name, module.id, option.name)
-    elif is_numeric_cpp_type(option.type):
-        return 'res.push_back({{"{}", std::to_string(opts.{}.{})}});'.format(
-            option.long_name, module.id, option.name)
-    else:
-        return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format(module.id,
-            option.name, option.long_name)
-
-
 class Module(object):
     """Options module.
 
@@ -700,7 +684,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
     headers_handler = set()  # option includes (for handlers, predicates, ...)
     getopt_short = []        # short options for getopt_long
     getopt_long = []         # long options for getopt_long
-    options_getall = []      # options for options::getAll()
     options_get_info = []    # code for getOptionInfo()
     options_handler = []     # option handler calls
     options_names = set()    # option names
@@ -889,11 +872,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                 cases.append('  break;')
                 options_handler.extend(cases)
 
-            if option.name:
-                # Build options for options::getOptions()
-                if option.long_name:
-                    options_getall.append(get_getall(module, option))
-
     options_all_names = ', '.join(map(lambda s: '"' + s + '"', sorted(options_names)))
     options_all_names = '\n'.join(textwrap.wrap(options_all_names, width=80, break_on_hyphens=False))
 
@@ -911,7 +889,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
         'help_others': '\n'.join(help_others),
         'options_handler': '\n    '.join(options_handler),
         'options_short': ''.join(getopt_short),
-        'options_getall': '\n  '.join(options_getall),
         'options_all_names': options_all_names,
         'options_get_info': '\n  '.join(sorted(options_get_info)),
         'getoption_handlers': '\n'.join(getoption_handlers),
diff --git a/src/options/options_public.h b/src/options/options_public.h
index 17a70cadd..afd777761 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -10,7 +10,11 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Global (command-line, set-option, ...) parameters for SMT.
+ * Implements a basic options API intended to be used by the external API:
+ * - list option names (`getNames()`)
+ * - get option value by name (`get()`)
+ * - set option value by name (`set()`)
+ * - get more detailed option information (`getInfo()`)
  */
 
 #include "cvc5_public.h"
@@ -47,11 +51,6 @@ void set(Options& opts,
          const std::string& optionarg) CVC5_EXPORT;
 
 /**
- * Get the setting for all options.
- */
-std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT;
-
-/**
  * Get a (sorted) list of all option names that are available.
  */
 std::vector<std::string> getNames() CVC5_EXPORT;
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index 6269894b4..4beb47e0f 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -257,15 +257,6 @@ void set(Options& opts, const std::string& name, const std::string& optionarg)
   setInternal(opts, name, optionarg);
 }
 
-std::vector<std::vector<std::string> > getAll(const Options& opts)
-{
-  std::vector<std::vector<std::string>> res;
-  // clang-format off
-  ${options_getall}$
-  // clang-format on
-  return res;
-}
-
 std::vector<std::string> getNames()
 {
   return {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5403928ec..72268aa03 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -520,7 +520,12 @@ std::string SmtEngine::getInfo(const std::string& key) const
   }
   Assert(key == "all-options");
   // get the options, like all-statistics
-  return toSExpr(options::getAll(getOptions()));
+  std::vector<std::vector<std::string>> res;
+  for (const auto& opt: options::getNames())
+  {
+    res.emplace_back(std::vector<std::string>{opt, options::get(getOptions(), opt)});
+  }
+  return toSExpr(res);
 }
 
 void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)