diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 17 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.h | 13 |
2 files changed, 26 insertions, 4 deletions
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: |