Improve subproof merging in proof node updater (cvc5#10123)

Leads to shorter proofs / better proof checking time.

src/proof/proof_node_updater.cpp

@@ -127,7 +127,13 @@ void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
     it = visited.find(cur);
     if (it == visited.end())
     {
-      // check if there is a proof in resCache with the same result
+      // Check if there is a proof in resCache with the same result.
+      // Note that if this returns true, we update the contents of the current
+      // proof. Moreover, parents will replace the reference to this proof.
+      // Thus, replacing the contents of this proof is not (typically)
+      // necessary, but is done anyways in case there are any other references
+      // to this proof that are not handled by this loop, that is, proof
+      // nodes having this as a child that are not subproofs of pf.
       if (checkMergeProof(cur, resCache, cfaMap))
       {
         visited[cur] = true;
@@ -188,7 +194,9 @@ void ProofNodeUpdater::processInternal(std::shared_ptr<ProofNode> pf,
         fa.resize(fa.size() - args.size());
       }
       // maybe found a proof in the meantime, i.e. a subproof of the current
-      // proof with the same result.
+      // proof with the same result. Same as above, updating the contents here
+      // is typically not necessary since references to this proof will be
+      // replaced.
       if (checkMergeProof(cur, resCache, cfaMap))
       {
         visited[cur] = true;
@@ -290,8 +298,7 @@ void ProofNodeUpdater::runFinalize(
     // cache the result if we don't contain an assumption
     if (!expr::containsAssumption(cur.get(), cfaMap, cfaAllowed))
     {
-      Trace("pf-process-debug")
-          << "No assumption pf: " << *cur.get() << std::endl;
+      Trace("pf-process-debug") << "No assumption pf: " << res << std::endl;
       // cache result if we are merging subproofs
       resCache[res] = cur;
       // go back and merge into the non-closed proofs of the same fact
@@ -309,10 +316,39 @@ void ProofNodeUpdater::runFinalize(
     }
     else
     {
-      Trace("pf-process-debug") << "Assumption pf: " << *cur.get() << ", with "
+      Trace("pf-process-debug") << "Assumption pf: " << res << ", with "
                                 << cfaAllowed.size() << std::endl;
       resCacheNcWaiting[res].push_back(cur);
     }
+    // Now, do update of children, that is, we replace children of the current
+    // proof with the representative child in the cache, if they are different.
+    // This is necessary to do here since we only locally update the contents of
+    // a proof when a duplicate is encountered. Updating the reference to a
+    // child is done here.
+    std::map<Node, std::shared_ptr<ProofNode>>::iterator itr;
+    const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
+    std::vector<std::shared_ptr<ProofNode>> newChildren;
+    bool childChanged = false;
+    for (const std::shared_ptr<ProofNode>& cp : ccp)
+    {
+      Node cpres = cp->getResult();
+      itr = resCache.find(cpres);
+      if (itr != resCache.end() && itr->second != cp)
+      {
+        newChildren.emplace_back(itr->second);
+        childChanged = true;
+      }
+      else
+      {
+        newChildren.emplace_back(cp);
+      }
+    }
+    if (childChanged)
+    {
+      ProofNodeManager* pnm = d_env.getProofNodeManager();
+      pnm->updateNode(
+          cur.get(), cur->getRule(), newChildren, cur->getArguments());
+    }
   }
   if (d_debugFreeAssumps)
   {