Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

10 files changed, 238 insertions, 167 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 3531497e8..d2f053379 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -38,15 +38,13 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
   // Remove all of the ITE occurrences and normalize
-  theory::TheoryPreprocessor* tpp =
-      d_preprocContext->getTheoryEngine()->getTheoryPreprocess();
+  prop::PropEngine* pe = d_preprocContext->getPropEngine();
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
     std::vector<theory::TrustNode> newAsserts;
     std::vector<Node> newSkolems;
-    // TODO (project #42): this will call the prop engine
-    TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false);
+    TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false);
     if (!trn.isNull())
     {
       // process
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index e888e7a2b..6c751f864 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -29,17 +29,44 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "theory-preprocess"){};
 
 PreprocessingPassResult TheoryPreprocess::applyInternal(
-    AssertionPipeline* assertionsToPreprocess)
+    AssertionPipeline* assertions)
 {
-  TheoryEngine* te = d_preprocContext->getTheoryEngine();
-  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+
+  IteSkolemMap& imap = assertions->getIteSkolemMap();
+  PropEngine* propEngine = d_preprocContext->getPropEngine();
+  // Remove all of the ITE occurrences and normalize
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
-    TNode a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
-    assertionsToPreprocess->replaceTrusted(i, te->preprocess(a));
-    a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
+    Node assertion = (*assertions)[i];
+    std::vector<theory::TrustNode> newAsserts;
+    std::vector<Node> newSkolems;
+    TrustNode trn =
+        propEngine->preprocess(assertion, newAsserts, newSkolems, true);
+    if (!trn.isNull())
+    {
+      // process
+      assertions->replaceTrusted(i, trn);
+      // rewritten assertion has a dependence on the node (old pf architecture)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
+      }
+    }
+    Assert(newSkolems.size() == newAsserts.size());
+    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    {
+      imap[newSkolems[j]] = assertions->size();
+      assertions->pushBackTrusted(newAsserts[j]);
+      // new assertions have a dependence on the node (old pf architecture)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
+                                                 assertion);
+      }
+    }
   }
