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

5 files changed, 115 insertions, 34 deletions

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