Refactor tag suggestion mechanism (#7199)

This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead.

5 files changed, 50 insertions, 107 deletions

diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
index 43e183b99..86cc94053 100644
--- a/src/base/collect_tags.py
+++ b/src/base/collect_tags.py
@@ -44,10 +44,16 @@ def collect_tags(basedir):
 def write_file(filename, type, tags):
     """Render the header file to the given filename."""
     with open(filename, 'w') as out:
-        out.write('static char const* const {}_tags[] = {{\n'.format(type))
+        out.write('static const std::vector<std::string> {}_tags = {{\n'.format(type))
+        if type == 'Debug':
+            out.write('#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)\n')
+        elif type == 'Trace':
+            out.write('#if defined(CVC5_TRACING)\n')
+        else:
+            raise 'type is neither Debug nor Trace: {}'.format(type)
         for t in tags:
             out.write('"{}",\n'.format(t))
-        out.write('nullptr\n')
+        out.write('#endif\n')
         out.write('};\n')
 
 
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index a370a0c47..b4f6cae7f 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -18,20 +18,15 @@
 #include <stdlib.h>
 #include <string.h>
 
+#include <algorithm>
 #include <sstream>
 #include <string>
 
+#include "base/Debug_tags.h"
+#include "base/Trace_tags.h"
 #include "base/configuration_private.h"
 #include "base/cvc5config.h"
 
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-#  include "base/Debug_tags.h"
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-
-#ifdef CVC5_TRACING
-#  include "base/Trace_tags.h"
-#endif /* CVC5_TRACING */
-
 using namespace std;
 
 namespace cvc5 {
@@ -253,70 +248,26 @@ bool Configuration::isBuiltWithPoly()
   return IS_POLY_BUILD;
 }
 
-unsigned Configuration::getNumDebugTags() {
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-  /* -1 because a NULL pointer is inserted as the last value */
-  return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1;
-#else  /* CVC5_DEBUG && CVC5_TRACING */
-  return 0;
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-}
-
-char const* const* Configuration::getDebugTags() {
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
+const std::vector<std::string>& Configuration::getDebugTags()
+{
   return Debug_tags;
-#else  /* CVC5_DEBUG && CVC5_TRACING */
-  static char const* no_tags[] = { NULL };
-  return no_tags;
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-}
-
-int strcmpptr(const char **s1, const char **s2){
-  return strcmp(*s1,*s2);
-}
-
-bool Configuration::isDebugTag(char const *tag){
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-  unsigned ntags = getNumDebugTags();
-  char const* const* tags = getDebugTags();
-  for (unsigned i = 0; i < ntags; ++ i) {
-    if (strcmp(tag, tags[i]) == 0) {
-      return true;
-    }
-  }
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-  return false;
 }
 
-unsigned Configuration::getNumTraceTags() {
-#if CVC5_TRACING
-  /* -1 because a NULL pointer is inserted as the last value */
-  return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1;
-#else  /* CVC5_TRACING */
-  return 0;
-#endif /* CVC5_TRACING */
+bool Configuration::isDebugTag(const std::string& tag)
+{
+  return std::find(Debug_tags.begin(), Debug_tags.end(), tag)
+         != Debug_tags.end();
 }
 
-char const* const* Configuration::getTraceTags() {
-#if CVC5_TRACING
+const std::vector<std::string>& Configuration::getTraceTags()
+{
   return Trace_tags;
-#else  /* CVC5_TRACING */
-  static char const* no_tags[] = { NULL };
-  return no_tags;
-#endif /* CVC5_TRACING */
 }
 
-bool Configuration::isTraceTag(char const * tag){
-#if CVC5_TRACING
-  unsigned ntags = getNumTraceTags();
-  char const* const* tags = getTraceTags();
-  for (unsigned i = 0; i < ntags; ++ i) {
-    if (strcmp(tag, tags[i]) == 0) {
-      return true;
-    }
-  }
-#endif /* CVC5_TRACING */
-  return false;
+bool Configuration::isTraceTag(const std::string& tag)
+{
+  return std::find(Trace_tags.begin(), Trace_tags.end(), tag)
+         != Trace_tags.end();
 }
 
 bool Configuration::isGitBuild() {
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 71c79c22e..01579526d 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -20,6 +20,7 @@
 #define CVC5__CONFIGURATION_H
 
 #include <string>
+#include <vector>
 
 #include "cvc5_export.h"
 
@@ -111,19 +112,15 @@ public:
 
   static bool isBuiltWithPoly();
 
-  /* Return the number of debug tags */
-  static unsigned getNumDebugTags();
   /* Return a sorted array of the debug tags name */
-  static char const* const* getDebugTags();
+  static const std::vector<std::string>& getDebugTags();
   /* Test if the given argument is a known debug tag name */
-  static bool isDebugTag(char const *);
+  static bool isDebugTag(const std::string& tag);
 
-  /* Return the number of trace tags */
-  static unsigned getNumTraceTags();
   /* Return a sorted array of the trace tags name */
-  static char const* const* getTraceTags();
+  static const std::vector<std::string>& getTraceTags();
   /* Test if the given argument is a known trace tag name */
-  static bool isTraceTag(char const *);
+  static bool isTraceTag(const std::string& tag);
 
   static bool isGitBuild();
   static const char* getGitBranchName();
diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h
index e588dd36d..0118f1484 100644
--- a/src/options/didyoumean.h
+++ b/src/options/didyoumean.h
@@ -36,6 +36,10 @@ class CVC5_EXPORT DidYouMean {
   ~DidYouMean() {}
 
   void addWord(std::string word) { d_words.insert(std::move(word)); }
+  void addWords(const std::vector<std::string>& words)
+  {
+    d_words.insert(words.begin(), words.end());
+  }
 
   std::vector<std::string> getMatch(const std::string& input);
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1b6cff519..bf2def05b 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -372,12 +372,12 @@ void OptionsHandler::showConfiguration(const std::string& option,
   exit(0);
 }
 
-static void printTags(unsigned ntags, char const* const* tags)
+static void printTags(const std::vector<std::string>& tags)
 {
   std::cout << "available tags:";
-  for (unsigned i = 0; i < ntags; ++ i)
+  for (const auto& t : tags)
   {
-    std::cout << "  " << tags[i] << std::endl;
+    std::cout << "  " << t << std::endl;
   }
   std::cout << std::endl;
 }
@@ -393,8 +393,8 @@ void OptionsHandler::showDebugTags(const std::string& option,
   {
     throw OptionException("debug tags not available in non-tracing builds");
   }
-  printTags(Configuration::getNumDebugTags(),Configuration::getDebugTags());
-  exit(0);
+  printTags(Configuration::getDebugTags());
+  std::exit(0);
 }
 
 void OptionsHandler::showTraceTags(const std::string& option,
@@ -404,29 +404,17 @@ void OptionsHandler::showTraceTags(const std::string& option,
   {
     throw OptionException("trace tags not available in non-tracing build");
   }
-  printTags(Configuration::getNumTraceTags(), Configuration::getTraceTags());
-  exit(0);
+  printTags(Configuration::getTraceTags());
+  std::exit(0);
 }
 
-static std::string suggestTags(char const* const* validTags,
+static std::string suggestTags(const std::vector<std::string>& validTags,
                                std::string inputTag,
-                               char const* const* additionalTags)
+                               const std::vector<std::string>& 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]);
-    }
-  }
-
+  didYouMean.addWords(validTags);
+  didYouMean.addWords(additionalTags);
   return didYouMean.getMatchAsString(inputTag);
 }
 
@@ -438,18 +426,17 @@ void OptionsHandler::enableTraceTag(const std::string& option,
   {
     throw OptionException("trace tags not available in non-tracing builds");
   }
-  else if(!Configuration::isTraceTag(optarg.c_str()))
+  else if (!Configuration::isTraceTag(optarg))
   {
     if (optarg == "help")
     {
-      printTags(
-          Configuration::getNumTraceTags(), Configuration::getTraceTags());
-      exit(0);
+      printTags(Configuration::getTraceTags());
+      std::exit(0);
     }
 
     throw OptionException(
         std::string("trace tag ") + optarg + std::string(" not available.")
-        + suggestTags(Configuration::getTraceTags(), optarg, nullptr));
+        + suggestTags(Configuration::getTraceTags(), optarg, {}));
   }
   Trace.on(optarg);
 }
@@ -467,14 +454,12 @@ void OptionsHandler::enableDebugTag(const std::string& option,
     throw OptionException("debug tags not available in non-tracing builds");
   }
 
-  if (!Configuration::isDebugTag(optarg.c_str())
-      && !Configuration::isTraceTag(optarg.c_str()))
+  if (!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg))
   {
     if (optarg == "help")
     {
-      printTags(
-          Configuration::getNumDebugTags(), Configuration::getDebugTags());
-      exit(0);
+      printTags(Configuration::getDebugTags());
+      std::exit(0);
     }
 
     throw OptionException(std::string("debug tag ") + optarg