(proof-new) Minor changes to proof node updater (#5011)

This includes some changes to proof node updater that are not currently on master.

This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.

It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.

2 files changed, 91 insertions, 32 deletions

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index 1e8fe4e7d..55eebb0d1 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -15,12 +15,22 @@
 #include "expr/proof_node_updater.h"
 
 #include "expr/lazy_proof.h"
+#include "expr/proof_node_algorithm.h"
 
 namespace CVC4 {
 
 ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
 ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
 
+bool ProofNodeUpdaterCallback::update(Node res,
+                                      PfRule id,
+                                      const std::vector<Node>& children,
+                                      const std::vector<Node>& args,
+                                      CDProof* cdp)
+{
+  return false;
+}
+
 ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
                                    ProofNodeUpdaterCallback& cb)
     : d_pnm(pnm), d_cb(cb)
@@ -30,53 +40,95 @@ ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
 void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
 {
   Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
-  std::unordered_set<ProofNode*> visited;
-  std::unordered_set<ProofNode*>::iterator it;
+  std::unordered_map<ProofNode*, bool> visited;
+  std::unordered_map<ProofNode*, bool>::iterator it;
   std::vector<ProofNode*> visit;
   ProofNode* cur;
   visit.push_back(pf.get());
+  std::map<Node, ProofNode*>::iterator itc;
+  // A cache from formulas to proof nodes that are in the current scope.
+  // Notice that we make a fresh recursive call to process if the current
+  // rule is SCOPE below.
+  std::map<Node, ProofNode*> resCache;
+  TNode res;
   do
   {
     cur = visit.back();
     visit.pop_back();
     it = visited.find(cur);
+    res = cur->getResult();
     if (it == visited.end())
     {
-      visited.insert(cur);
-      // should it be updated?
-      if (d_cb.shouldUpdate(cur))
+      itc = resCache.find(res);
+      if (itc != resCache.end())
       {
-        PfRule id = cur->getRule();
-        // use CDProof to open a scope for which the callback updates
-        CDProof cpf(d_pnm);
-        const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
-        std::vector<Node> ccn;
-        for (const std::shared_ptr<ProofNode>& cp : cc)
-        {
-          Node cpres = cp->getResult();
-          ccn.push_back(cpres);
-          // store in the proof
-          cpf.addProof(cp);
-        }
-        // only if the callback updated the node
-        if (d_cb.update(id, ccn, cur->getArguments(), &cpf))
-        {
-          // build the proof, which should be closed
-          std::shared_ptr<ProofNode> npn = cpf.getProofFor(cur->getResult());
-          Assert(npn->isClosed());
-          // then, update the original proof node based on this one
-          d_pnm->updateNode(cur, npn.get());
-        }
+        // already have a proof
+        visited[cur] = true;
+        d_pnm->updateNode(cur, itc->second);
       }
-      const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
-      // now, process children
-      for (const std::shared_ptr<ProofNode>& cp : ccp)
+      else
       {
-        visit.push_back(cp.get());
+        visited[cur] = false;
+        // run update first
+        runUpdate(cur);
+        visit.push_back(cur);
+        const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
+        // now, process children
+        for (const std::shared_ptr<ProofNode>& cp : ccp)
+        {
+          if (cp->getRule() == PfRule::SCOPE)
+          {
+            // Process in new call separately, since we should not cache
+            // the results of proofs that have a different scope.
+            process(cp);
+            continue;
+          }
+          visit.push_back(cp.get());
+        }
       }
     }
+    else if (!it->second)
+    {
+      visited[cur] = true;
+      // cache result
+      resCache[res] = cur;
+    }
   } while (!visit.empty());
   Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
 }
 
+void ProofNodeUpdater::runUpdate(ProofNode* cur)
+{
+  // should it be updated?
+  if (!d_cb.shouldUpdate(cur))
+  {
+    return;
+  }
+  PfRule id = cur->getRule();
+  // use CDProof to open a scope for which the callback updates
+  CDProof cpf(d_pnm);
+  const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
+  std::vector<Node> ccn;
+  for (const std::shared_ptr<ProofNode>& cp : cc)
+  {
+    Node cpres = cp->getResult();
+    ccn.push_back(cpres);
+    // store in the proof
+    cpf.addProof(cp);
+  }
+  Trace("pf-process-debug")
+      << "Updating (" << cur->getRule() << ")..." << std::endl;
+  Node res = cur->getResult();
+  // only if the callback updated the node
+  if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf))
+  {
+    std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
+    // then, update the original proof node based on this one
+    Trace("pf-process-debug") << "Update node..." << std::endl;
+    d_pnm->updateNode(cur, npn.get());
+    Trace("pf-process-debug") << "...update node finished." << std::endl;
+  }
+  Trace("pf-process-debug") << "..finished" << std::endl;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index be7a120ee..061a12310 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -42,10 +42,11 @@ class ProofNodeUpdaterCallback
    * the proof changed. It can be assumed that cdp contains proofs of each
    * fact in children.
    */
-  virtual bool update(PfRule id,
+  virtual bool update(Node res,
+                      PfRule id,
                       const std::vector<Node>& children,
                       const std::vector<Node>& args,
-                      CDProof* cdp) = 0;
+                      CDProof* cdp);
 };
 
 /**
@@ -72,6 +73,12 @@ class ProofNodeUpdater
   ProofNodeManager* d_pnm;
   /** The callback */
   ProofNodeUpdaterCallback& d_cb;
+  /**
+   * Update proof node cur based on the callback. This modifies curr using
+   * ProofNodeManager::updateNode based on the proof node constructed to
+   * replace it by the callback.
+   */
+  void runUpdate(ProofNode* cur);
 };
 
 }  // namespace CVC4