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

9 files changed, 205 insertions, 81 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
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 63e2bdd2a..6ca430ac4 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -49,7 +49,9 @@ class AssertionPipeline
    */
   void clear();
 
+  /** TODO (projects #75): remove this */
   Node& operator[](size_t i) { return d_nodes[i]; }
+  /** Get the assertion at index i */
   const Node& operator[](size_t i) const { return d_nodes[i]; }
 
   /**
@@ -70,7 +72,13 @@ class AssertionPipeline
   /** Same as above, with TrustNode */
   void pushBackTrusted(theory::TrustNode trn);
 
+  /** TODO (projects #75): remove this */
   std::vector<Node>& ref() { return d_nodes; }
+
+  /**
+   * Get the constant reference to the underlying assertions. It is only
+   * possible to modify these via the replace methods below.
+   */
   const std::vector<Node>& ref() const { return d_nodes; }
 
   std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
@@ -89,22 +97,6 @@ class AssertionPipeline
   /** 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,
-               ProofGenerator* pg = nullptr);
-
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
 
@@ -136,8 +128,23 @@ class AssertionPipeline
 
   /**
    * Adds a substitution node of the form (= lhs rhs) to the assertions.
+   * This conjoins n to assertions at a distinguished index given by
+   * d_substsIndex.
+   *
+   * @param n The substitution node
+   * @param pg The proof generator that can provide a proof of n.
+   */
+  void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr);
+
+  /**
+   * Conjoin n to the assertion vector at position i. This replaces
+   * d_nodes[i] with the rewritten form of (AND d_nodes[i] n).
+   *
+   * @param i The assertion to replace
+   * @param n The formula to conjoin at position i
+   * @param pg The proof generator that can provide a proof of n
    */
-  void addSubstitutionNode(Node n);
+  void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr);
 
   /**
    * Checks whether the assertion at a given index represents substitutions.
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 5c7ed0356..1739a4e7d 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -21,15 +21,24 @@
 namespace CVC4 {
 namespace smt {
 
-PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm)
-    : d_pnm(pnm)
+PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u,
+                                                   ProofNodeManager* pnm)
+    : d_pnm(pnm), d_src(u), d_helperProofs(u)
 {
 }
 
 void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
 {
-  Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl;
-  d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+  Trace("smt-proof-pp-debug")
+      << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
+  if (d_src.find(n) == d_src.end())
+  {
+    d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+  }
+  else
+  {
+    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+  }
 }
 
 void PreprocessProofGenerator::notifyPreprocessed(Node n,
@@ -40,14 +49,22 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n,
   if (n != np)
   {
     Trace("smt-proof-pp-debug")
-        << "- notifyPreprocessed: " << n << "..." << np << std::endl;
-    d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+        << "PreprocessProofGenerator::notifyPreprocessed: " << n << "..." << np
+        << std::endl;
+    if (d_src.find(np) == d_src.end())
+    {
+      d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg);
+    }
+    else
+    {
+      Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
+    }
   }
 }
 
 std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
 {
-  std::map<Node, theory::TrustNode>::iterator it = d_src.find(f);
+  NodeTrustNodeMap::iterator it = d_src.find(f);
   if (it == d_src.end())
   {
     // could be an assumption, return nullptr
@@ -56,67 +73,102 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
   // make CDProof to construct the proof below
   CDProof cdp(d_pnm);
 
+  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f
+                    << std::endl;
   Node curr = f;
   std::vector<Node> transChildren;
+  std::unordered_set<Node, NodeHashFunction> processed;
   bool success;
+  // we connect the proof of f to its source via the map d_src until we
+  // discover that its source is a preprocessing lemma (a lemma stored in d_src)
+  // or otherwise it is assumed to be an input assumption.
   do
   {
     success = false;
     if (it != d_src.end())
     {
-      Assert(it->second.getNode() == curr);
+      Assert((*it).second.getNode() == curr);
+      // get the proven node
+      Node proven = (*it).second.getProven();
+      Assert(!proven.isNull());
+      Trace("smt-pppg") << "...process proven " << proven << std::endl;
+      if (processed.find(proven) != processed.end())
+      {
+        Unhandled() << "Cyclic steps in preprocess proof generator";
+        continue;
+      }
+      processed.insert(proven);
       bool proofStepProcessed = false;
-      std::shared_ptr<ProofNode> pfr = it->second.toProofNode();
+
+      // if a generator for the step was provided, it is stored in the proof
+      Trace("smt-pppg") << "...get provided proof" << std::endl;
+      std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
       if (pfr != nullptr)
       {
-        Assert(pfr->getResult() == it->second.getProven());
+        Trace("smt-pppg") << "...add provided" << std::endl;
+        Assert(pfr->getResult() == proven);
         cdp.addProof(pfr);
         proofStepProcessed = true;
       }
 
-      if (it->second.getKind() == theory::TrustNodeKind::REWRITE)
+      Trace("smt-pppg") << "...update" << std::endl;
+      theory::TrustNodeKind tnk = (*it).second.getKind();
+      if (tnk == theory::TrustNodeKind::REWRITE)
       {
-        Node eq = it->second.getProven();
-        Assert(eq.getKind() == kind::EQUAL);
+        Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
+        Assert(proven.getKind() == kind::EQUAL);
         if (!proofStepProcessed)
         {
           // maybe its just a simple rewrite?
-          if (eq[1] == theory::Rewriter::rewrite(eq[0]))
+          if (proven[1] == theory::Rewriter::rewrite(proven[0]))
           {
-            cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]});
+            cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
             proofStepProcessed = true;
           }
         }
-        transChildren.push_back(eq);
+        transChildren.push_back(proven);
         // continue with source
-        curr = eq[0];
+        curr = proven[0];
         success = true;
         // find the next node
         it = d_src.find(curr);
       }
       else
       {
-        Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA);
+        Trace("smt-pppg") << "...lemma" << std::endl;
+        Assert(tnk == theory::TrustNodeKind::LEMMA);
       }
 
       if (!proofStepProcessed)
       {
-        // add trusted step
-        Node proven = it->second.getProven();
-        cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven});
+        Trace("smt-pppg") << "...add missing step" << std::endl;
+        // add trusted step, the rule depends on the kind of trust node
+        cdp.addStep(proven,
+                    tnk == theory::TrustNodeKind::LEMMA
+                        ? PfRule::PREPROCESS_LEMMA
+                        : PfRule::PREPROCESS,
+                    {},
+                    {proven});
       }
     }
   } while (success);
 
-  Assert(curr != f);
-  // prove ( curr == f )
-  Node fullRewrite = curr.eqNode(f);
-  if (transChildren.size() >= 2)
+  // prove ( curr == f ), which is not necessary if they are the same
+  // modulo symmetry.
+  if (!CDProof::isSame(f, curr))
   {
-    cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+    Node fullRewrite = curr.eqNode(f);
+    if (transChildren.size() >= 2)
+    {
+      Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
+      std::reverse(transChildren.begin(), transChildren.end());
+      cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
+    }
+    Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
+    // prove f
+    cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
+    Trace("smt-pppg") << "...finished" << std::endl;
   }
-  // prove f
-  cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
 
   // overall, proof is:
   //        --------- from proof generator       ---------- from proof generator
@@ -130,6 +182,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
   return cdp.getProofFor(f);
 }
 
+ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
+
+LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
+{
+  std::shared_ptr<LazyCDProof> helperPf = std::make_shared<LazyCDProof>(d_pnm);
+  d_helperProofs.push_back(helperPf);
+  return helperPf.get();
+}
+
 std::string PreprocessProofGenerator::identify() const
 {
   return "PreprocessProofGenerator";
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 5319071f0..b71187188 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -19,8 +19,12 @@
 
 #include <map>
 
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/lazy_proof.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node_manager.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
@@ -41,8 +45,11 @@ namespace smt {
  */
 class PreprocessProofGenerator : public ProofGenerator
 {
+  typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
+      NodeTrustNodeMap;
+
  public:
-  PreprocessProofGenerator(ProofNodeManager* pnm);
+  PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm);
   ~PreprocessProofGenerator() {}
   /**
    * Notify that n is a new assertion, where pg can provide a proof of n.
@@ -61,6 +68,17 @@ class PreprocessProofGenerator : public ProofGenerator
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
   /** Identify */
   std::string identify() const override;
