[proof-new] Updates to proof node updater (#5156)

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index b97d27c05b385102a0538fbeff3dbecd059f7c76..295d839e15461330c46e0f6277da1d38bc154687 100644 (file)
--- 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 63e764d20a9b7bad8e7bc1b2024211ae37a25be6..069b625dfeed519bf249d0ecd7da372b2ee84124 100644 (file)
--- 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 e90cbd9e0e082491da8cd3f8a010faf4ea86c1c0..3060355167604ec037ca1d86b0a0a2d6159fe9f0 100644 (file)
--- 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 41a0531a5d76b810b8de049dc0d45527231a6aaf..b65519c6d9506ff77650104a9fd2a62306549946 100644 (file)
--- 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;