Fix output of --trace=help. (#1500)

3 files changed, 102 insertions, 107 deletions

diff --git a/src/options/base_options b/src/options/base_options
index 7346641c7..7098e1f5d 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -199,9 +199,9 @@ option parseOnly parse-only --parse-only bool :read-write
 option preprocessOnly preprocess-only --preprocess-only bool
  exit after preprocessing input
 
-option - trace -t --trace=TAG argument :handler addTraceTag
+option - trace -t --trace=TAG argument :handler enableTraceTag
  trace something (e.g. -t pushpop), can repeat
-option - debug -d --debug=TAG argument :handler addDebugTag
+option - debug -d --debug=TAG argument :handler enableDebugTag
  debug something (e.g. -d arith), can repeat
 
 option printSuccess print-success --print-success bool :notify notifyPrintSuccess
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 583f79d2d..e8a243448 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1546,38 +1546,115 @@ void OptionsHandler::showConfiguration(std::string option) {
   exit(0);
 }
 
-void OptionsHandler::showDebugTags(std::string option) {
-  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
-    std::cout << "available tags:";
-    unsigned ntags = Configuration::getNumDebugTags();
-    char const* const* tags = Configuration::getDebugTags();
-    for(unsigned i = 0; i < ntags; ++ i) {
-      std::cout << tags[i];
-    }
-    std::cout << std::endl;
-  } else if(! Configuration::isDebugBuild()) {
+static void printTags(unsigned ntags, char const* const* tags)
+{
+  std::cout << "available tags:";
+  for (unsigned i = 0; i < ntags; ++ i)
+  {
+    std::cout << "  " << tags[i] << std::endl;
+  }
+  std::cout << std::endl;
+}
+
+void OptionsHandler::showDebugTags(std::string option)
+{
+  if (!Configuration::isDebugBuild())
+  {
     throw OptionException("debug tags not available in non-debug builds");
-  } else {
+  }
+  else if (!Configuration::isTracingBuild())
+  {
     throw OptionException("debug tags not available in non-tracing builds");
   }
+  printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
   exit(0);
 }
 
-void OptionsHandler::showTraceTags(std::string option) {
-  if(Configuration::isTracingBuild()) {
-    std::cout << "available tags:" << std::endl;
-    unsigned ntags = Configuration::getNumTraceTags();
-    char const* const* tags = Configuration::getTraceTags();
-    for (unsigned i = 0; i < ntags; ++ i) {
-      std::cout << "  " << tags[i] << std::endl;
-    }
-    std::cout << std::endl;
-  } else {
+void OptionsHandler::showTraceTags(std::string option)
+{
+  if (!Configuration::isTracingBuild())
+  {
     throw OptionException("trace tags not available in non-tracing build");
   }
+  printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
   exit(0);
 }
 
+static std::string suggestTags(char const* const* validTags,
+                               std::string inputTag,
+                               char const* const* additionalTags)
+{
+  DidYouMean didYouMean;
+
+  const char* opt;
+  for (size_t i = 0; (opt = validTags[i]) != nullptr; ++i)
+  {
+    didYouMean.addWord(validTags[i]);
+  }
+  if (additionalTags != nullptr)
+  {
+    for (size_t i = 0; (opt = additionalTags[i]) != nullptr; ++i)
+    {
+      didYouMean.addWord(additionalTags[i]);
+    }
+  }
+
+  return didYouMean.getMatchAsString(inputTag);
+}
+
+void OptionsHandler::enableTraceTag(std::string option, std::string optarg)
+{
+  if(!Configuration::isTracingBuild())
+  {
+    throw OptionException("trace tags not available in non-tracing builds");
+  }
+  else if(!Configuration::isTraceTag(optarg.c_str()))
+  {
+    if (optarg == "help")
+    {
+      printTags(
+          Configuration::getNumTraceTags(), Configuration::getTraceTags());
+      exit(0);
+    }
+
+    throw OptionException(
+        std::string("trace tag ") + optarg + std::string(" not available.")
+        + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
+  }
+  Trace.on(optarg);
+}
+
+void OptionsHandler::enableDebugTag(std::string option, std::string optarg)
+{
+  if (!Configuration::isDebugBuild())
+  {
+    throw OptionException("debug tags not available in non-debug builds");
+  }
+  else if (!Configuration::isTracingBuild())
+  {
+    throw OptionException("debug tags not available in non-tracing builds");
+  }
+
+  if (!Configuration::isDebugTag(optarg.c_str())
+      && !Configuration::isTraceTag(optarg.c_str()))
+  {
+    if (optarg == "help")
+    {
+      printTags(
+          Configuration::getNumDebugTags(), Configuration::getDebugTags());
+      exit(0);
+    }
+
+    throw OptionException(std::string("debug tag ") + optarg
+                          + std::string(" not available.")
+                          + suggestTags(Configuration::getDebugTags(),
+                                        optarg,
+                                        Configuration::getTraceTags()));
+  }
+  Debug.on(optarg);
+  Trace.on(optarg);
+}
+
 
 OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "help") {
@@ -1651,83 +1728,5 @@ void OptionsHandler::decreaseVerbosity(std::string option) {
 }
 
 
-void OptionsHandler::addTraceTag(std::string option, std::string optarg) {
-  if(Configuration::isTracingBuild()) {
-    if(!Configuration::isTraceTag(optarg.c_str())) {
-
-      if(optarg == "help") {
-        std::cout << "available tags:";
-        unsigned ntags = Configuration::getNumTraceTags();
-        char const* const* tags = Configuration::getTraceTags();
-        for(unsigned i = 0; i < ntags; ++ i) {
-          std::cout << tags[i];
-        }
-        std::cout << std::endl;
-        exit(0);
-      }
-
-      throw OptionException(std::string("trace tag ") + optarg +
-                            std::string(" not available.") +
-                            suggestTags(Configuration::getTraceTags(), optarg) );
-    }
-  } else {
-    throw OptionException("trace tags not available in non-tracing builds");
-  }
-  Trace.on(optarg);
-}
-
-void OptionsHandler::addDebugTag(std::string option, std::string optarg) {
-  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
-    if(!Configuration::isDebugTag(optarg.c_str()) &&
-       !Configuration::isTraceTag(optarg.c_str())) {
-
-      if(optarg == "help") {
-        std::cout << "available tags:";
-        unsigned ntags = Configuration::getNumDebugTags();
-        char const* const* tags = Configuration::getDebugTags();
-        for(unsigned i = 0; i < ntags; ++ i) {
-          std::cout << tags[i];
-        }
-        std::cout << std::endl;
-        exit(0);
-      }
-
-      throw OptionException(std::string("debug tag ") + optarg +
-                            std::string(" not available.") +
-                            suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );
-    }
-  } else if(! Configuration::isDebugBuild()) {
-    throw OptionException("debug tags not available in non-debug builds");
-  } else {
-    throw OptionException("debug tags not available in non-tracing builds");
-  }
-  Debug.on(optarg);
-  Trace.on(optarg);
-}
-
-
-
-
-std::string OptionsHandler::suggestTags(char const* const* validTags, std::string inputTag,
-                                           char const* const* additionalTags)
-{
-  DidYouMean didYouMean;
-
-  const char* opt;
-  for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) {
-    didYouMean.addWord(validTags[i]);
-  }
-  if(additionalTags != NULL) {
-    for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) {
-      didYouMean.addWord(additionalTags[i]);
-    }
-  }
-
-  return  didYouMean.getMatchAsString(inputTag);
-}
-
-
-
-
 }/* CVC4::options namespace */
 }/* CVC4 namespace */
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index eef4c9b61..23a6be501 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -188,16 +188,12 @@ public:
   void decreaseVerbosity(std::string option);
   OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException);
   InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException);
-  void addTraceTag(std::string option, std::string optarg);
-  void addDebugTag(std::string option, std::string optarg);
+  void enableTraceTag(std::string option, std::string optarg);
+  void enableDebugTag(std::string option, std::string optarg);
   void notifyPrintSuccess(std::string option);
 
  private:
 
-  /* Helper utilities */
-  static std::string suggestTags(char const* const* validTags, std::string inputTag,
-                                 char const* const* additionalTags = NULL);
-
   /** Pointer to the containing Options object.*/
   Options* d_options;