(proof-new) Make theory preprocessor proofs self contained (#5642)

Previously, there was a block of code in TheoryEngine::lemma for processing the proofs from theory preprocessing.

It is much cleaner if this block was self contained in TheoryPreprocessor.

This is required for the planned move of TheoryPreprocessor from TheoryEngine -> PropEngine.

3 files changed, 69 insertions, 49 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index fa8960446..c8812b160 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1451,48 +1451,7 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   std::vector<TrustNode> newLemmas;
   std::vector<Node> newSkolems;
   TrustNode tplemma =
-      d_tpp.preprocess(lemma, newLemmas, newSkolems, preprocess);
-  // the preprocessed lemma
-  Node lemmap;
-  if (tplemma.isNull())
-  {
-    lemmap = lemma;
-  }
-  else
-  {
-    Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
-    lemmap = tplemma.getNode();
-
-    // must update the trust lemma
-    if (lemmap != lemma)
-    {
-      // process the preprocessing
-      if (isProofEnabled())
-      {
-        Assert(d_lazyProof != nullptr);
-        // add the original proof to the lazy proof
-        d_lazyProof->addLazyStep(tlemma.getProven(), tlemma.getGenerator());
-        // only need to do anything if lemmap changed in a non-trivial way
-        if (!CDProof::isSame(lemmap, lemma))
-        {
-          d_lazyProof->addLazyStep(tplemma.getProven(),
-                                   tplemma.getGenerator(),
-                                   PfRule::PREPROCESS_LEMMA,
-                                   true,
-                                   "TheoryEngine::lemma_pp");
-          // ---------- from d_lazyProof -------------- from theory preprocess
-          // lemma                       lemma = lemmap
-          // ------------------------------------------ EQ_RESOLVE
-          // lemmap
-          std::vector<Node> pfChildren;
-          pfChildren.push_back(lemma);
-          pfChildren.push_back(tplemma.getProven());
-          d_lazyProof->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
-        }
-      }
-      tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get());
-    }
-  }
+      d_tpp.preprocessLemma(tlemma, newLemmas, newSkolems, preprocess);
 
   Assert(newSkolems.size() == newLemmas.size());
 
@@ -1501,7 +1460,7 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   // by extension must be justified as well.
   if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
   {
-    d_relManager->notifyPreprocessedAssertion(tlemma.getProven());
+    d_relManager->notifyPreprocessedAssertion(tplemma.getProven());
     for (const theory::TrustNode& tnl : newLemmas)
     {
       d_relManager->notifyPreprocessedAssertion(tnl.getProven());
@@ -1511,9 +1470,9 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   // do final checks on the lemmas we are about to send
   if (isProofEnabled())
   {
-    Assert(tlemma.getGenerator() != nullptr);
+    Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug
-    tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
     for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
     {
       Assert(newLemmas[i].getGenerator() != nullptr);
@@ -1524,7 +1483,7 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
 
   if (Trace.isOn("te-lemma"))
   {
-    Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
+    Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
     for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
     {
       Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
@@ -1533,14 +1492,14 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   }
 
   // now, send the lemmas to the prop engine
-  d_propEngine->assertLemmas(tlemma, newLemmas, newSkolems, removable);
+  d_propEngine->assertLemmas(tplemma, newLemmas, newSkolems, removable);
 
   // Mark that we added some lemmas
   d_lemmasAdded = true;
 
   // Lemma analysis isn't online yet; this lemma may only live for this
   // user level.
-  Node retLemma = tlemma.getNode();
+  Node retLemma = tplemma.getNode();
   if (!newLemmas.empty())
   {
     std::vector<Node> lemmas{retLemma};
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 7d265fc67..ad9250a78 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -224,6 +224,51 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   return tret;
 }
 
+TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
+                                              std::vector<TrustNode>& newLemmas,
+                                              std::vector<Node>& newSkolems,
+                                              bool doTheoryPreprocess)
+{
+  // what was originally proven
+  Node lemma = node.getProven();
+  TrustNode tplemma =
+      preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess);
+  if (tplemma.isNull())
+  {
+    // no change needed
+    return node;
+  }
+  Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
+  // what it was preprocessed to
+  Node lemmap = tplemma.getNode();
+  Assert(lemmap != node.getProven());
+  // process the preprocessing
+  if (isProofEnabled())
+  {
+    Assert(d_lp != nullptr);
+    // add the original proof to the lazy proof
+    d_lp->addLazyStep(node.getProven(), node.getGenerator());
+    // only need to do anything if lemmap changed in a non-trivial way
+    if (!CDProof::isSame(lemmap, lemma))
+    {
+      d_lp->addLazyStep(tplemma.getProven(),
+                        tplemma.getGenerator(),
+                        PfRule::PREPROCESS_LEMMA,
+                        true,
+                        "TheoryEngine::lemma_pp");
+      // ---------- from node -------------- from theory preprocess
+      // lemma                lemma = lemmap
+      // ------------------------------------------ EQ_RESOLVE
+      // lemmap
+      std::vector<Node> pfChildren;
+      pfChildren.push_back(lemma);
+      pfChildren.push_back(tplemma.getProven());
+      d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
+    }
+  }
+  return TrustNode::mkTrustLemma(lemmap, d_lp.get());
+}
+
 struct preprocess_stack_element
 {
   TNode node;
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index e34b10b1d..147c17f4a 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -63,13 +63,29 @@ class TheoryPreprocessor
    * @param newLemmas The lemmas to add to the set of assertions,
    * @param newSkolems The skolems that newLemmas correspond to,
    * @param doTheoryPreprocess whether to run theory-specific preprocessing.
-   * @return The trust node corresponding to rewriting node via preprocessing.
+   * @return The (REWRITE) trust node corresponding to rewritten node via
+   * preprocessing.
    */
   TrustNode preprocess(TNode node,
                        std::vector<TrustNode>& newLemmas,
                        std::vector<Node>& newSkolems,
                        bool doTheoryPreprocess);
   /**
+   * Same as above, but transforms the proof of node into a proof of the
+   * preprocessed node.
+   *
+   * @param node The assertion to preprocess,
+   * @param newLemmas The lemmas to add to the set of assertions,
+   * @param newSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The (LEMMA) trust node corresponding to the proof of the rewritten
+   * form of the proven field of node.
+   */
+  TrustNode preprocessLemma(TrustNode node,
+                            std::vector<TrustNode>& newLemmas,
+                            std::vector<Node>& newSkolems,
+                            bool doTheoryPreprocess);
+  /**
    * Runs theory specific preprocessing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs
    * have been removed.