+  /** Get the proof manager */
+  ProofNodeManager* getManager();
+  /**
+   * Allocate a helper proof. This returns a fresh lazy proof object that
+   * remains alive in this user context. This feature is used to construct
+   * helper proofs for preprocessing, e.g. to support the skeleton of proofs
+   * that connect AssertionPipeline::conjoin steps.
+   *
+   * Internally, this adds a LazyCDProof to the list d_helperProofs below.
+   */
+  LazyCDProof* allocateHelperProof();
 
  private:
   /** The proof node manager */
@@ -72,7 +90,9 @@ class PreprocessProofGenerator : public ProofGenerator
    * (1) A trust node REWRITE proving (n_src = n) for some n_src, or
    * (2) A trust node LEMMA proving n.
    */
-  std::map<Node, theory::TrustNode> d_src;
+  NodeTrustNodeMap d_src;
+  /** A context-dependent list of LazyCDProof, allocated for conjoin steps */
+  context::CDList<std::shared_ptr<LazyCDProof> > d_helperProofs;
 };
 
 }  // namespace smt
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index f51a116b7..df7b6bf4d 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -22,10 +22,10 @@
 namespace CVC4 {
 namespace smt {
 
-PfManager::PfManager(SmtEngine* smte)
+PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
     : d_pchecker(new ProofChecker(options::proofNewPedantic())),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
-      d_pppg(new PreprocessProofGenerator(d_pnm.get())),
+      d_pppg(new PreprocessProofGenerator(u, d_pnm.get())),
       d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
       d_finalProof(nullptr)
 {
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index bda741a05..118b82bec 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -41,7 +41,7 @@ class Assertions;
 class PfManager
 {
  public:
-  PfManager(SmtEngine* smte);
+  PfManager(context::UserContext* u, SmtEngine* smte);
   ~PfManager();
   /**
    * Print the proof on the output channel of the current options in scope.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3caf03946..755822d2a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -270,7 +270,7 @@ void SmtEngine::finishInit()
   ProofNodeManager* pnm = nullptr;
   if (options::proofNew())
   {
-    d_pfManager.reset(new PfManager(this));
+    d_pfManager.reset(new PfManager(getUserContext(), this));
     // use this proof node manager
     pnm = d_pfManager->getProofNodeManager();
     // enable proof support in the rewriter
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index fe66fc3cb..b0c8f3b79 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -101,7 +101,7 @@ ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
 
 bool TrustNode::isNull() const { return d_proven.isNull(); }
 
-std::shared_ptr<ProofNode> TrustNode::toProofNode()
+std::shared_ptr<ProofNode> TrustNode::toProofNode() const
 {
   if (d_gen == nullptr)
   {
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index 0e0bfddf5..a0586bd0c 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -132,7 +132,7 @@ class TrustNode
    * Gets the proof node for this trust node, which is obtained by
    * calling the generator's getProofFor method on the proven node.
    */
-  std::shared_ptr<ProofNode> toProofNode();
+  std::shared_ptr<ProofNode> toProofNode() const;
 
   /** Get the proven formula corresponding to a conflict call */
   static Node getConflictProven(Node conf);