From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Thu, 23 Sep 2021 16:30:07 +0000 (-0500) Subject: Use `|` to print quoted strings in `set-info` command. (#7240) X-Git-Tag: cvc5-1.0.0~1176 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=970072e32f860a43b37bc0473bfdf1ab0af5d01e;p=cvc5.git 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 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& 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, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 34b2c9692..1573ce16b 100644 --- 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 989e38ef0..0756714b6 100644 --- 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 a3c271fc5..a0a3962ac 100644 --- 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 96a1aa8ea..28ad11f46 100644 --- 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 54cfc9a6d..7fd786801 100644 --- 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::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::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); }