Clean up options holder class (#6458)

This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index fa2a39b04165fc8f70343c9c552da9cd5113ff2a..13df7b8bdf77a083ac103acb92b0f8c98f10bfaa 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -121,8 +121,10 @@ TPL_PUSHBACK_PREEMPT = 'extender->pushBackPreemption({});'
 TPL_HOLDER_MACRO = '#define ' + TPL_HOLDER_MACRO_NAME
 
 TPL_HOLDER_MACRO_ATTR = "  {name}__option_t::type {name};\\\n"
-TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__;"
+TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__ = false;"
 
+TPL_HOLDER_MACRO_ATTR_DEF = "  {name}__option_t::type {name} = {default};\\\n"
+TPL_HOLDER_MACRO_ATTR_DEF += "  bool {name}__setByUser__ = false;"
 
 TPL_OPTION_STRUCT_RW = \
 """extern struct {name}__option_t
@@ -450,7 +452,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         includes.update([format_include(x) for x in option.includes])
 
         # Generate option holder macro
-        holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name))
+        if option.default:
+            default = option.default
+            if option.mode and option.type not in default:
+                default = '{}::{}'.format(option.type, default)
+            holder_specs.append(TPL_HOLDER_MACRO_ATTR_DEF.format(name=option.name, default=default))
+        else:
+            holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name))
 
         # Generate module declaration
         tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW

diff --git a/src/options/options.h b/src/options/options.h
index b249c90edd2f5fe1a07d426f5e04547e2415184d..a8fc50b68970e08cb3bee10f8951aeec9a321279 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -19,6 +19,7 @@
 #define CVC5__OPTIONS__OPTIONS_H
 
 #include <iosfwd>
+#include <memory>
 #include <string>
 #include <vector>
 
@@ -45,7 +46,7 @@ class CVC5_EXPORT Options
 {
   friend api::Solver;
   /** The struct that holds all option values. */
-  options::OptionsHolder* d_holder;
+  std::unique_ptr<options::OptionsHolder> d_holder;
 
   /** The handler for the options of the theory. */
   options::OptionsHandler* d_handler;
@@ -251,22 +252,6 @@ public:
   /** Print help for the --lang command line option */
   static void printLanguageHelp(std::ostream& out);
 
-  /**
-   * Look up long command-line option names that bear some similarity
-   * to the given name.  Returns an empty string if there are no
-   * suggestions.
-   */
-  static std::string suggestCommandLineOptions(const std::string& optionName);
-
-  /**
-   * Look up SMT option names that bear some similarity to
-   * the given name.  Don't include the initial ":".  This might be
-   * useful in case of typos.  Can return an empty vector if there are
-   * no suggestions.
-   */
-  static std::vector<std::string> suggestSmtOptions(
-      const std::string& optionName);
-
   /**
    * Initialize the Options object options based on the given
    * command-line arguments given in argc and argv.  The return value

diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
index 8f5a0e096bf2549aae0a772b37e1dad729acbc7c..04e5eba531448f1018f1870a61e57ce0092b390c 100644 (file)
--- a/src/options/options_holder_template.h
+++ b/src/options/options_holder_template.h
@@ -24,13 +24,20 @@ ${headers_module}$
 namespace cvc5 {
 namespace options {
 
+#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+
 struct OptionsHolder
 {
-  OptionsHolder();
   ${macros_module}$
 
 }; /* struct OptionsHolder */
 
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
 }  // namespace options
 }  // namespace cvc5
 

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 4493f6094226bc2f5511c77da4698d6c91e946db..49a35ab38c2a1f5aae99199d49bd388181da13e1 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -230,13 +230,11 @@ Options::Options(OptionsListener* ol)
 
 Options::~Options() {
   delete d_handler;
-  delete d_holder;
 }
 
 void Options::copyValues(const Options& options){
   if(this != &options) {
-    delete d_holder;
-    d_holder = new options::OptionsHolder(*options.d_holder);
+    *d_holder = *options.d_holder;
   }
 }
 
@@ -254,19 +252,6 @@ void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
 ${custom_handlers}$
 // clang-format on
 
-#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
-
-// clang-format off
-options::OptionsHolder::OptionsHolder() :
-  ${module_defaults}$
-{
-}
-// clang-format on
-
 static const std::string mostCommonOptionsDescription =
     "\
 Most commonly-used cvc5 options:\n"
@@ -419,6 +404,18 @@ std::vector<std::string> Options::parseOptions(Options* options,
   return nonoptions;
 }
 
+std::string suggestCommandLineOptions(const std::string& optionName)
+{
+  DidYouMean didYouMean;
+
+  const char* opt;
+  for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) {
+    didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
+  }
+
+  return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
+}
+
 void Options::parseOptionsRecursive(int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions)
@@ -531,39 +528,6 @@ ${options_handler}$
                    << " non-option arguments." << std::endl;
 }
 
-std::string Options::suggestCommandLineOptions(const std::string& optionName)
-{
-  DidYouMean didYouMean;
-
-  const char* opt;
-  for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
-    didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
-  }
-
-  return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
-}
-
-// clang-format off
-static const char* smtOptions[] = {
-  ${options_smt}$
-  nullptr};
-// clang-format on
-
-std::vector<std::string> Options::suggestSmtOptions(
-    const std::string& optionName)
-{
-  std::vector<std::string> suggestions;
-
-  const char* opt;
-  for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
-    if(std::strstr(opt, optionName.c_str()) != NULL) {
-      suggestions.push_back(opt);
-    }
-  }
-
-  return suggestions;
-}
-
 // clang-format off
 std::vector<std::vector<std::string> > Options::getOptions() const
 {
@@ -608,8 +572,5 @@ std::string Options::getOption(const std::string& key) const
 }
 // clang-format on
 
-#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
-
 }  // namespace cvc5
-// clang-format on
+