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.

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 75219840ad8e386d6fc54cd12db9c296df071f81..7c1661e5e698c84fbb182e5924c715e09790ca9c 100644 (file)
--- 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 fd4775da44b1314104e01b8c6911d85565d20c28..fd5742c603f0d2c894990d8df4dab9890e525069 100644 (file)
--- 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 582c60d40d4cc59f6cf63d2369786c720cafdff3..a29d2eb4df01bc1f3e639c939894b71b48ec84d3 100644 (file)
--- 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 b657a6dfafe933335706fc1f4f4e48137e369c37..2a7cf1f4dd6a497f0adcb039c074b95441172add 100644 (file)
--- 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 3c0fe838bad2380d2253fb6fd0bfd64a26656308..f9bca85354c2e64664a60ebeba1d2b7f9e86afe8 100644 (file)
--- 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 839c016af07559ad4a5e3e76fd2528b3de8afe73..f12fa6b050d5cf26cd3e53119a75229771ada9b4 100644 (file)
--- 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,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 34b2c9692728c1b35611029a09677e32f84ac228..1573ce16bcd8db0df79c73864a7b5add74ac5d66 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1018,29 +1018,6 @@ void QuitCommand::toStream(std::ostream& out,
   Printer::getPrinter(language)->toStreamCmdQuit(out);
 }
 
-/* -------------------------------------------------------------------------- */
-/* class CommentCommand                                                       */
-/* -------------------------------------------------------------------------- */
-
-CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
-std::string CommentCommand::getComment() const { return d_comment; }
-void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  Dump("benchmark") << *this;
-  d_commandStatus = CommandSuccess::instance();
-}
-
-Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
-std::string CommentCommand::getCommandName() const { return "comment"; }
-
-void CommentCommand::toStream(std::ostream& out,
-                              int toDepth,
-                              size_t dag,
-                              Language language) const
-{
-  Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
-}
-
 /* -------------------------------------------------------------------------- */
 /* class CommandSequence                                                      */
 /* -------------------------------------------------------------------------- */
@@ -2548,61 +2525,6 @@ void GetAssertionsCommand::toStream(std::ostream& out,
   Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
 }
 
-/* -------------------------------------------------------------------------- */
-/* class SetBenchmarkStatusCommand                                            */
-/* -------------------------------------------------------------------------- */
-
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
-    : d_status(status)
-{
-}
-
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
-{
-  return d_status;
-}
-
-void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  try
-  {
-    stringstream ss;
-    ss << d_status;
-    solver->setInfo("status", ss.str());
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* SetBenchmarkStatusCommand::clone() const
-{
-  return new SetBenchmarkStatusCommand(d_status);
-}
-
-std::string SetBenchmarkStatusCommand::getCommandName() const
-{
-  return "set-info";
-}
-
-void SetBenchmarkStatusCommand::toStream(std::ostream& out,
-                                         int toDepth,
-                                         size_t dag,
-                                         Language language) const
-{
-  Result::Sat status = Result::SAT_UNKNOWN;
-  switch (d_status)
-  {
-    case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
-    case BenchmarkStatus::SMT_UNSATISFIABLE: status = Result::UNSAT; break;
-    case BenchmarkStatus::SMT_UNKNOWN: status = Result::SAT_UNKNOWN; break;
-  }
-
-  Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, status);
-}
-
 /* -------------------------------------------------------------------------- */
 /* class SetBenchmarkLogicCommand                                             */
 /* -------------------------------------------------------------------------- */

diff --git a/src/smt/command.h b/src/smt/command.h
index 989e38ef0e46d6fefaf9c0ea142b5705481a862c..0756714b6c6673e742c7a1b745167af15f293259 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1232,25 +1232,6 @@ class CVC5_EXPORT GetAssertionsCommand : public Command
                 Language language = Language::LANG_AUTO) const override;
 }; /* class GetAssertionsCommand */
 
-class CVC5_EXPORT SetBenchmarkStatusCommand : public Command
-{
- protected:
-  BenchmarkStatus d_status;
-
- public:
-  SetBenchmarkStatusCommand(BenchmarkStatus status);
-
-  BenchmarkStatus getStatus() const;
-
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-}; /* class SetBenchmarkStatusCommand */
-
 class CVC5_EXPORT SetBenchmarkLogicCommand : public Command
 {
  protected:
@@ -1413,24 +1394,6 @@ class CVC5_EXPORT QuitCommand : public Command
                 Language language = Language::LANG_AUTO) const override;
 }; /* class QuitCommand */
 
