diff options
| -rw-r--r-- | src/expr/proof_node_updater.cpp | 142 | ||||
| -rw-r--r-- | src/expr/proof_node_updater.h | 37 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 17 | ||||
| -rw-r--r-- | 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<Node>& children, const std::vector<Node>& 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<ProofNode> 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<Node> 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<ProofNode> pf, + const std::vector<Node>& fa) +{ Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; - std::unordered_map<ProofNode*, bool> visited; - std::unordered_map<ProofNode*, bool>::iterator it; - std::vector<ProofNode*> visit; - ProofNode* cur; - visit.push_back(pf.get()); - std::map<Node, ProofNode*>::iterator itc; + std::unordered_map<std::shared_ptr<ProofNode>, bool> visited; + std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it; + std::vector<std::shared_ptr<ProofNode>> visit; + std::shared_ptr<ProofNode> cur; + visit.push_back(pf); + std::map<Node, std::shared_ptr<ProofNode>>::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<Node, ProofNode*> resCache; - TNode res; + std::map<Node, std::shared_ptr<ProofNode>> resCache; + Node res; do { cur = visit.back(); @@ -64,26 +91,50 @@ void ProofNodeUpdater::process(std::shared_ptr<ProofNode> 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<Node> nfa; + // if we are debugging free assumptions, update the set + if (d_debugFreeAssumps) + { + nfa.insert(nfa.end(), fa.begin(), fa.end()); + const std::vector<Node>& 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<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); // now, process children for (const std::shared_ptr<ProofNode>& 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<ProofNode> 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<ProofNode> cur, + const std::vector<Node>& 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<ProofNode> npn = cpf.getProofFor(res); + std::vector<Node> 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<Node>& 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<Node>& children, const std::vector<Node>& args, - CDProof* cdp); + CDProof* cdp, + bool& continueUpdate); }; /** @@ -68,17 +76,40 @@ class ProofNodeUpdater */ void process(std::shared_ptr<ProofNode> 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<Node>& 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<ProofNode> pf, + const std::vector<Node>& 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<ProofNode> cur, + const std::vector<Node>& fa, + bool& continueUpdate); + /** Are we debugging free assumptions? */ + bool d_debugFreeAssumps; + /** The initial free assumptions */ + std::vector<Node> 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<Node>& children, const std::vector<Node>& 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<Node>& children, + const std::vector<Node>& args, + CDProof* cdp) +{ + bool continueUpdate = true; + return update(res, id, children, args, cdp, continueUpdate); +} + Node ProofPostprocessCallback::expandMacros(PfRule id, const std::vector<Node>& children, const std::vector<Node>& 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<Node>& children, const std::vector<Node>& args, - CDProof* cdp) override; + CDProof* cdp, + bool& continueUpdate) override; private: /** Common constants */ @@ -97,6 +98,16 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback const std::vector<Node>& 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<Node>& children, + const std::vector<Node>& 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. * Notice the proof of this fact may have open assumptions of the form: |