From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 10 Dec 2021 17:48:48 +0000 (-0800)
Subject: Allow for wildcards in `-t` (#7791)
X-Git-Tag: cvc5-1.0.0~688
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87cd3112098d24b35cedabffdc5f927998a4e4b0;p=cvc5.git

Allow for wildcards in `-t` (#7791)

This PR extends -t to allow for wildcards: -t nl-ext-*. Internally, these wildcards are replaced by .* and fed into std::regex.
---

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 9c40442b7..042fd6b8a 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -139,7 +139,7 @@ name   = "Base"
   long       = "trace=TAG"
   type       = "std::string"
   predicates = ["enableTraceTag"]
-  help       = "trace something (e.g. -t pushpop), can repeat"
+  help       = "trace something (e.g. -t pushpop), can repeat and may contain wildcards like (e.g. -t theory::*)"
 
 [[option]]
   category   = "regular"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 50b3ec0a9..132525e6d 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -18,6 +18,7 @@
 #include <cerrno>
 #include <iostream>
 #include <ostream>
+#include <regex>
 #include <string>
 
 #include "base/check.h"
@@ -66,6 +67,40 @@ std::string suggestTags(const std::vector<std::string>& validTags,
   return didYouMean.getMatchAsString(inputTag);
 }
 
+/**
+ * Select all tags from validTags that match the given (globbing) pattern.
+ * The pattern may contain `*` as wildcards. These are internally converted to
+ * `.*` and matched using std::regex. If no wildcards are present, regular
+ * string comparisons are used.
+ */
+std::vector<std::string> selectTags(const std::vector<std::string>& validTags, std::string pattern)
+{
+  bool isRegex = false;
+  size_t pos = 0;
+  while ((pos = pattern.find('*', pos)) != std::string::npos)
+  {
+    pattern.replace(pos, 1, ".*");
+    pos += 2;
+    isRegex = true;
+  }
+  std::vector<std::string> results;
+  if (isRegex)
+  {
+    std::regex re(pattern);
+    std::copy_if(validTags.begin(), validTags.end(), std::back_inserter(results),
+      [&re](const auto& tag){ return std::regex_match(tag, re); }
+    );
+  }
+  else
+  {
+    if (std::find(validTags.begin(), validTags.end(), pattern) != validTags.end())
+    {
+      results.emplace_back(pattern);
+    }
+  }
+  return results;
+}
+
 }  // namespace
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
@@ -199,7 +234,8 @@ void OptionsHandler::enableTraceTag(const std::string& flag,
   {
     throw OptionException("trace tags not available in non-tracing builds");
   }
-  else if (!Configuration::isTraceTag(optarg))
+  auto tags = selectTags(Configuration::getTraceTags(), optarg);
+  if (tags.empty())
   {
     if (optarg == "help")
     {
@@ -209,10 +245,13 @@ void OptionsHandler::enableTraceTag(const std::string& flag,
     }
 
     throw OptionException(
-        std::string("trace tag ") + optarg + std::string(" not available.")
+        std::string("no trace tag matching ") + optarg + std::string(" was found.")
         + suggestTags(Configuration::getTraceTags(), optarg, {}));
   }
-  Trace.on(optarg);
+  for (const auto& tag: tags)
+  {
+    Trace.on(tag);
+  }
 }
 
 void OptionsHandler::enableDebugTag(const std::string& flag,
diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp
index 0f95722fd..f4dbbbd36 100644
--- a/src/util/didyoumean.cpp
+++ b/src/util/didyoumean.cpp
@@ -37,7 +37,7 @@ uint64_t editDistance(const std::string& a, const std::string& b) {
   constexpr uint64_t swapCost = 0;
   constexpr uint64_t substituteCost = 2;
   constexpr uint64_t addCost = 1;
-  constexpr uint64_t deleteCost = 3;
+  constexpr uint64_t deleteCost = 2;
   constexpr uint64_t switchCaseCost = 0;
 
   uint64_t len1 = a.size();
@@ -104,7 +104,7 @@ std::vector<std::string> DidYouMean::getMatch(const std::string& input)
   }
 
   /** Magic numbers */
-  constexpr uint64_t similarityThreshold = 7;
+  constexpr uint64_t similarityThreshold = 10;
   constexpr uint64_t numMatchesThreshold = 10;
 
   std::vector<std::pair<uint64_t,std::string>> scores;
@@ -127,7 +127,7 @@ std::vector<std::string> DidYouMean::getMatch(const std::string& input)
     // from here on, matches are not similar enough
     if (score.first > similarityThreshold) break;
     // from here on, matches are way worse than the best one
-    if (score.first > min_score + 2) break;
+    if (score.first > min_score + 4) break;
     // we already have enough matches
     if (ret.size() >= numMatchesThreshold) break;
     ret.push_back(score.second);