From 89c5d4ac65f45f24a7dc0ab76bb2bdb447bdfcda Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Sep 2020 21:38:42 -0500 Subject: [PATCH] (proof-new) Updates to proof node updater algorithm (#5088) This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating. This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update. --- src/expr/proof_node_updater.cpp | 142 +++++++++++++++++++++++++------ src/expr/proof_node_updater.h | 37 +++++++- src/smt/proof_post_processor.cpp | 17 +++- src/smt/proof_post_processor.h | 13 ++- 4 files changed, 176 insertions(+), 33 deletions(-) diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 55eebb0d1..3368cb856 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -26,31 +26,58 @@ bool ProofNodeUpdaterCallback::update(Node res, PfRule id, const std::vector& children, const std::vector& args, - CDProof* cdp) + CDProof* cdp, + bool& continueUpdate) { return false; } ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb) - : d_pnm(pnm), d_cb(cb) + : d_pnm(pnm), d_cb(cb), d_debugFreeAssumps(false) { } void ProofNodeUpdater::process(std::shared_ptr pf) +{ + if (d_debugFreeAssumps) + { + if (Trace.isOn("pfnu-debug")) + { + Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl; + Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl; + Trace("pfnu-debug") << "Expected free assumptions: " << std::endl; + for (const Node& fa : d_freeAssumps) + { + Trace("pfnu-debug") << "- " << fa << std::endl; + } + std::vector assump; + expr::getFreeAssumptions(pf.get(), assump); + Trace("pfnu-debug") << "Current free assumptions: " << std::endl; + for (const Node& fa : assump) + { + Trace("pfnu-debug") << "- " << fa << std::endl; + } + } + } + processInternal(pf, d_freeAssumps); +} + +void ProofNodeUpdater::processInternal(std::shared_ptr pf, + const std::vector& fa) { Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - ProofNode* cur; - visit.push_back(pf.get()); - std::map::iterator itc; + std::unordered_map, bool> visited; + std::unordered_map, bool>::iterator it; + std::vector> visit; + std::shared_ptr cur; + visit.push_back(pf); + std::map>::iterator itc; // A cache from formulas to proof nodes that are in the current scope. // Notice that we make a fresh recursive call to process if the current // rule is SCOPE below. - std::map resCache; - TNode res; + std::map> resCache; + Node res; do { cur = visit.back(); @@ -64,26 +91,50 @@ void ProofNodeUpdater::process(std::shared_ptr pf) { // already have a proof visited[cur] = true; - d_pnm->updateNode(cur, itc->second); + d_pnm->updateNode(cur.get(), itc->second.get()); } else { visited[cur] = false; - // run update first - runUpdate(cur); + // run update to a fixed point + bool continueUpdate = true; + while (runUpdate(cur, fa, continueUpdate) && continueUpdate) + { + Trace("pf-process-debug") << "...updated proof." << std::endl; + } + if (!continueUpdate) + { + // no further changes should be made to cur according to the callback + Trace("pf-process-debug") + << "...marked to not continue update." << std::endl; + continue; + } visit.push_back(cur); + // If we are not the top-level proof, we were a scope, or became a + // scope after updating, we need to make a separate recursive call to + // this method. + if (cur->getRule() == PfRule::SCOPE && cur != pf) + { + std::vector nfa; + // if we are debugging free assumptions, update the set + if (d_debugFreeAssumps) + { + nfa.insert(nfa.end(), fa.begin(), fa.end()); + const std::vector& args = cur->getArguments(); + nfa.insert(nfa.end(), args.begin(), args.end()); + Trace("pfnu-debug2") + << "Process new scope with " << args << std::endl; + } + // Process in new call separately, since we should not cache + // the results of proofs that have a different scope. + processInternal(cur, nfa); + continue; + } const std::vector>& ccp = cur->getChildren(); // now, process children for (const std::shared_ptr& cp : ccp) { - if (cp->getRule() == PfRule::SCOPE) - { - // Process in new call separately, since we should not cache - // the results of proofs that have a different scope. - process(cp); - continue; - } - visit.push_back(cp.get()); + visit.push_back(cp); } } } @@ -92,17 +143,28 @@ void ProofNodeUpdater::process(std::shared_ptr pf) visited[cur] = true; // cache result resCache[res] = cur; + if (d_debugFreeAssumps) + { + // We have that npn is a node we occurring the final updated version of + // the proof. We can now debug based on the expected set of free + // assumptions. + Trace("pfnu-debug") << "Ensure update closed..." << std::endl; + pfnEnsureClosedWrt( + cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); + } } } while (!visit.empty()); Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; } -void ProofNodeUpdater::runUpdate(ProofNode* cur) +bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, + const std::vector& fa, + bool& continueUpdate) { // should it be updated? - if (!d_cb.shouldUpdate(cur)) + if (!d_cb.shouldUpdate(cur.get())) { - return; + return false; } PfRule id = cur->getRule(); // use CDProof to open a scope for which the callback updates @@ -120,15 +182,43 @@ void ProofNodeUpdater::runUpdate(ProofNode* cur) << "Updating (" << cur->getRule() << ")..." << std::endl; Node res = cur->getResult(); // only if the callback updated the node - if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf)) + if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) { std::shared_ptr npn = cpf.getProofFor(res); + std::vector fullFa; + if (d_debugFreeAssumps) + { + expr::getFreeAssumptions(cur.get(), fullFa); + Trace("pfnu-debug") << "Original proof : " << *cur << std::endl; + } // then, update the original proof node based on this one Trace("pf-process-debug") << "Update node..." << std::endl; - d_pnm->updateNode(cur, npn.get()); + d_pnm->updateNode(cur.get(), npn.get()); Trace("pf-process-debug") << "...update node finished." << std::endl; + if (d_debugFreeAssumps) + { + fullFa.insert(fullFa.end(), fa.begin(), fa.end()); + // We have that npn is a node we occurring the final updated version of + // the proof. We can now debug based on the expected set of free + // assumptions. + Trace("pfnu-debug") << "Ensure update closed..." << std::endl; + pfnEnsureClosedWrt( + npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); + } + Trace("pf-process-debug") << "..finished" << std::endl; + return true; } Trace("pf-process-debug") << "..finished" << std::endl; + return false; +} + +void ProofNodeUpdater::setDebugFreeAssumptions( + const std::vector& freeAssumps) +{ + d_freeAssumps.clear(); + d_freeAssumps.insert( + d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end()); + d_debugFreeAssumps = true; } } // namespace CVC4 diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 061a12310..d5c0a884f 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -41,12 +41,20 @@ class ProofNodeUpdaterCallback * Update the proof rule application, store steps in cdp. Return true if * the proof changed. It can be assumed that cdp contains proofs of each * fact in children. + * + * If continueUpdate is set to false in this method, then the resulting + * proof (the proof of res in cdp) is *not* called back to update by the + * proof node updater, nor are its children recursed. Otherwise, by default, + * the proof node updater will continue updating the resulting proof and will + * recursively update its children. This is analogous to marking REWRITE_DONE + * in a rewrite response. */ virtual bool update(Node res, PfRule id, const std::vector& children, const std::vector& args, - CDProof* cdp); + CDProof* cdp, + bool& continueUpdate); }; /** @@ -68,17 +76,40 @@ class ProofNodeUpdater */ void process(std::shared_ptr pf); + /** + * Set free assumptions to freeAssumps. This indicates that we expect + * the proof we are processing to have free assumptions that are in + * freeAssumps. This enables checking when this is violated, which is + * expensive in general. It is not recommended that this method is called + * by default. + */ + void setDebugFreeAssumptions(const std::vector& freeAssumps); + private: /** The proof node manager */ ProofNodeManager* d_pnm; /** The callback */ ProofNodeUpdaterCallback& d_cb; + /** + * Post-process, which performs the main post-processing technique described + * above. + */ + void processInternal(std::shared_ptr pf, + const std::vector& fa); /** * Update proof node cur based on the callback. This modifies curr using * ProofNodeManager::updateNode based on the proof node constructed to - * replace it by the callback. + * replace it by the callback. Return true if cur was updated. If + * continueUpdate is updated to false, then cur is not updated further + * and its children are not traversed. */ - void runUpdate(ProofNode* cur); + bool runUpdate(std::shared_ptr cur, + const std::vector& fa, + bool& continueUpdate); + /** Are we debugging free assumptions? */ + bool d_debugFreeAssumps; + /** The initial free assumptions */ + std::vector d_freeAssumps; }; } // namespace CVC4 diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 197cdd4b7..bb8a7c0c1 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -58,7 +58,8 @@ bool ProofPostprocessCallback::update(Node res, PfRule id, const std::vector& children, const std::vector& args, - CDProof* cdp) + CDProof* cdp, + bool& continueUpdate) { Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children << " / " << args << std::endl; @@ -113,6 +114,16 @@ bool ProofPostprocessCallback::update(Node res, return !ret.isNull(); } +bool ProofPostprocessCallback::updateInternal(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp) +{ + bool continueUpdate = true; + return update(res, id, children, args, cdp, continueUpdate); +} + Node ProofPostprocessCallback::expandMacros(PfRule id, const std::vector& children, const std::vector& args, @@ -150,7 +161,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, { Node eq = t.eqNode(ts); // apply SUBS proof rule if necessary - if (!update(eq, PfRule::SUBS, children, sargs, cdp)) + if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp)) { // if not elimianted, add as step cdp->addStep(eq, PfRule::SUBS, children, sargs); @@ -181,7 +192,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, { Node eq = ts.eqNode(tr); // apply REWRITE proof rule - if (!update(eq, PfRule::REWRITE, {}, rargs, cdp)) + if (!updateInternal(eq, PfRule::REWRITE, {}, rargs, cdp)) { // if not elimianted, add as step cdp->addStep(eq, PfRule::REWRITE, {}, rargs); diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 6c75af5ce..8c895275a 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -59,7 +59,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback PfRule id, const std::vector& children, const std::vector& args, - CDProof* cdp) override; + CDProof* cdp, + bool& continueUpdate) override; private: /** Common constants */ @@ -96,6 +97,16 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback const std::vector& children, const std::vector& args, CDProof* cdp); + /** + * Update the proof rule application, called during expand macros when + * we wish to apply the update method. This method has the same behavior + * as update apart from ignoring the continueUpdate flag. + */ + bool updateInternal(Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp); /** * Add proof for witness form. This returns the equality t = toWitness(t) * and ensures that the proof of this equality has been added to cdp. -- 2.30.2