diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-29 10:20:02 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-29 10:20:02 -0300 |
| commit | c789e8510ffa430f398bdc9eee2101e80c7c27de (patch) | |
| tree | 070226dc0f7a2c480069eafda28287fa84d1f046 /src/smt | |
| parent | d11d694f73ec0520cb251304f9508b3355b93725 (diff) | |
[proof-new] Updates to proof node updater (#5156)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 6 | ||||
| -rw-r--r-- | src/smt/proof_post_processor.h | 6 |
2 files changed, 8 insertions, 4 deletions
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; |