[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)

Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.

This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.

1 files changed, 17 insertions, 24 deletions

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index 933e5b999..cbd457cd7 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -125,28 +125,21 @@ void ProofNodeUpdater::processInternal(
       }
       traversing.push_back(cur);
       visit.push_back(cur);
-      if (d_mergeSubproofs)
+      // If we are not the top-level proof, we were a scope, or became a scope
+      // after updating, we do a separate recursive call to this method. This
+      // allows us to properly track the assumptions in scope, which is
+      // important for example to merge or to determine updates based on free
+      // assumptions.
+      if (cur->getRule() == PfRule::SCOPE && cur != pf)
       {
-        // If we are not the top-level proof, we were a scope, or became a
-        // scope after updating, we need to make a separate recursive call to
-        // this method. This is not necessary if we are not merging subproofs.
-        if (cur->getRule() == PfRule::SCOPE && cur != pf)
-        {
-          std::vector<Node> nfa;
-          // if we are debugging free assumptions, update the set
-          if (d_debugFreeAssumps)
-          {
-            nfa.insert(nfa.end(), fa.begin(), fa.end());
-            const std::vector<Node>& args = cur->getArguments();
-            nfa.insert(nfa.end(), args.begin(), args.end());
-            Trace("pfnu-debug2")
-                << "Process new scope with " << args << std::endl;
-          }
-          // Process in new call separately, since we should not cache
-          // the results of proofs that have a different scope.
-          processInternal(cur, nfa, traversing);
-          continue;
-        }
+        std::vector<Node> nfa;
+        nfa.insert(nfa.end(), fa.begin(), fa.end());
+        const std::vector<Node>& args = cur->getArguments();
+        nfa.insert(nfa.end(), args.begin(), args.end());
+        Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
+        // Process in new call separately
+        processInternal(cur, nfa, traversing);
+        continue;
       }
       const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
       // now, process children
@@ -180,7 +173,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
                                  bool& continueUpdate)
 {
   // should it be updated?
-  if (!d_cb.shouldUpdate(cur, continueUpdate))
+  if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
   {
     return false;
   }
@@ -196,9 +189,9 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
     // store in the proof
     cpf.addProof(cp);
   }
-  Trace("pf-process-debug")
-      << "Updating (" << cur->getRule() << ")..." << std::endl;
   Node res = cur->getResult();
+  Trace("pf-process-debug")
+      << "Updating (" << cur->getRule() << "): " << res << std::endl;
   // only if the callback updated the node
   if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
   {