From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Mar 2021 16:50:39 +0000 (-0600)
Subject: Simplify theory preprocessing (#6058)
X-Git-Tag: cvc5-1.0.0~2140
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a5a4ab5d7b4751ce0d730a2cff6678aa64b3306;p=cvc5.git

Simplify theory preprocessing (#6058)

Theory preprocessing now theory-preprocesses lemmas until fixed point. This eliminates the old code for rewriting them only, which is no longer necessary as theory-preprocessing subsumes rewriting.
---

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 0719d4130..3ea87cd0c 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -148,41 +148,6 @@ TrustNode TheoryPreprocessor::preprocessInternal(
     tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
   }
 
-  // now, rewrite the lemmas
-  Trace("tpp-debug") << "TheoryPreprocessor::preprocess: process lemmas"
-                     << std::endl;
-  for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
-  {
-    // get the trust node to process
-    TrustNode trn = newLemmas[i];
-    trn.debugCheckClosed(
-        "tpp-debug", "TheoryPreprocessor::lemma_new_initial", false);
-    Assert(trn.getKind() == TrustNodeKind::LEMMA);
-    Node assertion = trn.getNode();
-    // rewrite, which is independent of d_tpg, since additional lemmas
-    // are justified separately.
-    Node rewritten = Rewriter::rewrite(assertion);
-    if (assertion != rewritten)
-    {
-      if (isProofEnabled())
-      {
-        Assert(d_lp != nullptr);
-        // store in the lazy proof
-        d_lp->addLazyStep(assertion,
-                          trn.getGenerator(),
-                          PfRule::THEORY_PREPROCESS_LEMMA,
-                          true,
-                          "TheoryPreprocessor::rewrite_lemma_new");
-        d_lp->addStep(rewritten,
-                      PfRule::MACRO_SR_PRED_TRANSFORM,
-                      {assertion},
-                      {rewritten});
-      }
-      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
-    }
-    Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
-    newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
-  }
   Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
                      << tret.getNode() << std::endl;
   if (procLemmas)