From c1738f508bc9dd7615eaa7b7b4af24acfa46f65c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Jun 2022 14:55:52 -0700 Subject: [PATCH] Simplify printing of command results (#8902) This moves redundant code from `Command::printResult()` overrides to the base method. This is a step towards simplifying printing options, which is needed to fix #8893 (which itself is a step towards a parser API). --- src/smt/command.cpp | 286 +++++++++++--------------------------------- src/smt/command.h | 7 +- 2 files changed, 77 insertions(+), 216 deletions(-) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 174c47e36..fe02770cf 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -163,7 +163,11 @@ bool Command::interrupted() const void Command::invoke(cvc5::Solver* solver, SymbolManager* sm, std::ostream& out) { invoke(solver, sm); - if (!(isMuted() && ok())) + if (!ok()) + { + out << *d_commandStatus; + } + else if (!isMuted()) { printResult(out); } @@ -389,15 +393,7 @@ cvc5::Result CheckSatCommand::getResult() const { return d_result; } void CheckSatCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - Trace("dtview::command") << "* RESULT: " << d_result << std::endl; - out << d_result << endl; - } + out << d_result << endl; } Command* CheckSatCommand::clone() const @@ -457,14 +453,7 @@ cvc5::Result CheckSatAssumingCommand::getResult() const void CheckSatAssumingCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result << endl; - } + out << d_result << endl; } Command* CheckSatAssumingCommand::clone() const @@ -760,14 +749,7 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) cvc5::SynthResult CheckSynthCommand::getResult() const { return d_result; } void CheckSynthCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_solution.str(); - } + out << d_solution.str(); } Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); } @@ -1401,14 +1383,7 @@ void SimplifyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) cvc5::Term SimplifyCommand::getResult() const { return d_result; } void SimplifyCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result << endl; - } + out << d_result << endl; } Command* SimplifyCommand::clone() const @@ -1473,16 +1448,9 @@ void GetValueCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) cvc5::Term GetValueCommand::getResult() const { return d_result; } void GetValueCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); - out << d_result << endl; - } + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + out << d_result << endl; } Command* GetValueCommand::clone() const @@ -1545,14 +1513,7 @@ void GetAssignmentCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) cvc5::Term GetAssignmentCommand::getResult() const { return d_result; } void GetAssignmentCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result << endl; - } + out << d_result << endl; } Command* GetAssignmentCommand::clone() const @@ -1596,17 +1557,7 @@ void GetModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetModelCommand::printResult(std::ostream& out) const -{ - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result; - } -} +void GetModelCommand::printResult(std::ostream& out) const { out << d_result; } Command* GetModelCommand::clone() const { @@ -1732,17 +1683,7 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } -void GetProofCommand::printResult(std::ostream& out) const -{ - if (ok()) - { - out << d_result; - } - else - { - this->Command::printResult(out); - } -} +void GetProofCommand::printResult(std::ostream& out) const { out << d_result; } Command* GetProofCommand::clone() const { @@ -1786,14 +1727,7 @@ void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetInstantiationsCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_solver->getInstantiations(); - } + out << d_solver->getInstantiations(); } Command* GetInstantiationsCommand::clone() const @@ -1864,23 +1798,16 @@ void GetInterpolantCommand::invoke(Solver* solver, SymbolManager* sm) void GetInterpolantCommand::printResult(std::ostream& out) const { - if (!ok()) + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + if (!d_result.isNull()) { - this->Command::printResult(out); + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; } else { - options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); - if (!d_result.isNull()) - { - out << "(define-fun " << d_name << " () Bool " << d_result << ")" - << std::endl; - } - else - { - out << "fail" << std::endl; - } + out << "fail" << std::endl; } } @@ -1928,23 +1855,16 @@ void GetInterpolantNextCommand::invoke(Solver* solver, SymbolManager* sm) void GetInterpolantNextCommand::printResult(std::ostream& out) const { - if (!ok()) + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + if (!d_result.isNull()) { - this->Command::printResult(out); + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; } else { - options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); - if (!d_result.isNull()) - { - out << "(define-fun " << d_name << " () Bool " << d_result << ")" - << std::endl; - } - else - { - out << "fail" << std::endl; - } + out << "fail" << std::endl; } } @@ -2015,23 +1935,16 @@ void GetAbductCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetAbductCommand::printResult(std::ostream& out) const { - if (!ok()) + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + if (!d_result.isNull()) { - this->Command::printResult(out); + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; } else { - options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); - if (!d_result.isNull()) - { - out << "(define-fun " << d_name << " () Bool " << d_result << ")" - << std::endl; - } - else - { - out << "fail" << std::endl; - } + out << "fail" << std::endl; } } @@ -2075,23 +1988,16 @@ void GetAbductNextCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetAbductNextCommand::printResult(std::ostream& out) const { - if (!ok()) + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); + if (!d_result.isNull()) { - this->Command::printResult(out); + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; } else { - options::ioutils::Scope scope(out); - options::ioutils::applyDagThresh(out, 0); - if (!d_result.isNull()) - { - out << "(define-fun " << d_name << " () Bool " << d_result << ")" - << std::endl; - } - else - { - out << "fail" << std::endl; - } + out << "fail" << std::endl; } } @@ -2155,14 +2061,7 @@ cvc5::Term GetQuantifierEliminationCommand::getResult() const } void GetQuantifierEliminationCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result << endl; - } + out << d_result << endl; } Command* GetQuantifierEliminationCommand::clone() const @@ -2214,14 +2113,7 @@ std::vector GetUnsatAssumptionsCommand::getResult() const void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - container_to_stream(out, d_result, "(", ")\n", " "); - } + container_to_stream(out, d_result, "(", ")\n", " "); } Command* GetUnsatAssumptionsCommand::clone() const @@ -2268,26 +2160,19 @@ void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetUnsatCoreCommand::printResult(std::ostream& out) const { - if (!ok()) + if (d_solver->getOption("print-unsat-cores-full") == "true") { - this->Command::printResult(out); + // use the assertions + UnsatCore ucr(termVectorToNodes(d_result)); + ucr.toStream(out); } else { - if (d_solver->getOption("print-unsat-cores-full") == "true") - { - // use the assertions - UnsatCore ucr(termVectorToNodes(d_result)); - ucr.toStream(out); - } - else - { - // otherwise, use the names - std::vector names; - d_sm->getExpressionNames(d_result, names, true); - UnsatCore ucr(names); - ucr.toStream(out); - } + // otherwise, use the names + std::vector names; + d_sm->getExpressionNames(d_result, names, true); + UnsatCore ucr(names); + ucr.toStream(out); } } @@ -2342,30 +2227,23 @@ void GetDifficultyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetDifficultyCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else + out << "(" << std::endl; + for (const std::pair& d : d_result) { - out << "(" << std::endl; - for (const std::pair& d : d_result) + out << "("; + // use name if it has one + std::string name; + if (d_sm->getExpressionName(d.first, name, true)) { - out << "("; - // use name if it has one - std::string name; - if (d_sm->getExpressionName(d.first, name, true)) - { - out << name; - } - else - { - out << d.first; - } - out << " " << d.second << ")" << std::endl; + out << name; } - out << ")" << std::endl; + else + { + out << d.first; + } + out << " " << d.second << ")" << std::endl; } + out << ")" << std::endl; } const std::map& GetDifficultyCommand::getDifficultyMap() @@ -2417,19 +2295,12 @@ void GetLearnedLiteralsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) void GetLearnedLiteralsCommand::printResult(std::ostream& out) const { - if (!ok()) + out << "(" << std::endl; + for (const cvc5::Term& lit : d_result) { - this->Command::printResult(out); - } - else - { - out << "(" << std::endl; - for (const cvc5::Term& lit : d_result) - { - out << lit << std::endl; - } - out << ")" << std::endl; + out << lit << std::endl; } + out << ")" << std::endl; } const std::vector& GetLearnedLiteralsCommand::getLearnedLiterals() @@ -2481,14 +2352,7 @@ void GetAssertionsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) std::string GetAssertionsCommand::getResult() const { return d_result; } void GetAssertionsCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else - { - out << d_result; - } + out << d_result; } Command* GetAssertionsCommand::clone() const @@ -2625,11 +2489,7 @@ void GetInfoCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) std::string GetInfoCommand::getResult() const { return d_result; } void GetInfoCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else if (d_result != "") + if (d_result != "") { out << d_result << endl; } @@ -2720,11 +2580,7 @@ void GetOptionCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) std::string GetOptionCommand::getResult() const { return d_result; } void GetOptionCommand::printResult(std::ostream& out) const { - if (!ok()) - { - this->Command::printResult(out); - } - else if (d_result != "") + if (d_result != "") { out << d_result << endl; } diff --git a/src/smt/command.h b/src/smt/command.h index beffab0d6..e17105f1e 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -185,7 +185,6 @@ class CVC5_EXPORT Command /** Get the command status (it's NULL if we haven't run yet). */ const CommandStatus* getCommandStatus() const { return d_commandStatus; } - virtual void printResult(std::ostream& out) const; /** * Clone this Command (make a shallow copy). @@ -215,6 +214,12 @@ class CVC5_EXPORT Command static void resetSolver(cvc5::Solver* solver); protected: + /** + * Print the result of running the command. This method is only called if the + * command ran successfully. + */ + virtual void printResult(std::ostream& out) const; + // These methods rely on Command being a friend of classes in the API. // Subclasses of command should use these methods for conversions, // which is currently necessary for e.g. printing commands. -- 2.30.2