(proof-new) Updates to proof node updater algorithm (#5088)

This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.

This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.

1 files changed, 14 insertions, 3 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 197cdd4b7..bb8a7c0c1 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -58,7 +58,8 @@ bool ProofPostprocessCallback::update(Node res,
                                       PfRule id,
                                       const std::vector<Node>& children,
                                       const std::vector<Node>& args,
-                                      CDProof* cdp)
+                                      CDProof* cdp,
+                                      bool& continueUpdate)
 {
   Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children
                               << " / " << args << std::endl;
@@ -113,6 +114,16 @@ bool ProofPostprocessCallback::update(Node res,
   return !ret.isNull();
 }
 
+bool ProofPostprocessCallback::updateInternal(Node res,
+                                              PfRule id,
+                                              const std::vector<Node>& children,
+                                              const std::vector<Node>& args,
+                                              CDProof* cdp)
+{
+  bool continueUpdate = true;
+  return update(res, id, children, args, cdp, continueUpdate);
+}
+
 Node ProofPostprocessCallback::expandMacros(PfRule id,
                                             const std::vector<Node>& children,
                                             const std::vector<Node>& args,
@@ -150,7 +161,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       {
         Node eq = t.eqNode(ts);
         // apply SUBS proof rule if necessary
-        if (!update(eq, PfRule::SUBS, children, sargs, cdp))
+        if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp))
         {
           // if not elimianted, add as step
           cdp->addStep(eq, PfRule::SUBS, children, sargs);
@@ -181,7 +192,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     {
       Node eq = ts.eqNode(tr);
       // apply REWRITE proof rule
-      if (!update(eq, PfRule::REWRITE, {}, rargs, cdp))
+      if (!updateInternal(eq, PfRule::REWRITE, {}, rargs, cdp))
       {
         // if not elimianted, add as step
         cdp->addStep(eq, PfRule::REWRITE, {}, rargs);