(proof-new) Fixes for preprocess proof generator and proofs in assertion pipeline (#5136)

This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.

Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.

1 files changed, 64 insertions, 28 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 99e22b28f..cd92e5f3d 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -61,10 +62,17 @@ void AssertionPipeline::push_back(Node n,
     Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
     d_numAssumptions++;
   }
-  if (!isInput && isProofEnabled())
+  if (isProofEnabled())
   {
-    // notice this is always called, regardless of whether pgen is nullptr
-    d_pppg->notifyNewAssert(n, pgen);
+    if (!isInput)
+    {
+      // notice this is always called, regardless of whether pgen is nullptr
+      d_pppg->notifyNewAssert(n, pgen);
+    }
+    else
+    {
+      Trace("smt-pppg") << "...input assertion " << n << std::endl;
+    }
   }
 }
 
@@ -77,6 +85,13 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
 
 void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
 {
+  if (n == d_nodes[i])
+  {
+    // no change, skip
+    return;
+  }
+  Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n
+                         << std::endl;
   if (options::unsatCores())
   {
     ProofManager::currentPM()->addDependence(n, d_nodes[i]);
@@ -94,26 +109,6 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
   replace(i, trn.getNode(), trn.getGenerator());
 }
 
-void AssertionPipeline::replace(size_t i,
-                                Node n,
-                                const std::vector<Node>& addnDeps,
-                                ProofGenerator* pgen)
-{
-  if (options::unsatCores())
-  {
-    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::setProofGenerator(smt::PreprocessProofGenerator* pppg)
 {
   d_pppg = pppg;
@@ -133,14 +128,55 @@ void AssertionPipeline::disableStoreSubstsInAsserts()
   d_storeSubstsInAsserts = false;
 }
 
-void AssertionPipeline::addSubstitutionNode(Node n)
+void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
 {
   Assert(d_storeSubstsInAsserts);
   Assert(n.getKind() == kind::EQUAL);
-  d_nodes[d_substsIndex] = theory::Rewriter::rewrite(
-      NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex]));
-  Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex])
-         == d_nodes[d_substsIndex]);
+  conjoin(d_substsIndex, n, pg);
+}
+
+void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
+  Node newConjr = theory::Rewriter::rewrite(newConj);
+  if (newConjr == d_nodes[i])
+  {
+    // trivial, skip
+    return;
+  }
+  if (isProofEnabled())
+  {
+    // ---------- from pppg   --------- from pg
+    // d_nodes[i]                n
+    // -------------------------------- AND_INTRO
+    //      d_nodes[i] ^ n
+    // -------------------------------- MACRO_SR_PRED_TRANSFORM
+    //   rewrite( d_nodes[i] ^ n )
+    // allocate a fresh proof which will act as the proof generator
+    LazyCDProof* lcp = d_pppg->allocateHelperProof();
+    lcp->addLazyStep(d_nodes[i], d_pppg, false);
+    lcp->addLazyStep(
+        n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS);
+    lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
+    if (newConjr != newConj)
+    {
+      lcp->addStep(
+          newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
+    }
+    // Notice we have constructed a proof of a new assertion, where d_pppg
+    // is referenced in the lazy proof above. If alternatively we had
+    // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
+    // have used notifyPreprocessed. However, it is simpler to make the
+    // above proof.
+    d_pppg->notifyNewAssert(newConjr, lcp);
+  }
+  if (options::unsatCores())
+  {
+    ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
+  }
+  d_nodes[i] = newConjr;
+  Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
 }
 
 }  // namespace preprocessing