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

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index fa89604460d1559ce631ed3b8d41ccb0e27b41dd..c8812b1608e79d436a653f1471c5463c65887cfa 100644 (file)
--- 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 7d265fc6725a84359f181f0e32fd22477208137e..ad9250a78e7ec1d749fdded0c4b6f8f7b02b8ed1 100644 (file)
--- 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 e34b10b1dbd01bc6fb018cc6d3c820e019ca5a46..147c17f4a063bb43098e4d425ae49f420d134815 100644 (file)
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -63,12 +63,28 @@ 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