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/proof_post_processor.h | |
| parent | d11d694f73ec0520cb251304f9508b3355b93725 (diff) | |
[proof-new] Updates to proof node updater (#5156)
Diffstat (limited to 'src/smt/proof_post_processor.h')
| -rw-r--r-- | src/smt/proof_post_processor.h | 6 |
1 files changed, 4 insertions, 2 deletions
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; |