Remove options::X__name (#7414)

This PR removes the static strings options::module::X__name that hold the primary long option name. We used them to figure out which option an handler function was called on for certain handler functions. This was always a weird way, and the past refactorings have eliminated all these cases.
This also removes the need to the two arguments option and flag to all option handlers.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 57f8b64e63a36041d61728583939fd858c314acd..badfd59f01be6f9de907984731eb44d6c3ede32b 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -295,15 +295,12 @@ def _set_handlers(option):
     optname = option.long_name if option.long else ""
     if option.handler:
         if option.type == 'void':
-            return 'opts.handler().{}("{}", name)'.format(
-                option.handler, optname)
+            return 'opts.handler().{}(name)'.format(option.handler)
         else:
-            return 'opts.handler().{}("{}", name, optionarg)'.format(
-                option.handler, optname)
+            return 'opts.handler().{}(name, optionarg)'.format(option.handler)
     elif option.mode:
         return 'stringTo{}(optionarg)'.format(option.type)
-    return 'handlers::handleOption<{}>("{}", name, optionarg)'.format(
-        option.type, optname)
+    return 'handlers::handleOption<{}>(name, optionarg)'.format(option.type)
 
 
 def _set_predicates(option):
@@ -315,14 +312,14 @@ def _set_predicates(option):
     res = []
     if option.minimum:
         res.append(
-            'opts.handler().checkMinimum("{}", name, value, static_cast<{}>({}));'
-            .format(optname, option.type, option.minimum))
+            'opts.handler().checkMinimum(name, value, static_cast<{}>({}));'
+            .format(option.type, option.minimum))
     if option.maximum:
         res.append(
-            'opts.handler().checkMaximum("{}", name, value, static_cast<{}>({}));'
-            .format(optname, option.type, option.maximum))
+            'opts.handler().checkMaximum(name, value, static_cast<{}>({}));'
+            .format(option.type, option.maximum))
     res += [
-        'opts.handler().{}("{}", name, value);'.format(x, optname)
+        'opts.handler().{}(name, value);'.format(x)
         for x in option.predicates
     ]
     return res
@@ -361,7 +358,7 @@ def generate_set_impl(modules):
                                    name=option.name,
                                    handler=_set_handlers(option)))
         elif option.handler:
-            h = '  opts.handler().{handler}("{smtname}", name'
+            h = '  opts.handler().{handler}(name'
             if option.type not in ['bool', 'void']:
                 h += ', optionarg'
             h += ');'
@@ -471,15 +468,6 @@ def generate_module_wrapper_functions(module):
     return '\n'.join(res)
 
 
-def generate_module_option_names(module):
-    relevant = [
-        o for o in module.options
-        if not (o.name is None or o.long_name is None)
-    ]
-    return concat_format(
-        'static constexpr const char* {name}__name = "{long_name}";', relevant)
-
-
 ################################################################################
 # for options/<module>.cpp
 
@@ -842,7 +830,6 @@ def codegen_module(module, dst_dir, tpls):
         'modes_decl': generate_module_mode_decl(module),
         'holder_decl': generate_module_holder_decl(module),
         'wrapper_functions': generate_module_wrapper_functions(module),
-        'option_names': generate_module_option_names(module),
         # module source
         'header': module.header,
         'modes_impl': generate_module_mode_impl(module),

diff --git a/src/options/module_template.h b/src/options/module_template.h
index d9b591f1110b929a583579063ae875d13242b9b4..c613c1cba78bd9026bcfede1609e5bcc7b0037b6 100644 (file)
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -52,13 +52,6 @@ ${holder_decl}$
 ${wrapper_functions}$
 // clang-format on
 
