From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 20 May 2021 02:54:52 +0000 (-0700)
Subject: Fix echo printing. (#6573)
X-Git-Tag: cvc5-1.0.0~1726
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f91f8f24d6ed98698373f5d51b17cf583adcd768;p=cvc5.git

Fix echo printing. (#6573)

Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e4e8aff1a..02cea842a 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -294,7 +294,18 @@ void EmptyCommand::toStream(std::ostream& out,
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-EchoCommand::EchoCommand(std::string output) : d_output(output) {}
+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 + '"';
+}
+
 std::string EchoCommand::getOutput() const { return d_output; }
 void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fe034c519..8cb7f7d1f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -542,6 +542,7 @@ set(regress_0_tests
   regress0/define-fun-model.smt2
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
+  regress0/echo.smt2
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2
diff --git a/test/regress/regress0/echo.smt2 b/test/regress/regress0/echo.smt2
new file mode 100644
index 000000000..a2747373e
--- /dev/null
+++ b/test/regress/regress0/echo.smt2
@@ -0,0 +1,18 @@
+; EXPECT: "str"""
+; EXPECT: "str""ing"
+; EXPECT: "hi"
+; EXPECT: "str""""ing"
+; EXPECT: "str""i""ng"
+; EXPECT: "str\ing"
+; EXPECT: "str\\ing"
+; EXPECT: "str\"
+; EXPECT: "\u{65}"
+(echo "str""")
+(echo "str""ing")
+(echo "hi")
+(echo "str""""ing")
+(echo "str""i""ng")
+(echo "str\ing")
+(echo "str\\ing")
+(echo "str\")
+(echo "\u{65}")