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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5a06df28b739f1fbe86924c8c5e5706a0cc993fe..a7c50d1e4911db7556787cf3eb19ba82623f485e 100644 (file)
--- 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 1e8fe4e7dea2b058b43522aef5b3c7d0bda30a14..55eebb0d1dba4db945343f6c4b9eacb82ea26465 100644 (file)
--- 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 be7a120ee1988f10f7fbf37c993be9ef132b940b..061a123104d0da32cb45b888703260e9583dfcbd 100644 (file)
--- 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 5aa2ba987461c7828cbd51a104b875c15e36fae7..5ef8b63c62009d26031f3636a1488f8acb88e351 100644 (file)
--- 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()
   {