From 4ae747b98f58c61f95770aa7d2bec818d486433b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Oct 2020 17:18:02 -0500 Subject: [PATCH] (proof-new) Change merge policy for proof node updater (#5242) This updates the proof node updater with a mergeSubproofs field which automatically merges subproofs in the same SCOPE that prove the same thing. This is currently enabled by default, it is now configurable and disabled by default. --- src/expr/proof_node_updater.cpp | 120 +++++++++++++++++++++----------- src/expr/proof_node_updater.h | 30 +++++++- 2 files changed, 106 insertions(+), 44 deletions(-) diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 295d839e1..ac04baa6f 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -33,8 +33,12 @@ bool ProofNodeUpdaterCallback::update(Node res, } ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, - ProofNodeUpdaterCallback& cb) - : d_pnm(pnm), d_cb(cb), d_debugFreeAssumps(false) + ProofNodeUpdaterCallback& cb, + bool mergeSubproofs) + : d_pnm(pnm), + d_cb(cb), + d_debugFreeAssumps(false), + d_mergeSubproofs(mergeSubproofs) { } @@ -60,11 +64,14 @@ void ProofNodeUpdater::process(std::shared_ptr pf) } } } - processInternal(pf, d_freeAssumps); + std::vector> traversing; + processInternal(pf, d_freeAssumps, traversing); } -void ProofNodeUpdater::processInternal(std::shared_ptr pf, - const std::vector& fa) +void ProofNodeUpdater::processInternal( + std::shared_ptr pf, + const std::vector& fa, + std::vector>& traversing) { Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; std::unordered_map, bool> visited; @@ -86,33 +93,39 @@ void ProofNodeUpdater::processInternal(std::shared_ptr pf, res = cur->getResult(); if (it == visited.end()) { - itc = resCache.find(res); - if (itc != resCache.end()) + if (d_mergeSubproofs) { - // already have a proof - visited[cur] = true; - d_pnm->updateNode(cur.get(), itc->second.get()); - } - else - { - visited[cur] = false; - // 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) + itc = resCache.find(res); + if (itc != resCache.end()) { - // no further changes should be made to cur according to the callback - Trace("pf-process-debug") - << "...marked to not continue update." << std::endl; + // already have a proof, merge it into this one + visited[cur] = true; + d_pnm->updateNode(cur.get(), itc->second.get()); continue; } - visit.push_back(cur); + } + // run update to a fixed point + bool continueUpdate = true; + while (runUpdate(cur, fa, continueUpdate) && continueUpdate) + { + Trace("pf-process-debug") << "...updated proof." << std::endl; + } + visited[cur] = !continueUpdate; + 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; + runFinalize(cur, fa, resCache); + continue; + } + traversing.push_back(cur); + visit.push_back(cur); + if (d_mergeSubproofs) + { // 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. + // this method. This is not necessary if we are not merging subproofs. if (cur->getRule() == PfRule::SCOPE && cur != pf) { std::vector nfa; @@ -127,31 +140,32 @@ void ProofNodeUpdater::processInternal(std::shared_ptr pf, } // Process in new call separately, since we should not cache // the results of proofs that have a different scope. - processInternal(cur, nfa); + processInternal(cur, nfa, traversing); continue; } - const std::vector>& ccp = cur->getChildren(); - // now, process children - for (const std::shared_ptr& cp : ccp) + } + const std::vector>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr& cp : ccp) + { + if (std::find(traversing.begin(), traversing.end(), cp) + != traversing.end()) { - visit.push_back(cp); + Unhandled() + << "ProofNodeUpdater::processInternal: cyclic proof! (use " + "--proof-new-eager-checking)" + << std::endl; } + visit.push_back(cp); } } else if (!it->second) { + Assert(!traversing.empty()); + traversing.pop_back(); 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"); - } + // finalize the node + runFinalize(cur, fa, resCache); } } while (!visit.empty()); Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; @@ -212,6 +226,28 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, return false; } +void ProofNodeUpdater::runFinalize( + std::shared_ptr cur, + const std::vector& fa, + std::map>& resCache) +{ + if (d_mergeSubproofs) + { + Node res = cur->getResult(); + // cache result if we are merging subproofs + 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"); + } +} + void ProofNodeUpdater::setDebugFreeAssumptions( const std::vector& freeAssumps) { diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 069b625df..d4c2e8756 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -75,7 +75,15 @@ class ProofNodeUpdaterCallback class ProofNodeUpdater { public: - ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb); + /** + * @param pnm The proof node manager we are using + * @param cb The callback to apply to each node + * @param mergeSubproofs Whether to automatically merge subproofs within + * the same SCOPE that prove the same fact. + */ + ProofNodeUpdater(ProofNodeManager* pnm, + ProofNodeUpdaterCallback& cb, + bool mergeSubproofs = false); /** * Post-process, which performs the main post-processing technique described * above. @@ -99,9 +107,17 @@ class ProofNodeUpdater /** * Post-process, which performs the main post-processing technique described * above. + * + * @param pf The proof to process + * @param fa The assumptions of the scope that fa is a subproof of with + * respect to the original proof. For example, if (SCOPE P :args (A B)), we + * may call this method on P with fa = { A, B }. + * @param traversing The list of proof nodes we are currently traversing + * beneath. This is used for checking for cycles in the overall proof. */ void processInternal(std::shared_ptr pf, - const std::vector& fa); + const std::vector& fa, + std::vector>& traversing); /** * Update proof node cur based on the callback. This modifies curr using * ProofNodeManager::updateNode based on the proof node constructed to @@ -112,10 +128,20 @@ class ProofNodeUpdater bool runUpdate(std::shared_ptr cur, const std::vector& fa, bool& continueUpdate); + /** + * Finalize the node cur. This is called at the moment that it is established + * that cur will appear in the final proof. We do any final debug checking + * and add it to the results cache resCache if we are merging subproofs. + */ + void runFinalize(std::shared_ptr cur, + const std::vector& fa, + std::map>& resCache); /** Are we debugging free assumptions? */ bool d_debugFreeAssumps; /** The initial free assumptions */ std::vector d_freeAssumps; + /** Whether we are merging subproofs */ + bool d_mergeSubproofs; }; } // namespace CVC4 -- 2.30.2