(proof-new) Proof recording for assertions pipeline (#4766)

Adds explicit steps to preprocess proof generator if one is provided.

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index caad369b7719356cd3fda5bae9877d400b9fde38..a6b9531b691e199b5ddb368bb64244f80258c22f 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -28,7 +28,8 @@ AssertionPipeline::AssertionPipeline()
       d_storeSubstsInAsserts(false),
       d_substsIndex(0),
       d_assumptionsStart(0),
-      d_numAssumptions(0)
+      d_numAssumptions(0),
+      d_pppg(nullptr)
 {
 }
 
@@ -40,11 +41,15 @@ void AssertionPipeline::clear()
   d_numAssumptions = 0;
 }
 
-void AssertionPipeline::push_back(Node n, bool isAssumption)
+void AssertionPipeline::push_back(Node n,
+                                  bool isAssumption,
+                                  bool isInput,
+                                  ProofGenerator* pgen)
 {
   d_nodes.push_back(n);
   if (isAssumption)
   {
+    Assert(pgen == nullptr);
     if (d_numAssumptions == 0)
     {
       d_assumptionsStart = d_nodes.size() - 1;
@@ -56,39 +61,60 @@ void AssertionPipeline::push_back(Node n, bool isAssumption)
     Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
     d_numAssumptions++;
   }
+  if (!isInput && isProofEnabled())
+  {
+    // notice this is always called, regardless of whether pgen is nullptr
+    d_pppg->notifyNewAssert(n, pgen);
+  }
+}
+
+void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
+{
+  Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
+  // push back what was proven
+  push_back(trn.getProven(), false, trn.getGenerator());
 }
 
-void AssertionPipeline::replace(size_t i, Node n)
+void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
 {
   PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
+  if (isProofEnabled())
+  {
+    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
+  }
   d_nodes[i] = n;
 }
 
+void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
+{
+  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+  replace(i, trn.getNode(), trn.getGenerator());
+}
+
 void AssertionPipeline::replace(size_t i,
                                 Node n,
-                                const std::vector<Node>& addnDeps)
+                                const std::vector<Node>& addnDeps,
+                                ProofGenerator* pgen)
 {
   PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
         for (const auto& addnDep
              : addnDeps) {
           ProofManager::currentPM()->addDependence(n, addnDep);
         });
+  if (isProofEnabled())
+  {
+    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
+  }
   d_nodes[i] = n;
 }
 
-void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
+void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
 {
-  PROOF(
-      for (const auto& n
-           : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
-  d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
-
-  for (const auto& n : ns)
-  {
-    d_nodes.push_back(n);
-  }
+  d_pppg = pppg;
 }
 
+bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
+
 void AssertionPipeline::enableStoreSubstsInAsserts()
 {
   d_storeSubstsInAsserts = true;

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 5d8f645949e9a9352c2c97051f14842d16301e57..4fa8b5bb40ded27a55900b5f76cb6554ebf50181 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -21,7 +21,11 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/term_formula_removal.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -54,8 +58,17 @@ class AssertionPipeline
    * @param n The assertion/assumption
    * @param isAssumption If true, records that \p n is an assumption. Note that
    * all assumptions have to be added contiguously.
+   * @param isInput If true, n is an input formula (an assumption in the main
+   * body of the overall proof).
+   * @param pg The proof generator who can provide a proof of n. The proof
+   * generator is not required and is ignored if isInput is true.
    */
-  void push_back(Node n, bool isAssumption = false);
+  void push_back(Node n,
+                 bool isAssumption = false,
+                 bool isInput = false,
+                 ProofGenerator* pg = nullptr);
+  /** Same as above, with TrustNode */
+  void pushBackTrusted(theory::TrustNode trn);
 
   std::vector<Node>& ref() { return d_nodes; }
   const std::vector<Node>& ref() const { return d_nodes; }
@@ -66,21 +79,31 @@ class AssertionPipeline
   /*
    * Replaces assertion i with node n and records the dependency between the
    * original assertion and its replacement.
+   *
+   * @param i The position of the assertion to replace.
+   * @param n The replacement assertion.
+   * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
+   * where d_nodes[i] is the assertion at position i prior to this call.
    */
-  void replace(size_t i, Node n);
+  void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
+  /** Same as above, with TrustNode */
+  void replaceTrusted(size_t i, theory::TrustNode trn);
 
   /*
    * Replaces assertion i with node n and records that this replacement depends
    * on assertion i and the nodes listed in addnDeps. The dependency
    * information is used for unsat cores and proofs.
+   *
+   * @param i The position of the assertion to replace.
+   * @param n The replacement assertion.
+   * @param addnDeps The dependencies.
+   * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
+   * where d_nodes[i] is the assertion at position i prior to this call.
    */
-  void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
-
-  /*
-   * Replaces an assertion with a vector of assertions and records the
-   * dependencies.
-   */
-  void replace(size_t i, const std::vector<Node>& ns);
+  void replace(size_t i,
+               Node n,
+               const std::vector<Node>& addnDeps,
+               ProofGenerator* pg = nullptr);
 
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
@@ -125,7 +148,12 @@ class AssertionPipeline
   {
     return d_storeSubstsInAsserts && i == d_substsIndex;
   }
-
+  //------------------------------------ for proofs
+  /** Set proof generator */
+  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
+  //------------------------------------ end for proofs
  private:
   /** The list of current assertions */
   std::vector<Node> d_nodes;
@@ -157,6 +185,8 @@ class AssertionPipeline
   size_t d_assumptionsStart;
   /** The number of assumptions */
   size_t d_numAssumptions;
+  /** The proof generator, if one is provided */
+  smt::PreprocessProofGenerator* d_pppg;
 }; /* class AssertionPipeline */
 
 }  // namespace preprocessing