(proof-new) Proof node updater (#4647)

Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.

Requires #4617.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 5173c076dc560f95ef87eb964da1b3f790a2bc8b..b042b935231f3ff2b6de814dcc975bdb803f4869 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -53,6 +53,8 @@ libcvc4_add_sources(
   proof_node_to_sexpr.h
   proof_node_manager.cpp
   proof_node_manager.h
+  proof_node_updater.cpp
+  proof_node_updater.h
   proof_rule.cpp
   proof_rule.h
   proof_step_buffer.cpp

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
new file mode 100644 (file)
index 0000000..227be21
--- /dev/null
+++ b/src/expr/proof_node_updater.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file proof_node_updater.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of a utility for updating proof nodes
+ **/
+
+#include "expr/proof_node_updater.h"
+
+#include "expr/lazy_proof.h"
+
+
+namespace CVC4 {
+
+ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
+ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
+
+ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
+                                   ProofNodeUpdaterCallback& cb)
+    : d_pnm(pnm), d_cb(cb)
+{
+}
+
+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::vector<ProofNode*> visit;
+  ProofNode* cur;
+  visit.push_back(pf.get());
+  do
+  {
+    cur = visit.back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      // should it be updated?
+      if (d_cb.shouldUpdate(cur))
+      {
+        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());
+        }
+        const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
+        // now, process children
+        for (const std::shared_ptr<ProofNode>& cp : ccp)
+        {
+          visit.push_back(cp.get());
+        }
+      }
+    }
+  } while (!visit.empty());
+  Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
+}
+
+}  // namespace CVC4

diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
new file mode 100644 (file)
index 0000000..be7a120
--- /dev/null
+++ b/src/expr/proof_node_updater.h
@@ -0,0 +1,79 @@
+/*********************                                                        */
+/*! \file proof_node_updater.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A utility for updating proof nodes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_NODE_UPDATER_H
+#define CVC4__EXPR__PROOF_NODE_UPDATER_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/proof.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A virtual callback class for updating ProofNode. An example use case of this
+ * class is to eliminate a proof rule by expansion.
+ */
+class ProofNodeUpdaterCallback
+{
+ public:
+  ProofNodeUpdaterCallback();
+  virtual ~ProofNodeUpdaterCallback();
+  /** Should proof pn be updated? */
+  virtual bool shouldUpdate(ProofNode* pn) = 0;
+  /**
+   * Update the proof rule application, store steps in cdp. Return true if
+   * the proof changed. It can be assumed that cdp contains proofs of each
+   * fact in children.
+   */
+  virtual bool update(PfRule id,
+                      const std::vector<Node>& children,
+                      const std::vector<Node>& args,
+                      CDProof* cdp) = 0;
+};
+
+/**
+ * A generic class for updating ProofNode. It is parameterized by a callback
+ * class. Its process method runs this callback on all subproofs of a provided
+ * ProofNode application that meet some criteria
+ * (ProofNodeUpdaterCallback::shouldUpdate)
+ * and overwrites them based on the update procedure of the callback
+ * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that
+ * should be filled in the callback for each ProofNode to update.
+ */
+class ProofNodeUpdater
+{
+ public:
+  ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb);
+  /**
+   * Post-process, which performs the main post-processing technique described
+   * above.
+   */
+  void process(std::shared_ptr<ProofNode> pf);
+
+ private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The callback */
+  ProofNodeUpdaterCallback& d_cb;
+};
+
+}  // namespace CVC4
+
+#endif