Avoid quoting symbols already surrounded with vertical bars (#8896)

This PR fixes the issue of replacing bars with underscores in already quoted symbols.
For example previously this line would print |_a _|

std::cout << d_solver.declareFun("|a |", {}, d_solver.getRealSort());
Now it prints |a |.

diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index 7dbdc9b4737d8ff32ac75c389401cc6eba126665..728cc4f02c317b77a76faf9bce6a387341edf929 100644 (file)
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -23,26 +23,41 @@ namespace cvc5::internal {
 /**
  * SMT-LIB 2 quoting for symbols
  */
-std::string quoteSymbol(const std::string& s){
+std::string quoteSymbol(const std::string& s)
+{
+  if (s.empty())
+  {
+    return "||";
+  }
+
   // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted)
   // symbols
   if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
                           "0123456789~!@$%^&*_-+=<>.?/")
-          != std::string::npos
-      || s.empty() || (s[0] >= '0' && s[0] <= '9'))
+          == std::string::npos
+      && (s[0] < '0' || s[0] > '9'))
+  {
+    return s;
+  }
+  std::string tmp = s;
+  if (s.front() == '|' && s.back() == '|' && s.length() > 1)
+  {
+    // if s is already surrounded with vertical bars, we need to check the
+    // characters between them
+    tmp = s.substr(1, s.length() - 2);
+  }
+
+  // must quote the symbol, but it cannot contain | or \, we turn those into _
+  size_t p;
+  while ((p = tmp.find_first_of("\\|")) != std::string::npos)
   {
-    std::string tmp(s);
-    // must quote the symbol, but it cannot contain | or \, we turn those into _
-    size_t p;
-    while((p = tmp.find_first_of("\\|")) != std::string::npos) {
-      tmp = tmp.replace(p, 1, "_");
-    }
-    return "|" + tmp + "|";
+    tmp = tmp.replace(p, 1, "_");
   }
-  return s;
+  return "|" + tmp + "|";
 }
 
-std::string quoteString(const std::string& s) {
+std::string quoteString(const std::string& s)
+{
   // escape all double-quotes
   std::string output = s;
   size_t pos = 0;

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index e3bf8c074129341397d6cd351a17389276ecd1d1..878904da56ab5010897abb0db6cfe23f22e56ae3 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3533,5 +3533,11 @@ TEST_F(TestApiBlackSolver, declareOracleFunSat2)
   ASSERT_TRUE(xval != yval);
 }
 
+TEST_F(TestApiBlackSolver, verticalBars)
+{
+  Term a = d_solver.declareFun("|a |", {}, d_solver.getRealSort());
+  ASSERT_EQ("|a |", a.toString());
+}
+
 }  // namespace test
 }  // namespace cvc5::internal