Use `|` to print quoted strings in `set-info` command. (#7240)

This PR is a step towards enabling raw-benchmark for cvc5 regressions. cvc5 fails to reparse 57 regressions (in regress0) printed be raw-benchmark because they contain multi-line strings in set-info that we don't print between vertical bars right now. This PR fixes that bug and removes 2 commands (derived from set-info commands) that are not used by the parsers anymore.

6 files changed, 1 insertions, 67 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 75219840a..7c1661e5e 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -331,12 +331,6 @@ void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
   out << "GetUnsatCore()" << std::endl;
 }
 
-void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                               Result::Sat status) const
-{
-  out << "SetBenchmarkStatus(" << status << ')' << std::endl;
-}
-
 void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                               const std::string& logic) const
 {
@@ -380,12 +374,6 @@ void AstPrinter::toStreamCmdDatatypeDeclaration(
   out << "])" << std::endl;
 }
 
-void AstPrinter::toStreamCmdComment(std::ostream& out,
-                                    const std::string& comment) const
-{
-  out << "CommentCommand([" << comment << "])" << std::endl;
-}
-
 void AstPrinter::toStreamWithLetify(std::ostream& out,
                                     Node n,
                                     int toDepth,
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index fd4775da4..fd5742c60 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -112,10 +112,6 @@ class AstPrinter : public cvc5::Printer
   /** Print get-assertions command */
   void toStreamCmdGetAssertions(std::ostream& out) const override;
 
-  /** Print set-info :status command */
-  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                     Result::Sat status) const override;
-
   /** Print set-logic command */
   void toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                     const std::string& logic) const override;
@@ -151,10 +147,6 @@ class AstPrinter : public cvc5::Printer
   /** Print quit command */
   void toStreamCmdQuit(std::ostream& out) const override;
 
-  /** Print comment command */
-  void toStreamCmdComment(std::ostream& out,
-                          const std::string& comment) const override;
-
   /** Print command sequence command */
   void toStreamCmdCommandSequence(
       std::ostream& out, const std::vector<Command*>& sequence) const override;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 582c60d40..a29d2eb4d 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -436,12 +436,6 @@ void Printer::toStreamCmdGetAssertions(std::ostream& out) const
   printUnknownCommand(out, "get-assertions");
 }
 
-void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                            Result::Sat status) const
-{
-  printUnknownCommand(out, "set-info");
-}
-
 void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                            const std::string& logic) const
 {
@@ -503,12 +497,6 @@ void Printer::toStreamCmdQuit(std::ostream& out) const
   printUnknownCommand(out, "quit");
 }
 
-void Printer::toStreamCmdComment(std::ostream& out,
-                                 const std::string& comment) const
-{
-  printUnknownCommand(out, "comment");
-}
-
 void Printer::toStreamCmdDeclareHeap(std::ostream& out,
                                      TypeNode locType,
                                      TypeNode dataType) const
diff --git a/src/printer/printer.h b/src/printer/printer.h
index b657a6dfa..2a7cf1f4d 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -219,10 +219,6 @@ class Printer
   /** Print get-assertions command */
   virtual void toStreamCmdGetAssertions(std::ostream& out) const;
 
-  /** Print set-info :status command */
-  virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                             Result::Sat status) const;
-
   /** Print set-logic command */
   virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                             const std::string& logic) const;
@@ -263,9 +259,6 @@ class Printer
   /** Print quit command */
   virtual void toStreamCmdQuit(std::ostream& out) const;
 
-  /** Print comment command */
-  virtual void toStreamCmdComment(std::ostream& out,
-                                  const std::string& comment) const;
   /** Declare heap command */
   virtual void toStreamCmdDeclareHeap(std::ostream& out,
                                       TypeNode locType,
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 3c0fe838b..f9bca8535 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1626,12 +1626,6 @@ void Smt2Printer::toStreamCmdGetDifficulty(std::ostream& out) const
   out << "(get-difficulty)" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                                Result::Sat status) const
-{
-  out << "(set-info :status " << status << ')' << std::endl;
-}
-
 void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                                const std::string& logic) const
 {
@@ -1642,7 +1636,7 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
                                      const std::string& flag,
                                      const std::string& value) const
 {
-  out << "(set-info :" << flag << ' ' << value << ')' << std::endl;
+    out << "(set-info :" << flag << " |" << value << "|)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
@@ -1735,19 +1729,6 @@ void Smt2Printer::toStreamCmdDatatypeDeclaration(
   out << ")" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdComment(std::ostream& out,
-                                     const std::string& comment) const
-{
-  std::string s = comment;
-  size_t pos = 0;
-  while ((pos = s.find_first_of('"', pos)) != string::npos)
-  {
-    s.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(set-info :notes \"" << s << "\")" << std::endl;
-}
-
 void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
                                          TypeNode locType,
                                          TypeNode dataType) const
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 839c016af..f12fa6b05 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -171,10 +171,6 @@ class Smt2Printer : public cvc5::Printer
   /** Print get-assertions command */
   void toStreamCmdGetAssertions(std::ostream& out) const override;
 
-  /** Print set-info :status command */
-  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
-                                     Result::Sat status) const override;
-
   /** Print set-logic command */
   void toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                     const std::string& logic) const override;
@@ -210,10 +206,6 @@ class Smt2Printer : public cvc5::Printer
   /** Print quit command */
   void toStreamCmdQuit(std::ostream& out) const override;
 
-  /** Print comment command */
-  void toStreamCmdComment(std::ostream& out,
-                          const std::string& comment) const override;
-
   /** Print declare-heap command */
   void toStreamCmdDeclareHeap(std::ostream& out,
                               TypeNode locType,