From 2958e98eff88ce14aefcdeee3c6ec579fcc2bb1d Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 8 Jan 2021 13:38:24 -0300 Subject: [PATCH] [proof-new] Implementing getProof in the API and SMT engine (#5751) A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits). --- src/api/cvc4cpp.cpp | 2 +- src/smt/command.cpp | 26 +++++++++++++++++++++++++- src/smt/command.h | 7 +++++++ src/smt/proof_manager.cpp | 4 ++-- src/smt/proof_manager.h | 5 +++-- src/smt/smt_engine.cpp | 37 +++++++++++++++++++++++-------------- src/smt/smt_engine.h | 6 ++++++ 7 files changed, 67 insertions(+), 20 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 49974d30d..621e3c1c0 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2473,7 +2473,7 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const << "Cannot get specialized constructor type for non-datatype type " << retSort; CVC4_API_SOLVER_TRY_CATCH_BEGIN; - + NodeManager* nm = d_solver->getNodeManager(); Node ret = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index f3b0ee915..0c8accf7a 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1886,7 +1886,31 @@ void BlockModelValuesCommand::toStream(std::ostream& out, GetProofCommand::GetProofCommand() {} void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) { - Unimplemented() << "Unimplemented get-proof\n"; + try + { + d_result = solver->getSmtEngine()->getProof(); + d_commandStatus = CommandSuccess::instance(); + } + catch (api::CVC4ApiRecoverableException& e) + { + d_commandStatus = new CommandRecoverableFailure(e.what()); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const +{ + if (ok()) + { + out << d_result; + } + else + { + this->Command::printResult(out, verbosity); + } } Command* GetProofCommand::clone() const diff --git a/src/smt/command.h b/src/smt/command.h index 399050d94..9330f2015 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1015,6 +1015,9 @@ class CVC4_PUBLIC GetProofCommand : public Command GetProofCommand(); void invoke(api::Solver* solver, SymbolManager* sm) override; + + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1022,6 +1025,10 @@ class CVC4_PUBLIC GetProofCommand : public Command int toDepth = -1, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; + + private: + /** the result of the getProof call */ + std::string d_result; }; /* class GetProofCommand */ class CVC4_PUBLIC GetInstantiationsCommand : public Command diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index ce9b4923c..d82e22736 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -108,7 +108,8 @@ void PfManager::setFinalProof(std::shared_ptr pfn, Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } -void PfManager::printProof(std::shared_ptr pfn, +void PfManager::printProof(std::ostream& out, + std::shared_ptr pfn, Assertions& as, DefinedFunctionMap& df) { @@ -116,7 +117,6 @@ void PfManager::printProof(std::shared_ptr pfn, std::shared_ptr fp = getFinalProof(pfn, as, df); // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node - std::ostream& out = *options::out(); out << "(proof\n"; out << *fp; out << "\n)\n"; diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index be05fc2f7..a6f284cad 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -49,7 +49,7 @@ class PfManager PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** - * Print the proof on the output channel of the current options in scope. + * Print the proof on the given output stream. * * The argument pfn is the proof for false in the current context. * @@ -58,7 +58,8 @@ class PfManager * function map correspond to equalities of the form (= f (lambda (...) t)), * which are considered assertions in the final proof. */ - void printProof(std::shared_ptr pfn, + void printProof(std::ostream& out, + std::shared_ptr pfn, Assertions& as, DefinedFunctionMap& df); /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4c47587a6..d89b6e802 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -953,12 +953,6 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; - if (options::dumpProofs() && options::proofNew() - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - printProof(); - } - // Check that SAT results generate a model correctly. if(options::checkModels()) { if (r.asSatisfiabilityResult().isSat() == Result::SAT) @@ -1496,23 +1490,38 @@ UnsatCore SmtEngine::getUnsatCore() { return getUnsatCoreInternal(); } -void SmtEngine::printProof() +std::string SmtEngine::getProof() { - if (d_pfManager == nullptr) + Trace("smt") << "SMT getProof()\n"; + SmtScope smts(this); + finishInit(); + if (Dump.isOn("benchmark")) { - throw RecoverableModalException("Cannot print proof, no proof manager."); + getOutputManager().getPrinter().toStreamCmdGetProof( + getOutputManager().getDumpOut()); } - if (getSmtMode() != SmtMode::UNSAT) +#if IS_PROOFS_BUILD + if (!options::proofNew()) + { + throw ModalException("Cannot get a proof when proof-new option is off."); + } + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( - "Cannot print proof unless immediately preceded by " - "UNSAT/ENTAILED."); + "Cannot get a proof unless immediately preceded by " + "UNSAT/ENTAILED response."); } + // the prop engine has the proof of false PropEngine* pe = getPropEngine(); Assert(pe != nullptr); Assert(pe->getProof() != nullptr); - // the prop engine has the proof of false - d_pfManager->printProof(pe->getProof(), *d_asserts, *d_definedFunctions); + Assert(d_pfManager); + std::ostringstream ss; + d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions); + return ss.str(); +#else /* IS_PROOFS_BUILD */ + throw ModalException("This build of CVC4 doesn't have proof support."); +#endif /* IS_PROOFS_BUILD */ } void SmtEngine::printInstantiations( std::ostream& out ) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 091f69642..558bd2b40 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -683,6 +683,12 @@ class CVC4_PUBLIC SmtEngine */ UnsatCore getUnsatCore(); + /** + * Get a refutation proof (only if immediately preceded by an UNSAT or + * ENTAILED query). Only permitted if CVC4 was built with proof support and + * the proof option is on. */ + std::string getProof(); + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. -- 2.30.2