Avoid escaping `double-quotes` twice. (#7409)

With -o raw-benchmark, The command:

(echo """")
was printed as

(echo """""""")
because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bff4f72abd397ef53c6bc615fdc5b2b387958dcf..a75aa36da08c5e44cdae0fe9e3fc97a49e32a0f6 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -793,7 +793,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
 
     /* echo */
   | ECHO_TOK
-    ( simpleSymbolicExpr[s]
+    ( str[s, true]
       { cmd->reset(new EchoCommand(s)); }
     | { cmd->reset(new EchoCommand()); }
     )

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 32b195be2c38ae5a95291e282b3a7dcc7b3a83cb..1da2a3c7be9262bf79f8d03b3db760405ccc6b2b 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1723,15 +1723,7 @@ void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
 void Smt2Printer::toStreamCmdEcho(std::ostream& out,
                                   const std::string& output) const
 {
-  std::string s = output;
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = s.find('"', pos)) != string::npos)
-  {
-    s.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(echo \"" << s << "\")" << std::endl;
+  out << "(echo " << cvc5::quoteString(output) << ')' << std::endl;
 }
 
 /*
@@ -1930,14 +1922,9 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
 #endif /* CVC5_COMPETITION_MODE */
 }
 
-static void errorToStream(std::ostream& out, std::string message, Variant v) {
-  // escape all double-quotes
-  size_t pos = 0;
-  while((pos = message.find('"', pos)) != string::npos) {
-    message.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(error \"" << message << "\")" << endl;
+static void errorToStream(std::ostream& out, std::string message, Variant v)
+{
+  out << "(error " << cvc5::quoteString(message) << ')' << endl;
 }
 
 static void toStream(std::ostream& out, const CommandFailure* s, Variant v) {

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 311d6713aadd59574fa02f83d594d130f636fcbe..e8ee6d59ce60b746dcaed458e949f5a732a8ecc0 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,6 +38,7 @@
 #include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/model.h"
+#include "util/smt2_quote_string.h"
 #include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
@@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out,
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-EchoCommand::EchoCommand(std::string output)
-{
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = output.find('"', pos)) != string::npos)
-  {
-    output.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  d_output = '"' + output + '"';
-}
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 
 std::string EchoCommand::getOutput() const { return d_output; }
+
 void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   /* we don't have an output stream here, nothing to do */
@@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver,
                          SymbolManager* sm,
                          std::ostream& out)
 {
-  out << d_output << std::endl;
+  out << cvc5::quoteString(d_output) << std::endl;
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                            << std::endl;
   d_commandStatus = CommandSuccess::instance();
@@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver,
 }
 
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+
 std::string EchoCommand::getCommandName() const { return "echo"; }
 
 void EchoCommand::toStream(std::ostream& out,

diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index 82750c48b0e20a5df26bc6940032c0fbb50f3e96..e2ab4a74ce51ab3f42990ffd9dda3a3d59b6e853 100644 (file)
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -42,4 +42,16 @@ std::string quoteSymbol(const std::string& s){
   return s;
 }
 
+std::string quoteString(const std::string& s) {
+  // escape all double-quotes
+  std::string output = s;
+  size_t pos = 0;
+  while ((pos = output.find('"', pos)) != std::string::npos)
+  {
+    output.replace(pos, 1, "\"\"");
+    pos += 2;
+  }
+  return '"' + output + '"';
+}
+
 }  // namespace cvc5

diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h
index 98b2f89dd9f87f926f65c5ffce540d06caaa0ea3..f8be53c0cc3a66b070c6fec12f68b748bf2ebb33 100644 (file)
--- a/src/util/smt2_quote_string.h
+++ b/src/util/smt2_quote_string.h
@@ -27,6 +27,11 @@ namespace cvc5 {
  */
 std::string quoteSymbol(const std::string& s);
 
+/**
+ * SMT-LIB 2 quoting for strings
+ */
+std::string quoteString(const std::string& s);
+
 }  // namespace cvc5
 
 #endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */