(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.

4 files changed, 96 insertions, 35 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5a06df28b..a7c50d1e4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -222,6 +222,8 @@ libcvc4_add_sources(
   smt/preprocess_proof_generator.h
   smt/process_assertions.cpp
   smt/process_assertions.h
+  smt/proof_post_processor.cpp
+  smt/proof_post_processor.h
   smt/set_defaults.cpp
   smt/set_defaults.h
   smt/smt_engine.cpp
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
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5aa2ba987..5ef8b63c6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -860,6 +860,9 @@ class CVC4_PUBLIC SmtEngine
   /** Permit access to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
+  /** Get a pointer to the Rewriter owned by this SmtEngine. */
+  theory::Rewriter* getRewriter() { return d_rewriter.get(); }
+
   /**
    * Get expanded assertions.
    *
@@ -900,9 +903,6 @@ class CVC4_PUBLIC SmtEngine
   /** Get a pointer to the ProofManager owned by this SmtEngine. */
   ProofManager* getProofManager() { return d_proofManager.get(); };
 
-  /** Get a pointer to the Rewriter owned by this SmtEngine. */
-  theory::Rewriter* getRewriter() { return d_rewriter.get(); }
-
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
   StatisticsRegistry* getStatisticsRegistry()
   {