diff options
| -rw-r--r-- | src/expr/proof_node_updater.cpp | 2 | ||||
| -rw-r--r-- | src/expr/proof_node_updater.h | 10 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 6 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.h | 6 |
4 files changed, 17 insertions, 7 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index b97d27c05..295d839e1 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -162,7 +162,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, bool& continueUpdate) { // should it be updated? - if (!d_cb.shouldUpdate(cur.get())) + if (!d_cb.shouldUpdate(cur, continueUpdate)) { return false; } diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 63e764d20..069b625df 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -35,8 +35,14 @@ class ProofNodeUpdaterCallback public: ProofNodeUpdaterCallback(); virtual ~ProofNodeUpdaterCallback(); - /** Should proof pn be updated? */ - virtual bool shouldUpdate(ProofNode* pn) = 0; + /** Should proof pn be updated? + * + * @param pn the proof node that maybe should be updated + * @param continueUpdate whether we should continue recursively updating pn + * @return whether we should run the update method on pn + */ + virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn, + bool& continueUpdate) = 0; /** * 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 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<ProofNode> 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<ProofNode> 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<ProofNode> 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<ProofNode> pn, + bool& continueUpdate) override; /** was pedantic failure */ bool wasPedanticFailure(std::ostream& out) const; |