+
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a8a92096c..8352373c5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 #include "util/resource_manager.h"
@@ -94,8 +95,14 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::CnfStream(
       d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
-  d_theoryProxy = new TheoryProxy(
-      this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
+
+  d_theoryProxy = new TheoryProxy(this,
+                                  d_theoryEngine,
+                                  d_decisionEngine.get(),
+                                  d_context,
+                                  userContext,
+                                  d_cnfStream,
+                                  pnm);
   d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
 
   d_decisionEngine->setSatSolver(d_satSolver);
@@ -143,6 +150,16 @@ PropEngine::~PropEngine() {
   delete d_theoryProxy;
 }
 
+theory::TrustNode PropEngine::preprocess(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  return d_theoryProxy->preprocess(
+      node, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
 void PropEngine::notifyPreprocessedAssertions(
     const preprocessing::AssertionPipeline& ap)
 {
@@ -168,7 +185,6 @@ void PropEngine::notifyPreprocessedAssertions(
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
-  // Assert as non-removable
   if (isProofEnabled())
   {
     d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
@@ -181,35 +197,47 @@ void PropEngine::assertFormula(TNode node) {
   }
 }
 
-void PropEngine::assertLemma(theory::TrustNode trn, bool removable)
+Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
 {
-  Node node = trn.getNode();
-  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
-  Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
-  // Assert as (possibly) removable
-  if (isProofEnabled())
+  bool removable = isLemmaPropertyRemovable(p);
+  bool preprocess = isLemmaPropertyPreprocess(p);
+
+  // call preprocessor
+  std::vector<theory::TrustNode> ppLemmas;
+  std::vector<Node> ppSkolems;
+  theory::TrustNode tplemma =
+      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess);
+
+  Assert(ppSkolems.size() == ppLemmas.size());
+
+  // do final checks on the lemmas we are about to send
+  if (isProofEnabled() && options::proofNewEagerChecking())
   {
-    Assert(trn.getGenerator());
-    d_pfCnfStream->convertAndAssert(
-        node, negated, removable, trn.getGenerator());
+    Assert(tplemma.getGenerator() != nullptr);
+    // ensure closed, make the proof node eagerly here to debug
+    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    {
+      Assert(ppLemmas[i].getGenerator() != nullptr);
+      ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
+    }
   }
-  else
+
+  if (Trace.isOn("te-lemma"))
   {
-    d_cnfStream->convertAndAssert(node, removable, negated);
+    Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
+    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    {
+      Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
+                        << " (skolem is " << ppSkolems[i] << ")" << std::endl;
+    }
   }
-}
 
-void PropEngine::assertLemmas(theory::TrustNode lem,
-                              std::vector<theory::TrustNode>& ppLemmas,
-                              std::vector<Node>& ppSkolems,
-                              bool removable)
-{
-  Assert(ppSkolems.size() == ppLemmas.size());
-  // assert the lemmas
-  assertLemma(lem, removable);
+  // now, assert the lemmas
+  assertLemmaInternal(tplemma, removable);
   for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
   {
-    assertLemma(ppLemmas[i], removable);
+    assertLemmaInternal(ppLemmas[i], removable);
   }
 
   // assert to decision engine
@@ -217,7 +245,7 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
   {
     // also add to the decision engine, where notice we don't need proofs
     std::vector<Node> assertions;
-    assertions.push_back(lem.getProven());
+    assertions.push_back(tplemma.getProven());
     std::vector<Node> ppLemmasF;
     for (const theory::TrustNode& tnl : ppLemmas)
     {
@@ -225,6 +253,38 @@ void PropEngine::assertLemmas(theory::TrustNode lem,
     }
     d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
   }
+
+  // make the return lemma, which the theory engine will use
+  Node retLemma = tplemma.getProven();
+  if (!ppLemmas.empty())
+  {
+    std::vector<Node> lemmas{retLemma};
+    for (const theory::TrustNode& tnl : ppLemmas)
+    {
+      lemmas.push_back(tnl.getProven());
+    }
+    // the returned lemma is the conjunction of all additional lemmas.
+    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
+  }
+  return retLemma;
+}
+
+void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
+{
+  Node node = trn.getNode();
+  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+  Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+  // Assert as (possibly) removable
+  if (isProofEnabled())
+  {
+    Assert(trn.getGenerator());
+    d_pfCnfStream->convertAndAssert(
+        node, negated, removable, trn.getGenerator());
+  }
+  else
+  {
+    d_cnfStream->convertAndAssert(node, removable, negated);
+  }
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
@@ -361,7 +421,25 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
   d_cnfStream->getBooleanVariables(outputVariables);
 }
 
-void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); }
+Node PropEngine::ensureLiteral(TNode n)
+{
+  // must preprocess
+  std::vector<theory::TrustNode> newLemmas;
+  std::vector<Node> newSkolems;
+  theory::TrustNode tpn =
+      d_theoryProxy->preprocess(n, newLemmas, newSkolems, true);
+  // send lemmas corresponding to the skolems introduced by preprocessing n
+  for (const theory::TrustNode& tnl : newLemmas)
+  {
+    Trace("ensureLiteral") << "  lemma: " << tnl.getNode() << std::endl;
+    assertLemma(tnl, theory::LemmaProperty::NONE);
+  }
+  Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode();
+  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
+                         << std::endl;
+  d_cnfStream->ensureLiteral(preprocessed);
+  return preprocessed;
+}
 
 void PropEngine::push()
 {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 55a42c2a7..ac2b35ad6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -95,6 +95,23 @@ class PropEngine
   void shutdown() {}
 
   /**
+   * Preprocess the given node. Return the REWRITE trust node corresponding to
+   * rewriting node. New lemmas and skolems are added to ppLemmas and
+   * ppSkolems respectively.
+   *
+   * @param node The assertion to preprocess,
+   * @param ppLemmas The lemmas to add to the set of assertions,
+   * @param ppSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The (REWRITE) trust node corresponding to rewritten node via
+   * preprocessing.
+   */
+  theory::TrustNode preprocess(TNode node,
+                               std::vector<theory::TrustNode>& ppLemmas,
+                               std::vector<Node>& ppSkolems,
+                               bool doTheoryPreprocess);
+
+  /**
    * Notify preprocessed assertions. This method is called just before the
    * assertions are asserted to this prop engine. This method notifies the
    * decision engine and the theory engine of the assertions in ap.
@@ -114,27 +131,10 @@ class PropEngine
    * than the (SAT and SMT) level at which it was asserted.
    *
    * @param trn the trust node storing the formula to assert
-   * @param removable whether this lemma can be quietly removed based
-   * on an activity heuristic
+   * @param p the properties of the lemma
+   * @return the (preprocessed) lemma
    */
-  void assertLemma(theory::TrustNode trn, bool removable);
-
-  /**
-   * Assert lemma trn with preprocessing lemmas ppLemmas which correspond
-   * to lemmas for skolems in ppSkolems.
-   *
-   * @param trn the trust node storing the formula to assert
-   * @param ppLemmas the lemmas from preprocessing and term formula removal on
-   * the proven node of trn
-   * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should
-   * be the case that ppLemmas.size()==ppSkolems.size().
-   * @param removable whether this lemma can be quietly removed based
-   * on an activity heuristic
-   */
-  void assertLemmas(theory::TrustNode trn,
-                    std::vector<theory::TrustNode>& ppLemmas,
-                    std::vector<Node>& ppSkolems,
-                    bool removable);
+  Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
@@ -185,10 +185,11 @@ class PropEngine
 
   /**
    * Ensure that the given node will have a designated SAT literal
-   * that is definitionally equal to it.  The result of this function
-   * is that the Node can be queried via getSatValue().
+   * that is definitionally equal to it. Note that theory preprocessing is
+   * applied to n. The node returned by this method can be subsequently queried
+   * via getSatValue().
    */
-  void ensureLiteral(TNode n);
+  Node ensureLiteral(TNode n);
 
   /**
    * Push the context level.
@@ -261,6 +262,18 @@ class PropEngine
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
+
+  /**
+   * Converts the given formula to CNF and asserts the CNF to the SAT solver.
+   * The formula can be removed by the SAT solver after backtracking lower
+   * than the (SAT and SMT) level at which it was asserted.
+   *
+   * @param trn the trust node storing the formula to assert
+   * @param removable whether this lemma can be quietly removed based
+   * on an activity heuristic
+   */
+  void assertLemmaInternal(theory::TrustNode trn, bool removable);
+
   /**
    * Indicates that the SAT solver is currently solving something and we should
    * not mess with it's internal state.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 1b9e78d80..23405675a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,15 +19,14 @@
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "options/decision_options.h"
+#include "proof/cnf_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
-#include "proof/cnf_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
 
-
 namespace CVC4 {
 namespace prop {
 
@@ -35,12 +34,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
-                         CnfStream* cnfStream)
+                         context::UserContext* userContext,
+                         CnfStream* cnfStream,
+                         ProofNodeManager* pnm)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_queue(context)
+      d_queue(context),
+      d_tpp(*theoryEngine, userContext, pnm)
 {
 }
 
@@ -165,5 +167,25 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
 
 CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
 
+theory::TrustNode TheoryProxy::preprocessLemma(
+    theory::TrustNode trn,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems, doTheoryPreprocess);
+}
+
+theory::TrustNode TheoryProxy::preprocess(
+    TNode node,
+    std::vector<theory::TrustNode>& newLemmas,
+    std::vector<Node>& newSkolems,
+    bool doTheoryPreprocess)
+{
+  theory::TrustNode pnode =
+      d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess);
+  return pnode;
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index e16728d0d..4d460434d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -26,10 +26,13 @@
 #include <iosfwd>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
 #include "theory/theory.h"
+#include "theory/theory_preprocessor.h"
+#include "theory/trust_node.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
@@ -53,7 +56,9 @@ class TheoryProxy
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
-              CnfStream* cnfStream);
+              context::UserContext* userContext,
+              CnfStream* cnfStream,
+              ProofNodeManager* pnm);
 
   ~TheoryProxy();
 
@@ -90,6 +95,23 @@ class TheoryProxy
 
   CnfStream* getCnfStream();
 
+  /**
+   * Call the preprocessor on node, return trust node corresponding to the
+   * rewrite.
+   */
+  theory::TrustNode preprocessLemma(theory::TrustNode trn,
+                                    std::vector<theory::TrustNode>& newLemmas,
+                                    std::vector<Node>& newSkolems,
+                                    bool doTheoryPreprocess);
+  /**
+   * Call the preprocessor on node, return trust node corresponding to the
+   * rewrite.
+   */
+  theory::TrustNode preprocess(TNode node,
+                               std::vector<theory::TrustNode>& newLemmas,
+                               std::vector<Node>& newSkolems,
+                               bool doTheoryPreprocess);
+
  private:
   /** The prop engine we are using. */
   PropEngine* d_propEngine;
@@ -111,6 +133,9 @@ class TheoryProxy
    * all imported and exported lemmas.
    */
   std::unordered_set<Node, NodeHashFunction> d_shared;
+
+  /** The theory preprocessor */
+  theory::TheoryPreprocessor d_tpp;
 }; /* class TheoryProxy */
 
 }/* CVC4::prop namespace */
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 77c7d450e..8b9b0a53c 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -328,13 +328,8 @@ bool ProcessAssertions::apply(Assertions& as)
 
   // ensure rewritten
   d_passes["rewrite"]->apply(&assertions);
-  // apply theory preprocess
+  // apply theory preprocess, which includes ITE removal
   d_passes["theory-preprocess"]->apply(&assertions);
-  // Must remove ITEs again since theory preprocessing may introduce them.
-  // Notice that we alternatively could ensure that the theory-preprocess
-  // pass above calls TheoryPreprocess::preprocess instead of
-  // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal.
-  d_passes["ite-removal"]->apply(&assertions);
   // This is needed because when solving incrementally, removeITEs may
   // introduce skolems that were solved for earlier and thus appear in the
   // substitution map.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ecb15fbe9..941d900d3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -249,7 +249,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_propagatedLiterals(context),
       d_propagatedLiteralsIndex(context, 0),
       d_atomRequests(context),
-      d_tpp(*this, userContext, d_pnm),
       d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
       d_true(),
       d_false(),
@@ -853,11 +852,6 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   return solveStatus;
 }
 
-TrustNode TheoryEngine::preprocess(TNode assertion)
-{
-  return d_tpp.theoryPreprocess(assertion);
-}
-
 void TheoryEngine::notifyPreprocessedAssertions(
     const std::vector<Node>& assertions) {
   // call all the theories
@@ -1171,21 +1165,7 @@ Node TheoryEngine::getModelValue(TNode var) {
 Node TheoryEngine::ensureLiteral(TNode n) {
   Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
-  Trace("ensureLiteral") << "  got: " << rewritten << std::endl;
-  std::vector<TrustNode> newLemmas;
-  std::vector<Node> newSkolems;
-  TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true);
-  // send lemmas corresponding to the skolems introduced by preprocessing n
-  for (const TrustNode& tnl : newLemmas)
-  {
-    Trace("ensureLiteral") << "  lemma: " << tnl.getNode() << std::endl;
-    lemma(tnl, LemmaProperty::NONE);
-  }
-  Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
-  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
-                         << std::endl;
-  d_propEngine->ensureLiteral(preprocessed);
-  return preprocessed;
+  return d_propEngine->ensureLiteral(rewritten);
 }
 
 
@@ -1440,75 +1420,20 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
     printer.toStreamCmdComment(out, "theory lemma: expect valid");
     printer.toStreamCmdCheckSat(out, n);
   }
-  bool removable = isLemmaPropertyRemovable(p);
-  bool preprocess = isLemmaPropertyPreprocess(p);
-
-  // ensure closed
-  tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
-
-  // call preprocessor
-  std::vector<TrustNode> newLemmas;
-  std::vector<Node> newSkolems;
-  TrustNode tplemma =
-      d_tpp.preprocessLemma(tlemma, newLemmas, newSkolems, preprocess);
 
-  Assert(newSkolems.size() == newLemmas.size());
+  Node retLemma = d_propEngine->assertLemma(tlemma, p);
 
   // If specified, we must add this lemma to the set of those that need to be
   // justified, where note we pass all auxiliary lemmas in lemmas, since these
   // by extension must be justified as well.
   if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
   {
-    d_relManager->notifyPreprocessedAssertion(tplemma.getProven());
-    for (const theory::TrustNode& tnl : newLemmas)
-    {
-      d_relManager->notifyPreprocessedAssertion(tnl.getProven());
-    }
-  }
-
-  // do final checks on the lemmas we are about to send
-  if (isProofEnabled())
-  {
-    Assert(tplemma.getGenerator() != nullptr);
-    // ensure closed, make the proof node eagerly here to debug
-    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
-    for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
-    {
-      Assert(newLemmas[i].getGenerator() != nullptr);
-      newLemmas[i].debugCheckClosed("te-proof-debug",
-                                    "TheoryEngine::lemma_new");
-    }
-  }
-
-  if (Trace.isOn("te-lemma"))
-  {
-    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()
-                        << " (skolem is " << newSkolems[i] << ")" << std::endl;
-    }
+    d_relManager->notifyPreprocessedAssertion(retLemma);
   }
 
-  // now, send the lemmas to the prop engine
-  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 = tplemma.getNode();
-  if (!newLemmas.empty())
-  {
-    std::vector<Node> lemmas{retLemma};
-    for (const theory::TrustNode& tnl : newLemmas)
-    {
-      lemmas.push_back(tnl.getProven());
-    }
-    // the returned lemma is the conjunction of all additional lemmas.
-    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
-  }
   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bdc79931f..bade5a206 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -290,9 +290,6 @@ class TheoryEngine {
   /** sort inference module */
   SortInference d_sortInfer;
 
-  /** The theory preprocessor */
-  theory::TheoryPreprocessor d_tpp;
-
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -442,14 +439,6 @@ class TheoryEngine {
   bool isProofEnabled() const;
 
  public:
-  /**
-   * Runs theory specific preprocessing on the non-Boolean parts of
-   * the formula.  This is only called on input assertions, after ITEs
-   * have been removed.
-   */
-  theory::TrustNode preprocess(TNode node);
-  /** Get the theory preprocessor TODO (project #42) remove this */
-  theory::TheoryPreprocessor* getTheoryPreprocess() { return &d_tpp; }
 
   /** Notify (preprocessed) assertions. */
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 349e7917e..8bda3f5aa 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -72,7 +72,7 @@ class TheoryPreprocessor
                        bool doTheoryPreprocess);
   /**
    * Same as above, but transforms the proof of node into a proof of the
-   * preprocessed node.
+   * preprocessed node and returns the LEMMA trust node.
    *
    * @param node The assertion to preprocess,
    * @param newLemmas The lemmas to add to the set of assertions,
@@ -85,14 +85,13 @@ class TheoryPreprocessor
                             std::vector<TrustNode>& newLemmas,
                             std::vector<Node>& newSkolems,
                             bool doTheoryPreprocess);
+
+ private:
   /**
-   * Runs theory specific preprocessing on the non-Boolean parts of
-   * the formula.  This is only called on input assertions, after ITEs
-   * have been removed.
+   * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean
+   * parts of the node.
    */
   TrustNode theoryPreprocess(TNode node);
-
- private:
   /** Reference to owning theory engine */
   TheoryEngine& d_engine;
   /** Logic info of theory engine */