From 01d8991ad7059fff4807c2c597c04959d39ab176 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Dec 2020 16:14:59 -0600 Subject: [PATCH] (proof-new) Updates to SMT proof manager and SmtEngine (#5446) This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode. This makes it so that it only remains to make PropEngine to be proof producing. --- src/prop/prop_engine.cpp | 6 +++ src/prop/prop_engine.h | 7 +++ src/smt/proof_manager.cpp | 89 ++++++++++++++++++++++++++------------- src/smt/proof_manager.h | 42 +++++++++++++----- src/smt/smt_engine.cpp | 56 ++++++++++++++++++++++++ src/smt/smt_engine.h | 19 ++++++++- 6 files changed, 177 insertions(+), 42 deletions(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4596972e9..26d1e615b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -353,5 +353,11 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const { return true; } +std::shared_ptr PropEngine::getProof() +{ + // TODO (proj #37) implement this + return nullptr; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1fb79231d..e4d536c29 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -219,6 +219,13 @@ class PropEngine */ bool properExplanation(TNode node, TNode expl) const; + /** + * Return the prop engine proof. This should be called only when proofs are + * enabled. Returns a proof of false whose free assumptions are the + * preprocessed assertions. + */ + std::shared_ptr getProof(); + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 685032136..6bdc4ced0 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -18,6 +18,7 @@ #include "options/base_options.h" #include "options/smt_options.h" #include "smt/assertions.h" +#include "smt/defined_function.h" namespace CVC4 { namespace smt { @@ -55,78 +56,80 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) PfManager::~PfManager() {} -void PfManager::setFinalProof(ProofGenerator* pg, context::CDList* al) +void PfManager::setFinalProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df) { - Assert(al != nullptr); // Note this assumes that setFinalProof is only called once per unsat // response. This method would need to cache its result otherwise. Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n"; - // d_finalProof should just be a ProofNode - std::shared_ptr body = pg->getProofFor(d_false)->clone(); - if (Trace.isOn("smt-proof-debug")) { Trace("smt-proof-debug") << "SmtEngine::setFinalProof(): Proof node for false:\n"; - Trace("smt-proof-debug") << *body.get() << std::endl; + Trace("smt-proof-debug") << *pfn.get() << std::endl; Trace("smt-proof-debug") << "=====" << std::endl; } + std::vector assertions; + getAssertions(as, df, assertions); + if (Trace.isOn("smt-proof")) { + Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..." + << std::endl; std::vector fassumps; - expr::getFreeAssumptions(body.get(), fassumps); + expr::getFreeAssumptions(pfn.get(), fassumps); Trace("smt-proof") << "SmtEngine::setFinalProof(): initial free assumptions are:\n"; for (const Node& a : fassumps) { Trace("smt-proof") << "- " << a << std::endl; } - } - std::vector assertions; - Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n"; - for (context::CDList::const_iterator i = al->begin(); i != al->end(); - ++i) - { - Node n = *i; - Trace("smt-proof") << "- " << n << std::endl; - assertions.push_back(n); + Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n"; + for (const Node& n : assertions) + { + Trace("smt-proof") << "- " << n << std::endl; + } + Trace("smt-proof") << "=====" << std::endl; } - Trace("smt-proof") << "=====" << std::endl; Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n"; Assert(d_pfpp != nullptr); - d_pfpp->process(body); + d_pfpp->process(pfn); Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n"; // Now make the final scope, which ensures that the only open leaves // of the proof are the assertions. - d_finalProof = d_pnm->mkScope(body, assertions); + d_finalProof = d_pnm->mkScope(pfn, assertions); Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } -void PfManager::printProof(ProofGenerator* pg, Assertions& as) +void PfManager::printProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df) { Trace("smt-proof") << "PfManager::printProof: start" << std::endl; - std::shared_ptr fp = getFinalProof(pg, as); + 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 - // leanPrinter(out, fp.get()); std::ostream& out = *options::out(); out << "(proof\n"; out << *fp; out << "\n)\n"; } -void PfManager::checkProof(ProofGenerator* pg, Assertions& as) +void PfManager::checkProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df) { Trace("smt-proof") << "PfManager::checkProof: start" << std::endl; - std::shared_ptr fp = getFinalProof(pg, as); - Trace("smt-proof") << "PfManager::checkProof: returned " << *fp.get() - << std::endl; + std::shared_ptr fp = getFinalProof(pfn, as, df); + Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get() + << std::endl; } ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); } @@ -138,14 +141,40 @@ smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const return d_pppg.get(); } -std::shared_ptr PfManager::getFinalProof(ProofGenerator* pg, - Assertions& as) +std::shared_ptr PfManager::getFinalProof( + std::shared_ptr pfn, Assertions& as, DefinedFunctionMap& df) { - context::CDList* al = as.getAssertionList(); - setFinalProof(pg, al); + setFinalProof(pfn, as, df); Assert(d_finalProof); return d_finalProof; } +void PfManager::getAssertions(Assertions& as, + DefinedFunctionMap& df, + std::vector& assertions) +{ + context::CDList* al = as.getAssertionList(); + Assert(al != nullptr); + for (context::CDList::const_iterator i = al->begin(); i != al->end(); + ++i) + { + assertions.push_back(*i); + } + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair& dfn : df) + { + Node def = dfn.second.getFormula(); + const std::vector& formals = dfn.second.getFormals(); + if (!formals.empty()) + { + Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals); + def = nm->mkNode(kind::LAMBDA, bvl, def); + } + // assume the (possibly higher order) equality + Node eq = dfn.first.eqNode(def); + assertions.push_back(eq); + } +} + } // namespace smt } // namespace CVC4 diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 1916f0162..be05fc2f7 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -17,6 +17,7 @@ #ifndef CVC4__SMT__PROOF_MANAGER_H #define CVC4__SMT__PROOF_MANAGER_H +#include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node.h" #include "expr/proof_checker.h" @@ -32,6 +33,7 @@ class SmtEngine; namespace smt { class Assertions; +class DefinedFunction; /** * This class is responsible for managing the proof output of SmtEngine, as @@ -39,31 +41,41 @@ class Assertions; */ class PfManager { + /** The type of our internal map of defined functions */ + using DefinedFunctionMap = + context::CDHashMap; + public: PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** * Print the proof on the output channel of the current options in scope. * - * The argument pg is the module that can provide a proof for false in the - * current context. + * The argument pfn is the proof for false in the current context. * * Throws an assertion failure if pg cannot provide a closed proof with - * respect to assertions in as. + * respect to assertions in as and df. For the latter, entries in the defined + * function map correspond to equalities of the form (= f (lambda (...) t)), + * which are considered assertions in the final proof. */ - void printProof(ProofGenerator* pg, Assertions& as); + void printProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df); /** * Check proof, same as above, without printing. */ - void checkProof(ProofGenerator* pg, Assertions& as); + void checkProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df); /** * Get final proof. * - * The argument pg is the module that can provide a proof for false in the - * current context. + * The argument pfn is the proof for false in the current context. */ - std::shared_ptr getFinalProof(ProofGenerator* pg, Assertions& as); + std::shared_ptr getFinalProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df); //--------------------------- access to utilities /** Get a pointer to the ProofChecker owned by this. */ ProofChecker* getProofChecker() const; @@ -74,10 +86,18 @@ class PfManager //--------------------------- end access to utilities private: /** - * Set final proof, which initializes d_finalProof to the proof of false - * from pg, postprocesses it, and stores it in d_finalProof. + * Set final proof, which initializes d_finalProof to the given proof node of + * false, postprocesses it, and stores it in d_finalProof. + */ + void setFinalProof(std::shared_ptr pfn, + Assertions& as, + DefinedFunctionMap& df); + /** + * Get assertions from the assertions */ - void setFinalProof(ProofGenerator* pg, context::CDList* al); + void getAssertions(Assertions& as, + DefinedFunctionMap& df, + std::vector& assertions); /** The false node */ Node d_false; /** For the new proofs module */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2faad7961..81294722f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -328,6 +328,8 @@ SmtEngine::~SmtEngine() #ifdef CVC4_PROOF d_proofManager.reset(nullptr); #endif + d_rewriter.reset(nullptr); + d_pfManager.reset(nullptr); d_absValues.reset(nullptr); d_asserts.reset(nullptr); @@ -951,6 +953,12 @@ 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) @@ -958,6 +966,20 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, checkModel(); } } + // Check that UNSAT results generate a proof correctly. + if (options::checkProofsNew() || options::proofNewEagerChecking()) + { + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + if ((options::checkProofsNew() || options::proofNewEagerChecking()) + && !options::proofNew()) + { + throw ModalException( + "Cannot check-proofs-new because proof-new was disabled."); + } + checkProof(); + } + } // Check that UNSAT results generate an unsat core correctly. if(options::checkUnsatCores()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -1360,6 +1382,20 @@ Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } +void SmtEngine::checkProof() +{ + Assert(options::proofNew()); + // internal check the proof + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + Assert(pe->getProof() != nullptr); + std::shared_ptr pePfn = pe->getProof(); + if (options ::checkProofsNew()) + { + d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions); + } +} + UnsatCore SmtEngine::getUnsatCoreInternal() { #if IS_PROOFS_BUILD @@ -1460,6 +1496,25 @@ UnsatCore SmtEngine::getUnsatCore() { return getUnsatCoreInternal(); } +void SmtEngine::printProof() +{ + if (d_pfManager == nullptr) + { + throw RecoverableModalException("Cannot print proof, no proof manager."); + } + if (getSmtMode() != SmtMode::UNSAT) + { + throw RecoverableModalException( + "Cannot print proof unless immediately preceded by " + "UNSAT/ENTAILED."); + } + 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); +} + void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); finishInit(); @@ -1664,6 +1719,7 @@ void SmtEngine::resetAssertions() // push the state to maintain global context around everything d_state->setup(); + // reset SmtSolver, which will construct a new prop engine d_smtSolver->resetAssertions(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a55428b55..bce086202 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -534,7 +534,13 @@ class CVC4_PUBLIC SmtEngine /** Print all instantiations made by the quantifiers module. */ void printInstantiations(std::ostream& out); - + /** + * Print the current proof. This method should be called after an UNSAT + * response. It gets the proof of false from the PropEngine and passes + * it to the ProofManager, which post-processes the proof and prints it + * in the proper format. + */ + void printProof(); /** * Print solution for synthesis conjectures found by counter-example guided * instantiation module. @@ -870,6 +876,9 @@ class CVC4_PUBLIC SmtEngine /** Set solver instance that owns this SmtEngine. */ void setSolver(api::Solver* solver) { d_solver = solver; } + /** Get a pointer to the (new) PfManager owned by this SmtEngine. */ + smt::PfManager* getPfManager() { return d_pfManager.get(); }; + /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ StatisticsRegistry* getStatisticsRegistry() { @@ -884,6 +893,14 @@ class CVC4_PUBLIC SmtEngine */ UnsatCore getUnsatCoreInternal(); + /** + * Check that a generated proof checks. This method is the same as printProof, + * but does not print the proof. Like that method, it should be called + * after an UNSAT response. It ensures that a well-formed proof of false + * can be constructed by the combination of the PropEngine and ProofManager. + */ + void checkProof(); + /** * Check that an unsatisfiable core is indeed unsatisfiable. */ -- 2.30.2