From c789e8510ffa430f398bdc9eee2101e80c7c27de Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 29 Sep 2020 10:20:02 -0300 Subject: [proof-new] Updates to proof node updater (#5156) --- src/smt/proof_post_processor.cpp | 6 ++++-- src/smt/proof_post_processor.h | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) (limited to 'src/smt') diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index e90cbd9e0..306035516 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -49,7 +49,8 @@ void ProofPostprocessCallback::setEliminateRule(PfRule rule) d_elimRules.insert(rule); } -bool ProofPostprocessCallback::shouldUpdate(ProofNode* pn) +bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, + bool& continueUpdate) { return d_elimRules.find(pn->getRule()) != d_elimRules.end(); } @@ -617,7 +618,8 @@ void ProofPostprocessFinalCallback::initializeUpdate() d_pedanticFailureOut.str(""); } -bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode* pn) +bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, + bool& continueUpdate) { PfRule r = pn->getRule(); if (Trace.isOn("final-pf-hole")) diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 41a0531a5..b65519c6d 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -53,7 +53,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback */ void setEliminateRule(PfRule rule); /** Should proof pn be updated? */ - bool shouldUpdate(ProofNode* pn) override; + bool shouldUpdate(std::shared_ptr pn, + bool& continueUpdate) override; /** Update the proof rule application. */ bool update(Node res, PfRule id, @@ -162,7 +163,8 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback */ void initializeUpdate(); /** Should proof pn be updated? Returns false, adds to stats. */ - bool shouldUpdate(ProofNode* pn) override; + bool shouldUpdate(std::shared_ptr pn, + bool& continueUpdate) override; /** was pedantic failure */ bool wasPedanticFailure(std::ostream& out) const; -- cgit v1.2.3