-class CVC5_EXPORT CommentCommand : public Command
-{
-  std::string d_comment;
-
- public:
-  CommentCommand(std::string comment);
-
-  std::string getComment() const;
-
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                Language language = Language::LANG_AUTO) const override;
-}; /* class CommentCommand */
-
 class CVC5_EXPORT CommandSequence : public Command
 {
  protected:

diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index a3c271fc57d731619836747cdfee8a25e24b8d4b..a0a3962accf16a5115ef749d247c4014714413ad 100644 (file)
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -97,8 +97,8 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
   DeclareFunctionNodeCommand c(id, n, n.getType());
   if (Dump.isOn("skolems") && comment != "")
   {
-    d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(),
-                                             id + " is " + comment);
+    d_outMgr.getPrinter().toStreamCmdSetInfo(
+        d_outMgr.getDumpOut(), "notes", id + " is " + comment);
   }
   d_dm.addToDump(c, "skolems");
 }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 96a1aa8ea0303b2bc5b0f859dd1214e33b2cd4ce..28ad11f46a23fe94ee587d16ff3b2d91bf08abab 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -235,8 +235,9 @@ void SmtEngine::finishInit()
   {
       LogicInfo everything;
       everything.lock();
-      getPrinter().toStreamCmdComment(
+      getPrinter().toStreamCmdSetInfo(
           d_env->getDumpOut(),
+          "notes",
           "cvc5 always dumps the most general, all-supported logic (below), as "
           "some internals might require the use of a logic more general than "
           "the input.");
@@ -378,18 +379,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
 
   if (Dump.isOn("benchmark"))
   {
-    if (key == "status")
-    {
-      Result::Sat status =
-          (value == "sat")
-              ? Result::SAT
-              : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
-      getPrinter().toStreamCmdSetBenchmarkStatus(d_env->getDumpOut(), status);
-    }
-    else
-    {
-      getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value);
-    }
+    getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value);
   }
 
   if (key == "filename")

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 54cfc9a6d9d0a196d2d4d209b00827bd1cadb0a8..7fd786801bf1c962fcc71a8112f8c68d48cf5ea6 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -362,26 +362,26 @@ void TheoryEngine::dumpAssertions(const char* tag) {
   if (Dump.isOn(tag)) {
     const Printer& printer = d_env.getPrinter();
     std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdComment(out, "Starting completeness check");
+    printer.toStreamCmdSetInfo(out, "notes", "Starting completeness check");
     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
       Theory* theory = d_theoryTable[theoryId];
       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-        printer.toStreamCmdComment(out, "Completeness check");
+        printer.toStreamCmdSetInfo(out, "notes", "Completeness check");
         printer.toStreamCmdPush(out);
 
         // Dump the shared terms
         if (d_logicInfo.isSharingEnabled()) {
-          printer.toStreamCmdComment(out, "Shared terms");
+          printer.toStreamCmdSetInfo(out, "notes", "Shared terms");
           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
           for (unsigned i = 0; it != it_end; ++ it, ++i) {
               stringstream ss;
               ss << (*it);
-              printer.toStreamCmdComment(out, ss.str());
+              printer.toStreamCmdSetInfo(out, "notes", ss.str());
           }
         }
 
         // Dump the assertions
-        printer.toStreamCmdComment(out, "Assertions");
+        printer.toStreamCmdSetInfo(out, "notes", "Assertions");
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (; it != it_end; ++ it) {
           // Get the assertion
@@ -390,11 +390,11 @@ void TheoryEngine::dumpAssertions(const char* tag) {
 
           if ((*it).d_isPreregistered)
           {
-            printer.toStreamCmdComment(out, "Preregistered");
+            printer.toStreamCmdSetInfo(out, "notes", "Preregistered");
           }
           else
           {
-            printer.toStreamCmdComment(out, "Shared assertion");
+            printer.toStreamCmdSetInfo(out, "notes", "Shared assertion");
           }
           printer.toStreamCmdAssert(out, assertionNode);
         }
@@ -1365,7 +1365,7 @@ void TheoryEngine::lemma(TrustNode tlemma,
     Node n = lemma.negate();
     const Printer& printer = d_env.getPrinter();
     std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdComment(out, "theory lemma: expect valid");
+    printer.toStreamCmdSetInfo(out, "notes", "theory lemma: expect valid");
     printer.toStreamCmdCheckSat(out, n);
   }
 
@@ -1424,7 +1424,7 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
   if(Dump.isOn("t-conflicts")) {
     const Printer& printer = d_env.getPrinter();
     std::ostream& out = d_env.getDumpOut();
-    printer.toStreamCmdComment(out, "theory conflict: expect unsat");
+    printer.toStreamCmdSetInfo(out, "notes", "theory conflict: expect unsat");
     printer.toStreamCmdCheckSat(out, conflict);
   }