-namespace ${id}$
-{
-// clang-format off
-${option_names}$
-// clang-format on
-}
-
 }  // namespace cvc5::options
 
 #endif /* CVC5__OPTIONS__${id_cap}$_H */

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index ec6c831e437770797f1fe083bfa0c1bdec293671..fe0e1d96194955f1990eabe8e5228420f08b15be 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -71,9 +71,7 @@ std::string suggestTags(const std::vector<std::string>& validTags,
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-void OptionsHandler::setErrStream(const std::string& option,
-                                  const std::string& flag,
-                                  const ManagedErr& me)
+void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me)
 {
   Debug.setStream(me);
   Warning.setStream(me);
@@ -83,8 +81,7 @@ void OptionsHandler::setErrStream(const std::string& option,
   Trace.setStream(me);
 }
 
-Language OptionsHandler::stringToLanguage(const std::string& option,
-                                          const std::string& flag,
+Language OptionsHandler::stringToLanguage(const std::string& flag,
                                           const std::string& optarg)
 {
   if (optarg == "help")
@@ -114,16 +111,14 @@ Languages currently supported as arguments to the --output-lang option:
   }
   catch (OptionException& oe)
   {
-    throw OptionException("Error in " + option + ": " + oe.getMessage()
+    throw OptionException("Error in " + flag + ": " + oe.getMessage()
                           + "\nTry --lang help");
   }
 
   Unreachable();
 }
 
-void OptionsHandler::languageIsNotAST(const std::string& option,
-                                      const std::string& flag,
-                                      Language lang)
+void OptionsHandler::languageIsNotAST(const std::string& flag, Language lang)
 {
   if (lang == Language::LANG_AST)
   {
@@ -131,16 +126,12 @@ void OptionsHandler::languageIsNotAST(const std::string& option,
   }
 }
 
-void OptionsHandler::applyOutputLanguage(const std::string& option,
-                                         const std::string& flag,
-                                         Language lang)
+void OptionsHandler::applyOutputLanguage(const std::string& flag, Language lang)
 {
   d_options->base.out << language::SetLanguage(lang);
 }
 
-void OptionsHandler::setVerbosity(const std::string& option,
-                                  const std::string& flag,
-                                  int value)
+void OptionsHandler::setVerbosity(const std::string& flag, int value)
 {
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
@@ -170,23 +161,19 @@ void OptionsHandler::setVerbosity(const std::string& option,
   }
 }
 
-void OptionsHandler::decreaseVerbosity(const std::string& option,
-                                       const std::string& flag)
+void OptionsHandler::decreaseVerbosity(const std::string& flag)
 {
   d_options->base.verbosity -= 1;
-  setVerbosity(option, flag, d_options->base.verbosity);
+  setVerbosity(flag, d_options->base.verbosity);
 }
 
-void OptionsHandler::increaseVerbosity(const std::string& option,
-                                       const std::string& flag)
+void OptionsHandler::increaseVerbosity(const std::string& flag)
 {
   d_options->base.verbosity += 1;
-  setVerbosity(option, flag, d_options->base.verbosity);
+  setVerbosity(flag, d_options->base.verbosity);
 }
 
-void OptionsHandler::setStats(const std::string& option,
-                              const std::string& flag,
-                              bool value)
+void OptionsHandler::setStats(const std::string& flag, bool value)
 {
 #ifndef CVC5_STATISTICS_ON
   if (value)
@@ -206,9 +193,7 @@ void OptionsHandler::setStats(const std::string& option,
   }
 }
 
-void OptionsHandler::setStatsDetail(const std::string& option,
-                              const std::string& flag,
-                              bool value)
+void OptionsHandler::setStatsDetail(const std::string& flag, bool value)
 {
 #ifndef CVC5_STATISTICS_ON
   if (value)
@@ -226,8 +211,7 @@ void OptionsHandler::setStatsDetail(const std::string& option,
   }
 }
 
-void OptionsHandler::enableTraceTag(const std::string& option,
-                                    const std::string& flag,
+void OptionsHandler::enableTraceTag(const std::string& flag,
                                     const std::string& optarg)
 {
   if(!Configuration::isTracingBuild())
@@ -249,8 +233,7 @@ void OptionsHandler::enableTraceTag(const std::string& option,
   Trace.on(optarg);
 }
 
-void OptionsHandler::enableDebugTag(const std::string& option,
-                                    const std::string& flag,
+void OptionsHandler::enableDebugTag(const std::string& flag,
                                     const std::string& optarg)
 {
   if (!Configuration::isDebugBuild())
@@ -281,17 +264,14 @@ void OptionsHandler::enableDebugTag(const std::string& option,
   Trace.on(optarg);
 }
 
-void OptionsHandler::enableOutputTag(const std::string& option,
-                                     const std::string& flag,
+void OptionsHandler::enableOutputTag(const std::string& flag,
                                      const std::string& optarg)
 {
   d_options->base.outputTagHolder.set(
       static_cast<size_t>(stringToOutputTag(optarg)));
 }
 
-void OptionsHandler::setPrintSuccess(const std::string& option,
-                                     const std::string& flag,
-                                     bool value)
+void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
 {
   Debug.getStream() << Command::printsuccess(value);
   Trace.getStream() << Command::printsuccess(value);
@@ -302,21 +282,18 @@ void OptionsHandler::setPrintSuccess(const std::string& option,
   *d_options->base.out << Command::printsuccess(value);
 }
 
-void OptionsHandler::setResourceWeight(const std::string& option,
-                                       const std::string& flag,
+void OptionsHandler::setResourceWeight(const std::string& flag,
                                        const std::string& optarg)
 {
   d_options->base.resourceWeightHolder.emplace_back(optarg);
 }
 
-void OptionsHandler::abcEnabledBuild(const std::string& option,
-                                     const std::string& flag,
-                                     bool value)
+void OptionsHandler::abcEnabledBuild(const std::string& flag, bool value)
 {
 #ifndef CVC5_USE_ABC
   if(value) {
     std::stringstream ss;
-    ss << "option `" << option
+    ss << "option `" << flag
        << "' requires an abc-enabled build of cvc5; this binary was not built "
           "with abc support";
     throw OptionException(ss.str());
@@ -324,14 +301,13 @@ void OptionsHandler::abcEnabledBuild(const std::string& option,
 #endif /* CVC5_USE_ABC */
 }
 
-void OptionsHandler::abcEnabledBuild(const std::string& option,
-                                     const std::string& flag,
+void OptionsHandler::abcEnabledBuild(const std::string& flag,
                                      const std::string& value)
 {
 #ifndef CVC5_USE_ABC
   if(!value.empty()) {
     std::stringstream ss;
-    ss << "option `" << option
+    ss << "option `" << flag
        << "' requires an abc-enabled build of cvc5; this binary was not built "
           "with abc support";
     throw OptionException(ss.str());
@@ -339,15 +315,13 @@ void OptionsHandler::abcEnabledBuild(const std::string& option,
 #endif /* CVC5_USE_ABC */
 }
 
-void OptionsHandler::checkBvSatSolver(const std::string& option,
-                                      const std::string& flag,
-                                      SatSolverMode m)
+void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m)
 {
   if (m == SatSolverMode::CRYPTOMINISAT
       && !Configuration::isBuiltWithCryptominisat())
   {
     std::stringstream ss;
-    ss << "option `" << option
+    ss << "option `" << flag
        << "' requires a CryptoMiniSat build of cvc5; this binary was not built "
           "with CryptoMiniSat support";
     throw OptionException(ss.str());
@@ -356,7 +330,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
   if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
   {
     std::stringstream ss;
-    ss << "option `" << option
+    ss << "option `" << flag
        << "' requires a Kissat build of cvc5; this binary was not built with "
           "Kissat support";
     throw OptionException(ss.str());
@@ -394,9 +368,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
   }
 }
 
-void OptionsHandler::setBitblastAig(const std::string& option,
-                                    const std::string& flag,
-                                    bool arg)
+void OptionsHandler::setBitblastAig(const std::string& flag, bool arg)
 {
   if(arg) {
     if (d_options->bv.bitblastModeWasSetByUser) {
@@ -410,9 +382,7 @@ void OptionsHandler::setBitblastAig(const std::string& option,
   }
 }
 
-void OptionsHandler::setDefaultExprDepth(const std::string& option,
-                                         const std::string& flag,
-                                         int depth)
+void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
 {
   Debug.getStream() << expr::ExprSetDepth(depth);
   Trace.getStream() << expr::ExprSetDepth(depth);
@@ -422,9 +392,7 @@ void OptionsHandler::setDefaultExprDepth(const std::string& option,
   Warning.getStream() << expr::ExprSetDepth(depth);
 }
 
-void OptionsHandler::setDefaultDagThresh(const std::string& option,
-                                         const std::string& flag,
-                                         int dag)
+void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
 {
   Debug.getStream() << expr::ExprDag(dag);
   Trace.getStream() << expr::ExprDag(dag);
@@ -448,8 +416,7 @@ static void print_config_cond(const char* str, bool cond = false)
   print_config(str, cond ? "yes" : "no");
 }
 
-void OptionsHandler::showConfiguration(const std::string& option,
-                                       const std::string& flag)
+void OptionsHandler::showConfiguration(const std::string& flag)
 {
   std::cout << Configuration::about() << std::endl;
 
@@ -498,22 +465,19 @@ void OptionsHandler::showConfiguration(const std::string& option,
   std::exit(0);
 }
 
-void OptionsHandler::showCopyright(const std::string& option,
-                                   const std::string& flag)
+void OptionsHandler::showCopyright(const std::string& flag)
 {
   std::cout << Configuration::copyright() << std::endl;
   std::exit(0);
 }
 
-void OptionsHandler::showVersion(const std::string& option,
-                                 const std::string& flag)
+void OptionsHandler::showVersion(const std::string& flag)
 {
   d_options->base.out << Configuration::about() << std::endl;
   std::exit(0);
 }
 
-void OptionsHandler::showDebugTags(const std::string& option,
-                                   const std::string& flag)
+void OptionsHandler::showDebugTags(const std::string& flag)
 {
   if (!Configuration::isDebugBuild())
   {
@@ -527,8 +491,7 @@ void OptionsHandler::showDebugTags(const std::string& option,
   std::exit(0);
 }
 
-void OptionsHandler::showTraceTags(const std::string& option,
-                                   const std::string& flag)
+void OptionsHandler::showTraceTags(const std::string& flag)
 {
   if (!Configuration::isTracingBuild())
   {
@@ -538,8 +501,7 @@ void OptionsHandler::showTraceTags(const std::string& option,
   std::exit(0);
 }
 
-void OptionsHandler::setDumpMode(const std::string& option,
-                                 const std::string& flag,
+void OptionsHandler::setDumpMode(const std::string& flag,
                                  const std::string& optarg)
 {
 #ifdef CVC5_DUMPING
@@ -550,8 +512,7 @@ void OptionsHandler::setDumpMode(const std::string& option,
 #endif /* CVC5_DUMPING */
 }
 
-void OptionsHandler::setDumpStream(const std::string& option,
-                                   const std::string& flag,
+void OptionsHandler::setDumpStream(const std::string& flag,
                                    const ManagedOut& mo)
 {
 #ifdef CVC5_DUMPING

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index c3cd8c358ab9a8bfca92505f12da996889bdfe06..077e2119dc85b642feb1c281910c727625288182 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -46,10 +46,7 @@ class OptionsHandler
   OptionsHandler(Options* options);
 
   template <typename T>
-  void checkMinimum(const std::string& option,
-                    const std::string& flag,
-                    T value,
-                    T minimum) const
+  void checkMinimum(const std::string& flag, T value, T minimum) const
   {
     if (value < minimum)
     {
@@ -61,10 +58,7 @@ class OptionsHandler
     }
   }
   template <typename T>
-  void checkMaximum(const std::string& option,
-                    const std::string& flag,
-                    T value,
-                    T maximum) const
+  void checkMaximum(const std::string& flag, T value, T maximum) const
   {
     if (value > maximum)
     {
@@ -78,107 +72,69 @@ class OptionsHandler
 
   /******************************* base options *******************************/
   /** Apply the error output stream to the different output channels */
-  void setErrStream(const std::string& option,
-                    const std::string& flag,
-                    const ManagedErr& me);
+  void setErrStream(const std::string& flag, const ManagedErr& me);
 
   /** Convert option value to Language enum */
-  Language stringToLanguage(const std::string& option,
-                            const std::string& flag,
-                            const std::string& optarg);
+  Language stringToLanguage(const std::string& flag, const std::string& optarg);
   /** Check that lang is not LANG_AST (not allowed as input language) */
-  void languageIsNotAST(const std::string& option,
-                        const std::string& flag,
-                        Language lang);
+  void languageIsNotAST(const std::string& flag, Language lang);
   /** Apply the output language to the default output stream */
-  void applyOutputLanguage(const std::string& option,
-                           const std::string& flag,
-                           Language lang);
+  void applyOutputLanguage(const std::string& flag, Language lang);
   /** Apply verbosity to the different output channels */
-  void setVerbosity(const std::string& option,
-                    const std::string& flag,
-                    int value);
+  void setVerbosity(const std::string& flag, int value);
   /** Decrease verbosity and call setVerbosity */
-  void decreaseVerbosity(const std::string& option, const std::string& flag);
+  void decreaseVerbosity(const std::string& flag);
   /** Increase verbosity and call setVerbosity */
-  void increaseVerbosity(const std::string& option, const std::string& flag);
+  void increaseVerbosity(const std::string& flag);
   /** If statistics are disabled, disable statistics sub-options */
-  void setStats(const std::string& option, const std::string& flag, bool value);
+  void setStats(const std::string& flag, bool value);
   /** If statistics sub-option is disabled, enable statistics */
-  void setStatsDetail(const std::string& option,
-                      const std::string& flag,
-                      bool value);
+  void setStatsDetail(const std::string& flag, bool value);
   /** Enable a particular trace tag */
-  void enableTraceTag(const std::string& option,
-                      const std::string& flag,
-                      const std::string& optarg);
+  void enableTraceTag(const std::string& flag, const std::string& optarg);
   /** Enable a particular debug tag */
-  void enableDebugTag(const std::string& option,
-                      const std::string& flag,
-                      const std::string& optarg);
+  void enableDebugTag(const std::string& flag, const std::string& optarg);
   /** Enable a particular output tag */
-  void enableOutputTag(const std::string& option,
-                       const std::string& flag,
-                       const std::string& optarg);
+  void enableOutputTag(const std::string& flag, const std::string& optarg);
   /** Apply print success flag to the different output channels */
-  void setPrintSuccess(const std::string& option,
-                       const std::string& flag,
-                       bool value);
+  void setPrintSuccess(const std::string& flag, bool value);
   /** Pass the resource weight specification to the resource manager */
-  void setResourceWeight(const std::string& option,
-                         const std::string& flag,
-                         const std::string& optarg);
+  void setResourceWeight(const std::string& flag, const std::string& optarg);
 
   /******************************* bv options *******************************/
 
   /** Check that abc is enabled */
-  void abcEnabledBuild(const std::string& option,
-                       const std::string& flag,
-                       bool value);
+  void abcEnabledBuild(const std::string& flag, bool value);
   /** Check that abc is enabled */
-  void abcEnabledBuild(const std::string& option,
-                       const std::string& flag,
-                       const std::string& value);
+  void abcEnabledBuild(const std::string& flag, const std::string& value);
   /** Check that the sat solver mode is compatible with other bv options */
-  void checkBvSatSolver(const std::string& option,
-                        const std::string& flag,
-                        SatSolverMode m);
+  void checkBvSatSolver(const std::string& flag, SatSolverMode m);
   /** Check that we use eager bitblasting for aig */
-  void setBitblastAig(const std::string& option,
-                      const std::string& flag,
-                      bool arg);
+  void setBitblastAig(const std::string& flag, bool arg);
 
   /******************************* expr options *******************************/
   /** Set ExprSetDepth on all output streams */
-  void setDefaultExprDepth(const std::string& option,
-                           const std::string& flag,
-                           int depth);
+  void setDefaultExprDepth(const std::string& flag, int depth);
   /** Set ExprDag on all output streams */
-  void setDefaultDagThresh(const std::string& option,
-                           const std::string& flag,
-                           int dag);
+  void setDefaultDagThresh(const std::string& flag, int dag);
 
   /******************************* main options *******************************/
   /** Show the solver build configuration and exit */
-  void showConfiguration(const std::string& option, const std::string& flag);
+  void showConfiguration(const std::string& flag);
   /** Show copyright information and exit */
-  void showCopyright(const std::string& option, const std::string& flag);
+  void showCopyright(const std::string& flag);
   /** Show version information and exit */
-  void showVersion(const std::string& option, const std::string& flag);
+  void showVersion(const std::string& flag);
   /** Show all debug tags and exit */
-  void showDebugTags(const std::string& option, const std::string& flag);
+  void showDebugTags(const std::string& flag);
   /** Show all trace tags and exit */
-  void showTraceTags(const std::string& option, const std::string& flag);
+  void showTraceTags(const std::string& flag);
 
   /******************************* smt options *******************************/
   /** Set a mode on the dumping output stream. */
-  void setDumpMode(const std::string& option,
-                   const std::string& flag,
-                   const std::string& optarg);
+  void setDumpMode(const std::string& flag, const std::string& optarg);
   /** Set the dumping output stream. */
-  void setDumpStream(const std::string& option,
-                     const std::string& flag,
-                     const ManagedOut& mo);
+  void setDumpStream(const std::string& flag, const ManagedOut& mo);
 
  private:
   /** Pointer to the containing Options object.*/

diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index df61249af3be617ef8a7e69de03465d84e4ad7d8..a6ab6efde4e2ad0f8333ae76395a175c99c74b86 100644 (file)
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -86,9 +86,7 @@ namespace cvc5::options
 
   /** Default handler that triggers a compiler error */
   template <typename T>
-  T handleOption(const std::string& option,
-                 const std::string& flag,
-                 const std::string& optionarg)
+  T handleOption(const std::string& flag, const std::string& optionarg)
   {
     T::unsupported_handleOption_specialization;
     return *static_cast<T*>(nullptr);
@@ -96,17 +94,14 @@ namespace cvc5::options
 
   /** Handle a string option by returning it as is. */
   template <>
-  std::string handleOption<std::string>(const std::string& option,
-                                        const std::string& flag,
+  std::string handleOption<std::string>(const std::string& flag,
                                         const std::string& optionarg)
   {
     return optionarg;
   }
   /** Handle a bool option, recognizing "true" or "false". */
   template <>
-  bool handleOption<bool>(const std::string& option,
-                          const std::string& flag,
-                          const std::string& optionarg)
+  bool handleOption<bool>(const std::string& flag, const std::string& optionarg)
   {
     if (optionarg == "true")
     {
@@ -122,8 +117,7 @@ namespace cvc5::options
 
   /** Handle a double option, using `parseNumber` with `std::stod`. */
   template <>
-  double handleOption<double>(const std::string& option,
-                              const std::string& flag,
+  double handleOption<double>(const std::string& flag,
                               const std::string& optionarg)
   {
     return parseNumber<double>(
@@ -135,8 +129,7 @@ namespace cvc5::options
 
   /** Handle a int64_t option, using `parseNumber` with `std::stoll`. */
   template <>
-  int64_t handleOption<int64_t>(const std::string& option,
-                                const std::string& flag,
+  int64_t handleOption<int64_t>(const std::string& flag,
                                 const std::string& optionarg)
   {
     return parseNumber<int64_t>(
@@ -148,8 +141,7 @@ namespace cvc5::options
 
   /** Handle a uint64_t option, using `parseNumber` with `std::stoull`. */
   template <>
-  uint64_t handleOption<uint64_t>(const std::string& option,
-                                  const std::string& flag,
+  uint64_t handleOption<uint64_t>(const std::string& flag,
                                   const std::string& optionarg)
   {
     return parseNumber<uint64_t>(
@@ -161,8 +153,7 @@ namespace cvc5::options
 
   /** Handle a ManagedIn option. */
   template <>
-  ManagedIn handleOption<ManagedIn>(const std::string& option,
-                                    const std::string& flag,
+  ManagedIn handleOption<ManagedIn>(const std::string& flag,
                                     const std::string& optionarg)
   {
     ManagedIn res;
@@ -172,8 +163,7 @@ namespace cvc5::options
 
   /** Handle a ManagedErr option. */
   template <>
-  ManagedErr handleOption<ManagedErr>(const std::string& option,
-                                      const std::string& flag,
+  ManagedErr handleOption<ManagedErr>(const std::string& flag,
                                       const std::string& optionarg)
   {
     ManagedErr res;
@@ -183,8 +173,7 @@ namespace cvc5::options
 
   /** Handle a ManagedOut option. */
   template <>
-  ManagedOut handleOption<ManagedOut>(const std::string& option,
-                                      const std::string& flag,
+  ManagedOut handleOption<ManagedOut>(const std::string& flag,
                                       const std::string& optionarg)
   {
     ManagedOut res;

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6fdd45c4e7a336e37b8bcaf6eed4803a6d4aca17..7c813cee0ecf332bafb5fd088038b75bcaa82a8f 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -836,15 +836,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
     if (opts.arith.nlCadWasSetByUser)
     {
-      std::stringstream ss;
-      ss << "Cannot use " << options::arith::nlCad__name
-         << " without configuring with --poly.";
-      throw OptionException(ss.str());
+      throw OptionException(
+          "Cannot use --nl-cad without configuring with --poly.");
     }
     else
     {
-      Notice() << "Cannot use --" << options::arith::nlCad__name
-               << " without configuring with --poly." << std::endl;
+      Notice() << "Cannot use --nl-cad without configuring with --poly."
+               << std::endl;
       opts.arith.nlCad = false;
       opts.arith.nlExt = options::NlExtMode::FULL;
     }