Move option names out of struct (#6554)

This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index a7212641ce2afbb1f92b96dc0c44e2709831c8e3..b6efb16957eea3f2bb3c6c4eae251c7ef2dbaba6 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -122,12 +122,13 @@ TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__ = false;"
 TPL_HOLDER_MACRO_ATTR_DEF = "  {type} {name} = {default};\\\n"
 TPL_HOLDER_MACRO_ATTR_DEF += "  bool {name}__setByUser__ = false;"
 
+TPL_NAME_DECL = 'static constexpr const char* {name}__name = "{long_name}";'
+
 TPL_OPTION_STRUCT_RW = \
 """extern struct {name}__option_t
 {{
   typedef {type} type;
   type operator()() const;
-  static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
 TPL_DECL_SET = \
@@ -563,6 +564,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
     # *_options.h
     includes = set()
     holder_specs = []
+    option_names = []
     decls = []
     specs = []
     inls = []
@@ -597,6 +599,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         else:
             long_name = ""
         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))
 
         # Generate module specialization
         specs.append(TPL_DECL_SET.format(name=option.name))
@@ -668,9 +671,10 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         id_cap=module.id_cap,
         id=module.id,
         includes='\n'.join(sorted(list(includes))),
-        holder_spec=' \\\n'.join(holder_specs),
+        holder_spec='\n'.join(holder_specs),
         decls='\n'.join(decls),
         specs='\n'.join(specs),
+        option_names='\n'.join(option_names),
         inls='\n'.join(inls),
         modes=''.join(mode_decl)))
 

diff --git a/src/options/module_template.h b/src/options/module_template.h
index 4e031d8435c14e3d552aab70cafb29c41a303622..219775dd612bb33f1ba09a431290f71ae28442e7 100644 (file)
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -53,6 +53,13 @@ ${holder_spec}$
 ${decls}$
 // clang-format on
 
+namespace ${id}$
+{
+// clang-format off
+${option_names}$
+// clang-format on
+}
+
 }  // namespace options
 
 // clang-format off

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index ee5396dffaf79c3f9d32339f5304e045a13769a9..b80e5a3b89499a607b863408356aa096e2a5ead2 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -256,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value)
   std::string opt = option.substr(2);
   if (value)
   {
-    if (opt == options::statisticsAll.name)
+    if (option == options::base::statisticsAll__name)
     {
       d_options->base().statistics = true;
     }
-    else if (opt == options::statisticsEveryQuery.name)
+    else if (option == options::base::statisticsEveryQuery__name)
     {
       d_options->base().statistics = true;
     }
-    else if (opt == options::statisticsExpert.name)
+    else if (option == options::base::statisticsExpert__name)
     {
       d_options->base().statistics = true;
     }
   }
   else
   {
-    if (opt == options::statistics.name)
+    if (option == options::base::statistics__name)
     {
       d_options->base().statisticsAll = false;
       d_options->base().statisticsEveryQuery = false;

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 05bad2727b2bdcee5c794beb07a773e8b13529a8..3fc58ff0523a55a9bfac52ce077894227c801903 100644 (file)
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -33,31 +33,31 @@ OptionsManager::OptionsManager(Options* opts) : d_options(opts)
   // set options that must take effect immediately
   if (opts->wasSetByUser(options::defaultExprDepth))
   {
-    notifySetOption(options::defaultExprDepth.name);
+    notifySetOption(options::expr::defaultExprDepth__name);
   }
   if (opts->wasSetByUser(options::defaultDagThresh))
   {
-    notifySetOption(options::defaultDagThresh.name);
+    notifySetOption(options::expr::defaultDagThresh__name);
   }
   if (opts->wasSetByUser(options::dumpModeString))
   {
-    notifySetOption(options::dumpModeString.name);
+    notifySetOption(options::smt::dumpModeString__name);
   }
   if (opts->wasSetByUser(options::printSuccess))
   {
-    notifySetOption(options::printSuccess.name);
+    notifySetOption(options::base::printSuccess__name);
   }
   if (opts->wasSetByUser(options::diagnosticChannelName))
   {
-    notifySetOption(options::diagnosticChannelName.name);
+    notifySetOption(options::smt::diagnosticChannelName__name);
   }
   if (opts->wasSetByUser(options::regularChannelName))
   {
-    notifySetOption(options::regularChannelName.name);
+    notifySetOption(options::smt::regularChannelName__name);
   }
   if (opts->wasSetByUser(options::dumpToFileName))
   {
-    notifySetOption(options::dumpToFileName.name);
+    notifySetOption(options::smt::dumpToFileName__name);
   }
   // set this as a listener to be notified of options changes from now on
   opts->setListener(this);
@@ -69,7 +69,7 @@ void OptionsManager::notifySetOption(const std::string& key)
 {
   Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")"
                << std::endl;
-  if (key == options::defaultExprDepth.name)
+  if (key == options::expr::defaultExprDepth__name)
   {
     int depth = (*d_options)[options::defaultExprDepth];
     Debug.getStream() << expr::ExprSetDepth(depth);
@@ -80,7 +80,7 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << expr::ExprSetDepth(depth);
     // intentionally exclude Dump stream from this list
   }
-  else if (key == options::defaultDagThresh.name)
+  else if (key == options::expr::defaultDagThresh__name)
   {
     int dag = (*d_options)[options::defaultDagThresh];
     Debug.getStream() << expr::ExprDag(dag);
@@ -91,12 +91,12 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << expr::ExprDag(dag);
     Dump.getStream() << expr::ExprDag(dag);
   }
-  else if (key == options::dumpModeString.name)
+  else if (key == options::smt::dumpModeString__name)
   {
     const std::string& value = (*d_options)[options::dumpModeString];
     Dump.setDumpFromString(value);
   }
-  else if (key == options::printSuccess.name)
+  else if (key == options::base::printSuccess__name)
   {
     bool value = (*d_options)[options::printSuccess];
     Debug.getStream() << Command::printsuccess(value);
@@ -107,15 +107,15 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << Command::printsuccess(value);
     *options::out() << Command::printsuccess(value);
   }
-  else if (key == options::regularChannelName.name)
+  else if (key == options::smt::regularChannelName__name)
   {
     d_managedRegularChannel.set(options::regularChannelName());
   }
-  else if (key == options::diagnosticChannelName.name)
+  else if (key == options::smt::diagnosticChannelName__name)
   {
     d_managedDiagnosticChannel.set(options::diagnosticChannelName());
   }
-  else if (key == options::dumpToFileName.name)
+  else if (key == options::smt::dumpToFileName__name)
   {
     d_managedDumpChannel.set(options::dumpToFileName());
   }