[proof-new] Adds a proof post processor for the Prop Engine (#5161)

The post processor connects the two proofs in the prop engine: the refutation proof in the SAT solver and the CNF transformation proof in the CNF stream. The proof generators from theory engine in the latter are also expanded during the connection.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fc251e0ec0566278ceef20653fb0b4757130e37c..23d9675b49cd7d1f9bb0e068affaf0e033ff7bfc 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -192,6 +192,8 @@ libcvc4_add_sources(
   prop/sat_solver_factory.cpp
   prop/sat_solver_factory.h
   prop/bv_sat_solver_notify.h
+  prop/proof_post_processor.cpp
+  prop/proof_post_processor.h
   prop/sat_proof_manager.cpp
   prop/sat_proof_manager.h
   prop/sat_solver_types.cpp

diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp
new file mode 100644 (file)
index 0000000..4418057
--- /dev/null
+++ b/src/prop/proof_post_processor.cpp
@@ -0,0 +1,108 @@
+/*********************                                                        */
+/*! \file proof_post_processor.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 the module for processing proof nodes in the prop
+ ** engine
+ **/
+
+#include "prop/proof_post_processor.h"
+
+#include "theory/builtin/proof_checker.h"
+
+namespace CVC4 {
+namespace prop {
+
+ProofPostprocessCallback::ProofPostprocessCallback(
+    ProofNodeManager* pnm, ProofCnfStream* proofCnfStream)
+    : d_pnm(pnm), d_proofCnfStream(proofCnfStream)
+{
+}
+
+void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); }
+
+bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                            bool& continueUpdate)
+{
+  bool result = pn->getRule() == PfRule::ASSUME
+                && d_proofCnfStream->hasProofFor(pn->getResult());
+  // check if should continue traversing
+  if (d_proofCnfStream->isBlocked(pn))
+  {
+    continueUpdate = false;
+    result = false;
+  }
+  return result;
+}
+
+bool ProofPostprocessCallback::update(Node res,
+                                      PfRule id,
+                                      const std::vector<Node>& children,
+                                      const std::vector<Node>& args,
+                                      CDProof* cdp,
+                                      bool& continueUpdate)
+{
+  Trace("prop-proof-pp-debug")
+      << "- Post process " << id << " " << children << " / " << args << "\n";
+  Assert(id == PfRule::ASSUME);
+  // we cache based on the assumption node, not the proof node, since there
+  // may be multiple occurrences of the same node.
+  Node f = args[0];
+  std::shared_ptr<ProofNode> pfn;
+  std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
+      d_assumpToProof.find(f);
+  if (it != d_assumpToProof.end())
+  {
+    Trace("prop-proof-pp-debug") << "...already computed" << std::endl;
+    pfn = it->second;
+  }
+  else
+  {
+    Assert(d_proofCnfStream != nullptr);
+    // get proof from proof cnf stream
+    pfn = d_proofCnfStream->getProofFor(f);
+    Assert(pfn != nullptr && pfn->getResult() == f);
+    if (Trace.isOn("prop-proof-pp"))
+    {
+      Trace("prop-proof-pp") << "=== Connect CNF proof for: " << f << "\n";
+      Trace("prop-proof-pp") << *pfn.get() << "\n";
+    }
+    d_assumpToProof[f] = pfn;
+  }
+  // connect the proof
+  cdp->addProof(pfn);
+  // do not recursively process the result
+  continueUpdate = false;
+  // moreover block the fact f so that its proof node is not traversed if we run
+  // this post processor again (which can happen in incremental benchmarks)
+  d_proofCnfStream->addBlocked(pfn);
+  return true;
+}
+
+ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
+                                     ProofCnfStream* proofCnfStream)
+    : d_cb(pnm, proofCnfStream), d_pnm(pnm)
+{
+}
+
+ProofPostproccess::~ProofPostproccess() {}
+
+void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
+{
+  // Initialize the callback, which computes necessary static information about
+  // how to process, including how to process assumptions in pf.
+  d_cb.initializeUpdate();
+  // now, process
+  ProofNodeUpdater updater(d_pnm, d_cb);
+  updater.process(pf);
+}
+
+}  // namespace prop
+}  // namespace CVC4

diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
new file mode 100644 (file)
index 0000000..ced3e5b
--- /dev/null
+++ b/src/prop/proof_post_processor.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \file proof_post_processor.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 The module for processing proof nodes in the prop engine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H
+#define CVC4__PROP__PROOF_POST_PROCESSOR_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/proof_node_updater.h"
+#include "prop/proof_cnf_stream.h"
+
+namespace CVC4 {
+
+namespace prop {
+
+/**
+ * A callback class used by PropEngine for post-processing proof nodes by
+ * connecting proofs of resolution, whose leaves are clausified preprocessed
+ * assertions and lemmas, with the CNF transformation of these formulas, while
+ * expanding the generators of lemmas.
+ */
+class ProofPostprocessCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  ProofPostprocessCallback(ProofNodeManager* pnm,
+                           ProofCnfStream* proofCnfStream);
+  ~ProofPostprocessCallback() {}
+  /**
+   * Initialize, called once for each new ProofNode to process. This initializes
+   * static information to be used by successive calls to update. For this
+   * callback it resets d_assumpToProof.
+   */
+  void initializeUpdate();
+  /** Should proof pn be updated?
+   *
+   * For this callback a proof node is updatable if it's an assumption for which
+   * the proof cnf straem has a proof. However if the proof node is blocked
+   * (which is the case for proof nodes introduced into the proof cnf stream's
+   * proof via expansion of its generators) then traversal is the proof node is
+   * cancelled, i.e., continueUpdate is set to false.
+   */
+  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    bool& continueUpdate) override;
+  /** Update the proof rule application.
+   *
+   * Replaces assumptions by their proof in proof cnf stream. Note that in doing
+   * this the proof node is blocked, so that future post-processing does not
+   * traverse it.
+   *
+   * This method uses the cache in d_assumpToProof to avoid recomputing proofs
+   * for the same assumption (in the same scope).
+   */
+  bool update(Node res,
+              PfRule id,
+              const std::vector<Node>& children,
+              const std::vector<Node>& args,
+              CDProof* cdp,
+              bool& continueUpdate) override;
+
+ private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The cnf stream proof generator */
+  ProofCnfStream* d_proofCnfStream;
+  //---------------------------------reset at the begining of each update
+  /** Mapping assumptions to their proof from cnf transformation */
+  std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
+  //---------------------------------end reset at the begining of each update
+};
+
+/**
+ * The proof postprocessor module. This postprocesses the refutation proof
+ * produced by the SAT solver. Its main task is to connect the refutation's
+ * assumptions to the CNF transformation proof in ProofCnfStream.
+ */
+class ProofPostproccess
+{
+ public:
+  ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream);
+  ~ProofPostproccess();
+  /** post-process
+   *
+   * The post-processing is done via a proof node updater run on pf with this
+   * class's callback d_cb.
+   */
+  void process(std::shared_ptr<ProofNode> pf);
+
+ private:
+  /** The post process callback */
+  ProofPostprocessCallback d_cb;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace prop
+}  // namespace CVC4
+
+#endif