(proof-new) Split TheoryEngine (#4558)

This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs.

This PR does not change their behavior and is code-move only modulo a few cosmetic changes.

7 files changed, 753 insertions, 456 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3872e2b42..08725409b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -434,6 +434,8 @@ libcvc4_add_sources(
   theory/decision_strategy.h
   theory/eager_proof_generator.cpp
   theory/eager_proof_generator.h
+  theory/engine_output_channel.cpp
+  theory/engine_output_channel.h
   theory/evaluator.cpp
   theory/evaluator.h
   theory/ext_theory.cpp
@@ -745,6 +747,8 @@ libcvc4_add_sources(
   theory/theory_model.h
   theory/theory_model_builder.cpp
   theory/theory_model_builder.h
+  theory/theory_preprocessor.cpp
+  theory/theory_preprocessor.h
   theory/theory_proof_step_buffer.cpp
   theory/theory_proof_step_buffer.h
   theory/theory_rewriter.h
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
new file mode 100644
index 000000000..176d08acf
--- /dev/null
+++ b/src/theory/engine_output_channel.cpp
@@ -0,0 +1,302 @@
+/*********************                                                        */
+/*! \file engine_output_channel.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory engine output channel.
+ **/
+
+#include "theory/engine_output_channel.h"
+
+#include "proof/cnf_proof.h"
+#include "proof/lemma_proof.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
+#include "prop/prop_engine.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
+    : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
+      propagations(getStatsPrefix(theory) + "::propagations", 0),
+      lemmas(getStatsPrefix(theory) + "::lemmas", 0),
+      requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
+      restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
+      trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
+      trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
+{
+  smtStatisticsRegistry()->registerStat(&conflicts);
+  smtStatisticsRegistry()->registerStat(&propagations);
+  smtStatisticsRegistry()->registerStat(&lemmas);
+  smtStatisticsRegistry()->registerStat(&requirePhase);
+  smtStatisticsRegistry()->registerStat(&restartDemands);
+  smtStatisticsRegistry()->registerStat(&trustedConflicts);
+  smtStatisticsRegistry()->registerStat(&trustedLemmas);
+}
+
+EngineOutputChannel::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&conflicts);
+  smtStatisticsRegistry()->unregisterStat(&propagations);
+  smtStatisticsRegistry()->unregisterStat(&lemmas);
+  smtStatisticsRegistry()->unregisterStat(&requirePhase);
+  smtStatisticsRegistry()->unregisterStat(&restartDemands);
+  smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
+  smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
+}
+
+EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
+                                         theory::TheoryId theory)
+    : d_engine(engine), d_statistics(theory), d_theory(theory)
+{
+}
+
+void EngineOutputChannel::safePoint(ResourceManager::Resource r)
+{
+  spendResource(r);
+  if (d_engine->d_interrupted)
+  {
+    throw theory::Interrupted();
+  }
+}
+
+theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma,
+                                               ProofRule rule,
+                                               bool removable,
+                                               bool preprocess,
+                                               bool sendAtoms)
+{
+  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+                         << lemma << ")"
+                         << ", preprocess = " << preprocess << std::endl;
+  ++d_statistics.lemmas;
+  d_engine->d_outputChannelUsed = true;
+
+  PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); });
+
+  theory::LemmaStatus result =
+      d_engine->lemma(lemma,
+                      rule,
+                      false,
+                      removable,
+                      preprocess,
+                      sendAtoms ? d_theory : theory::THEORY_LAST);
+  return result;
+}
+
+void EngineOutputChannel::registerLemmaRecipe(Node lemma,
+                                              Node originalLemma,
+                                              bool preprocess,
+                                              theory::TheoryId theoryId)
+{
+  // During CNF conversion, conjunctions will be broken down into
+  // multiple lemmas. In order for the recipes to match, we have to do
+  // the same here.
+  NodeManager* nm = NodeManager::currentNM();
+
+  if (preprocess) lemma = d_engine->preprocess(lemma);
+
+  bool negated = (lemma.getKind() == NOT);
+  Node nnLemma = negated ? lemma[0] : lemma;
+
+  switch (nnLemma.getKind())
+  {
+    case AND:
+      if (!negated)
+      {
+        for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
+          registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
+      }
+      else
+      {
+        NodeBuilder<> builder(OR);
+        for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
+          builder << nnLemma[i].negate();
+
+        Node disjunction =
+            (builder.getNumChildren() == 1) ? builder[0] : builder;
+        registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
+      }
+      break;
+
+    case EQUAL:
+      if (nnLemma[0].getType().isBoolean())
+      {
+        if (!negated)
+        {
+          registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()),
+                              originalLemma,
+                              false,
+                              theoryId);
+          registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
+                              originalLemma,
+                              false,
+                              theoryId);
+        }
+        else
+        {
+          registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]),
+                              originalLemma,
+                              false,
+                              theoryId);
+          registerLemmaRecipe(
+              nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
+              originalLemma,
+              false,
+              theoryId);
+        }
+      }
+      break;
+
+    case ITE:
+      if (!negated)
+      {
+        registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
+                            originalLemma,
+                            false,
+                            theoryId);
+        registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]),
+                            originalLemma,
+                            false,
+                            theoryId);
+      }
+      else
+      {
+        registerLemmaRecipe(
+            nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
+            originalLemma,
+            false,
+            theoryId);
+        registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()),
+                            originalLemma,
+                            false,
+                            theoryId);
+      }
+      break;
+
+    default: break;
+  }
+
+  // Theory lemmas have one step that proves the empty clause
+  LemmaProofRecipe proofRecipe;
+  Node emptyNode;
+  LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
+
+  // Remember the original lemma, so we can report this later when asked to
+  proofRecipe.setOriginalLemma(originalLemma);
+
+  // Record the assertions and rewrites
+  Node rewritten;
+  if (lemma.getKind() == OR)
+  {
+    for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+    {
+      rewritten = theory::Rewriter::rewrite(lemma[i]);
+      if (rewritten != lemma[i])
+      {
+        proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate());
+      }
+      proofStep.addAssertion(lemma[i]);
+      proofRecipe.addBaseAssertion(rewritten);
+    }
+  }
+  else
+  {
+    rewritten = theory::Rewriter::rewrite(lemma);
+    if (rewritten != lemma)
+    {
+      proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate());
+    }
+    proofStep.addAssertion(lemma);
+    proofRecipe.addBaseAssertion(rewritten);
+  }
+  proofRecipe.addStep(proofStep);
+  ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
+}
+
+theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
+{
+  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+                         << lemma << ")" << std::endl;
+  ++d_statistics.lemmas;
+  d_engine->d_outputChannelUsed = true;
+
+  Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
+                       << std::endl;
+  theory::LemmaStatus result =
+      d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
+  return result;
+}
+
+bool EngineOutputChannel::propagate(TNode literal)
+{
+  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
+                             << ">::propagate(" << literal << ")" << std::endl;
+  ++d_statistics.propagations;
+  d_engine->d_outputChannelUsed = true;
+  return d_engine->propagate(literal, d_theory);
+}
+
+void EngineOutputChannel::conflict(TNode conflictNode,
+                                   std::unique_ptr<Proof> proof)
+{
+  Trace("theory::conflict")
+      << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
+      << ")" << std::endl;
+  Assert(!proof);  // Theory shouldn't be producing proofs yet
+  ++d_statistics.conflicts;
+  d_engine->d_outputChannelUsed = true;
+  d_engine->conflict(conflictNode, d_theory);
+}
+
+void EngineOutputChannel::demandRestart()
+{
+  NodeManager* curr = NodeManager::currentNM();
+  Node restartVar = curr->mkSkolem(
+      "restartVar",
+      curr->booleanType(),
+      "A boolean variable asserted to be true to force a restart");
+  Trace("theory::restart") << "EngineOutputChannel<" << d_theory
+                           << ">::restart(" << restartVar << ")" << std::endl;
+  ++d_statistics.restartDemands;
+  lemma(restartVar, RULE_INVALID, true);
+}
+
+void EngineOutputChannel::requirePhase(TNode n, bool phase)
+{
+  Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
+                  << ")" << std::endl;
+  ++d_statistics.requirePhase;
+  d_engine->getPropEngine()->requirePhase(n, phase);
+}
+
+void EngineOutputChannel::setIncomplete()
+{
+  Trace("theory") << "setIncomplete()" << std::endl;
+  d_engine->setIncomplete(d_theory);
+}
+
+void EngineOutputChannel::spendResource(ResourceManager::Resource r)
+{
+  d_engine->spendResource(r);
+}
+
+void EngineOutputChannel::handleUserAttribute(const char* attr,
+                                              theory::Theory* t)
+{
+  d_engine->handleUserAttribute(attr, t);
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
new file mode 100644
index 000000000..714a206c2
--- /dev/null
+++ b/src/theory/engine_output_channel.h
@@ -0,0 +1,100 @@
+/*********************                                                        */
+/*! \file engine_output_channel.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory engine output channel.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
+#define CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
+
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/theory.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+/**
+ * An output channel for Theory that passes messages back to a TheoryEngine
+ * for a given Theory.
+ *
+ * Notice that it has interfaces trustedConflict and trustedLemma which are
+ * used for ensuring that proof generators are associated with the lemmas
+ * and conflicts sent on this output channel.
+ */
+class EngineOutputChannel : public theory::OutputChannel
+{
+  friend class TheoryEngine;
+
+ public:
+  EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
+
+  void safePoint(ResourceManager::Resource r) override;
+
+  void conflict(TNode conflictNode,
+                std::unique_ptr<Proof> pf = nullptr) override;
+  bool propagate(TNode literal) override;
+
+  theory::LemmaStatus lemma(TNode lemma,
+                            ProofRule rule,
+                            bool removable = false,
+                            bool preprocess = false,
+                            bool sendAtoms = false) override;
+
+  theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
+
+  void demandRestart() override;
+
+  void requirePhase(TNode n, bool phase) override;
+
+  void setIncomplete() override;
+
+  void spendResource(ResourceManager::Resource r) override;
+
+  void handleUserAttribute(const char* attr, theory::Theory* t) override;
+
+ protected:
+  /**
+   * Statistics for a particular theory.
+   */
+  class Statistics
+  {
+   public:
+    Statistics(theory::TheoryId theory);
+    ~Statistics();
+    /** Number of calls to conflict, propagate, lemma, requirePhase,
+     * restartDemands */
+    IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
+        trustedConflicts, trustedLemmas;
+  };
+  /** The theory engine we're communicating with. */
+  TheoryEngine* d_engine;
+  /** The statistics of the theory interractions. */
+  Statistics d_statistics;
+  /** The theory owning this channel. */
+  theory::TheoryId d_theory;
+  /** A helper function for registering lemma recipes with the proof engine */
+  void registerLemmaRecipe(Node lemma,
+                           Node originalLemma,
+                           bool preprocess,
+                           theory::TheoryId theoryId);
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 71c144daa..1e4f2a7ac 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -127,144 +127,6 @@ std::string getTheoryString(theory::TheoryId id)
   }
 }
 
-theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
-                                                             ProofRule rule,
-                                                             bool removable,
-                                                             bool preprocess,
-                                                             bool sendAtoms) {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
-                         << lemma << ")"
-                         << ", preprocess = " << preprocess << std::endl;
-  ++d_statistics.lemmas;
-  d_engine->d_outputChannelUsed = true;
-
-  PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); });
-
-  theory::LemmaStatus result =
-      d_engine->lemma(lemma, rule, false, removable, preprocess,
-                      sendAtoms ? d_theory : theory::THEORY_LAST);
-  return result;
-}
-
-void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId) {
-  // During CNF conversion, conjunctions will be broken down into
-  // multiple lemmas. In order for the recipes to match, we have to do
-  // the same here.
-  NodeManager* nm = NodeManager::currentNM();
-
-  if (preprocess)
-    lemma = d_engine->preprocess(lemma);
-
-  bool negated = (lemma.getKind() == kind::NOT);
-  Node nnLemma = negated ? lemma[0] : lemma;
-
-  switch (nnLemma.getKind()) {
-
-  case kind::AND:
-    if (!negated) {
-      for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
-        registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
-    } else {
-      NodeBuilder<> builder(kind::OR);
-      for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
-        builder << nnLemma[i].negate();
-
-      Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder;
-      registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
-    }
-    break;
-
-  case kind::EQUAL:
-    if( nnLemma[0].getType().isBoolean() ){
-      if (!negated) {
-        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
-        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
-      } else {
-        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
-        registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
-      }
-    }
-    break;
-
-  case kind::ITE:
-    if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId);
-    } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId);
-    }
-    break;
-
-  default:
-    break;
-  }
-
-  // Theory lemmas have one step that proves the empty clause
-  LemmaProofRecipe proofRecipe;
-  Node emptyNode;
-  LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
-
-  // Remember the original lemma, so we can report this later when asked to
-  proofRecipe.setOriginalLemma(originalLemma);
-
-  // Record the assertions and rewrites
-  Node rewritten;
-  if (lemma.getKind() == kind::OR) {
-    for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
-      rewritten = theory::Rewriter::rewrite(lemma[i]);
-      if (rewritten != lemma[i]) {
-        proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate());
-      }
-      proofStep.addAssertion(lemma[i]);
-      proofRecipe.addBaseAssertion(rewritten);
-    }
-  } else {
-    rewritten = theory::Rewriter::rewrite(lemma);
-    if (rewritten != lemma) {
-      proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate());
-    }
-    proofStep.addAssertion(lemma);
-    proofRecipe.addBaseAssertion(rewritten);
-  }
-  proofRecipe.addStep(proofStep);
-  ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
-}
-
-theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(
-    TNode lemma, bool removable) {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
-                         << lemma << ")" << std::endl;
-  ++d_statistics.lemmas;
-  d_engine->d_outputChannelUsed = true;
-
-  Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( "
-                       << lemma << " )" << std::endl;
-  theory::LemmaStatus result =
-      d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
-  return result;
-}
-
-bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) {
-  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
-                             << ">::propagate(" << literal << ")" << std::endl;
-  ++d_statistics.propagations;
-  d_engine->d_outputChannelUsed = true;
-  return d_engine->propagate(literal, d_theory);
-}
-
-void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
-                                                 std::unique_ptr<Proof> proof)
-{
-  Trace("theory::conflict")
-      << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
-      << ")" << std::endl;
-  Assert(!proof);  // Theory shouldn't be producing proofs yet
-  ++d_statistics.conflicts;
-  d_engine->d_outputChannelUsed = true;
-  d_engine->conflict(conflictNode, d_theory);
-}
-
 void TheoryEngine::finishInit() {
   //initialize the quantifiers engine, master equality engine, model, model builder
   if( d_logicInfo.isQuantified() ) {
@@ -327,7 +189,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_curr_model_builder(nullptr),
       d_aloc_curr_model_builder(false),
       d_eager_model_building(false),
-      d_ppCache(),
       d_possiblePropagations(context),
       d_hasPropagated(context),
       d_inConflict(context, false),
@@ -339,7 +200,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_propagatedLiterals(context),
       d_propagatedLiteralsIndex(context, 0),
       d_atomRequests(context),
-      d_tform_remover(iteRemover),
+      d_tpp(*this, iteRemover),
       d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
       d_true(),
       d_false(),
@@ -1073,7 +934,7 @@ void TheoryEngine::shutdown() {
     }
   }
 
-  d_ppCache.clear();
+  d_tpp.clearCache();
 }
 
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
@@ -1099,144 +960,10 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
   return solveStatus;
 }
 
-// Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryEngine::ppTheoryRewrite(TNode term) {
-  NodeMap::iterator find = d_ppCache.find(term);
-  if (find != d_ppCache.end()) {
-    return (*find).second;
-  }
-  unsigned nc = term.getNumChildren();
-  if (nc == 0) {
-    return theoryOf(term)->ppRewrite(term);
-  }
-  Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
-
-  Node newTerm;
-  // do not rewrite inside quantifiers
-  if (term.isClosure())
-  {
-    newTerm = Rewriter::rewrite(term);
-  }
-  else
-  {
-    NodeBuilder<> newNode(term.getKind());
-    if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      newNode << term.getOperator();
-    }
-    unsigned i;
-    for (i = 0; i < nc; ++i) {
-      newNode << ppTheoryRewrite(term[i]);
-    }
-    newTerm = Rewriter::rewrite(Node(newNode));
-  }
-  Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
-  if (newTerm != newTerm2) {
-    newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
-  }
-  d_ppCache[term] = newTerm;
-  Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl;
-  return newTerm;
-}
-
-
-void TheoryEngine::preprocessStart()
-{
-  d_ppCache.clear();
-}
-
-
-struct preprocess_stack_element {
-  TNode node;
-  bool children_added;
-  preprocess_stack_element(TNode n) : node(n), children_added(false) {}
-};/* struct preprocess_stack_element */
-
+void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
 
 Node TheoryEngine::preprocess(TNode assertion) {
-
-  Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
-  // spendResource();
-
-  // Do a topological sort of the subexpressions and substitute them
-  vector<preprocess_stack_element> toVisit;
-  toVisit.push_back(assertion);
-
-  while (!toVisit.empty())
-  {
-    // The current node we are processing
-    preprocess_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.node;
-
-    Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl;
-
-    // If node already in the cache we're done, pop from the stack
-    NodeMap::iterator find = d_ppCache.find(current);
-    if (find != d_ppCache.end()) {
-      toVisit.pop_back();
-      continue;
-    }
-
-    if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) &&
-       Theory::theoryOf(current) != THEORY_SAT_SOLVER) {
-      stringstream ss;
-      ss << "The logic was specified as " << d_logicInfo.getLogicString()
-         << ", which doesn't include " << Theory::theoryOf(current)
-         << ", but got a preprocessing-time fact for that theory." << endl
-         << "The fact:" << endl
-         << current;
-      throw LogicException(ss.str());
-    }
-
-    // If this is an atom, we preprocess its terms with the theory ppRewriter
-    if (Theory::theoryOf(current) != THEORY_BOOL) {
-      Node ppRewritten = ppTheoryRewrite(current);
-      d_ppCache[current] = ppRewritten;
-      Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
-      continue;
-    }
-
-    // Not yet substituted, so process
-    if (stackHead.children_added) {
-      // Children have been processed, so substitute
-      NodeBuilder<> builder(current.getKind());
-      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        builder << current.getOperator();
-      }
-      for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-        Assert(d_ppCache.find(current[i]) != d_ppCache.end());
-        builder << d_ppCache[current[i]];
-      }
-      // Mark the substitution and continue
-      Node result = builder;
-      if (result != current) {
-        result = Rewriter::rewrite(result);
-      }
-      Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
-      d_ppCache[current] = result;
-      toVisit.pop_back();
-    } else {
-      // Mark that we have added the children if any
-      if (current.getNumChildren() > 0) {
-        stackHead.children_added = true;
-        // We need to add the children
-        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = d_ppCache.find(childNode);
-          if (childFind == d_ppCache.end()) {
-            toVisit.push_back(childNode);
-          }
-        }
-      } else {
-        // No children, so we're done
-        Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl;
-        d_ppCache[current] = current;
-        toVisit.pop_back();
-      }
-    }
-  }
-
-  // Return the substituted version
-  return d_ppCache[assertion];
+  return d_tpp.theoryPreprocess(assertion);
 }
 
 void TheoryEngine::notifyPreprocessedAssertions(
@@ -1881,49 +1608,27 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                      << CheckSatCommand(n.toExpr());
   }
 
-  AssertionPipeline additionalLemmas;
-
-  // Run theory preprocessing, maybe
-  Node ppNode = preprocess ? this->preprocess(node) : Node(node);
-
-  // Remove the ITEs
-  Debug("ite") << "Remove ITE from " << ppNode << std::endl;
-  additionalLemmas.push_back(ppNode);
-  additionalLemmas.updateRealAssertionsEnd();
-  d_tform_remover.run(additionalLemmas.ref(),
-                      additionalLemmas.getIteSkolemMap());
-  Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
-  additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0]));
-
-  if(Debug.isOn("lemma-ites")) {
-    Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
-    Debug("lemma-ites") << " + now have the following "
-                        << additionalLemmas.size() << " lemma(s):" << endl;
-    for(std::vector<Node>::const_iterator i = additionalLemmas.begin();
-        i != additionalLemmas.end();
-        ++i) {
-      Debug("lemma-ites") << " + " << *i << endl;
-    }
-    Debug("lemma-ites") << endl;
-  }
-
-  // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
-  for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
-    additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i]));
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
+  // the assertion pipeline storing the lemmas
+  AssertionPipeline lemmas;
+  // call preprocessor
+  d_tpp.preprocess(node, lemmas, preprocess);
+  // assert lemmas to prop engine
+  for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
+  {
+    d_propEngine->assertLemma(
+        lemmas[i], i == 0 && negated, removable, rule, node);
   }
 
-  // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+  // WARNING: Below this point don't assume lemmas[0] to be not negated.
   if(negated) {
-    additionalLemmas.replace(0, additionalLemmas[0].notNode());
+    lemmas.replace(0, lemmas[0].notNode());
     negated = false;
   }
 
   // assert to decision engine
   if (!removable)
   {
-    d_propEngine->addAssertionsToDecisionEngine(additionalLemmas);
+    d_propEngine->addAssertionsToDecisionEngine(lemmas);
   }
 
   // Mark that we added some lemmas
@@ -1931,12 +1636,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
 
   // Lemma analysis isn't online yet; this lemma may only live for this
   // user level.
-  Node retLemma = additionalLemmas[0];
-  if (additionalLemmas.size() > 1)
+  Node retLemma = lemmas[0];
+  if (lemmas.size() > 1)
   {
     // the returned lemma is the conjunction of all additional lemmas.
-    retLemma =
-        NodeManager::currentNM()->mkNode(kind::AND, additionalLemmas.ref());
+    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
   }
   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
 }
@@ -2379,26 +2083,4 @@ void TheoryEngine::spendResource(ResourceManager::Resource r)
   d_resourceManager->spendResource(r);
 }
 
-TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
-    conflicts(getStatsPrefix(theory) + "::conflicts", 0),
-    propagations(getStatsPrefix(theory) + "::propagations", 0),
-    lemmas(getStatsPrefix(theory) + "::lemmas", 0),
-    requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
-    restartDemands(getStatsPrefix(theory) + "::restartDemands", 0)
-{
-  smtStatisticsRegistry()->registerStat(&conflicts);
-  smtStatisticsRegistry()->registerStat(&propagations);
-  smtStatisticsRegistry()->registerStat(&lemmas);
-  smtStatisticsRegistry()->registerStat(&requirePhase);
-  smtStatisticsRegistry()->registerStat(&restartDemands);
-}
-
-TheoryEngine::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&conflicts);
-  smtStatisticsRegistry()->unregisterStat(&propagations);
-  smtStatisticsRegistry()->unregisterStat(&lemmas);
-  smtStatisticsRegistry()->unregisterStat(&requirePhase);
-  smtStatisticsRegistry()->unregisterStat(&restartDemands);
-}
-
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 233047321..1557495a0 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -36,6 +36,7 @@
 #include "smt/command.h"
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
+#include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
 #include "theory/shared_terms_database.h"
@@ -43,6 +44,7 @@
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
+#include "theory/theory_preprocessor.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
@@ -114,6 +116,7 @@ class TheoryEngine {
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
   friend class theory::quantifiers::TermDb;
+  friend class theory::EngineOutputChannel;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
@@ -217,11 +220,6 @@ class TheoryEngine {
   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   /**
-  * Cache for theory-preprocessing of assertions
-   */
-  NodeMap d_ppCache;
-
-  /**
    * Used for "missed-t-propagations" dumping mode only.  A set of all
    * theory-propagable literals.
    */
@@ -234,115 +232,10 @@ class TheoryEngine {
    */
   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
-
-  /**
-   * Statistics for a particular theory.
-   */
-  class Statistics {
-
-    static std::string mkName(std::string prefix,
-                              theory::TheoryId theory,
-                              std::string suffix) {
-      std::stringstream ss;
-      ss << prefix << theory << suffix;
-      return ss.str();
-    }
-
-   public:
-    IntStat conflicts, propagations, lemmas, requirePhase, restartDemands;
-
-    Statistics(theory::TheoryId theory);
-    ~Statistics();
-  };/* class TheoryEngine::Statistics */
-
-  /**
-   * An output channel for Theory that passes messages
-   * back to a TheoryEngine.
-   */
-  class EngineOutputChannel : public theory::OutputChannel {
-    friend class TheoryEngine;
-
-    /**
-     * The theory engine we're communicating with.
-     */
-    TheoryEngine* d_engine;
-
-    /**
-     * The statistics of the theory interractions.
-     */
-    Statistics d_statistics;
-
-    /** The theory owning this channel. */
-    theory::TheoryId d_theory;
-
-   public:
-    EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory)
-        : d_engine(engine), d_statistics(theory), d_theory(theory) {}
-
-    void safePoint(ResourceManager::Resource r) override
-    {
-      spendResource(r);
-      if (d_engine->d_interrupted) {
-        throw theory::Interrupted();
-      }
-    }
-
-    void conflict(TNode conflictNode,
-                  std::unique_ptr<Proof> pf = nullptr) override;
-    bool propagate(TNode literal) override;
-
-    theory::LemmaStatus lemma(TNode lemma, ProofRule rule,
-                              bool removable = false, bool preprocess = false,
-                              bool sendAtoms = false) override;
-
-    theory::LemmaStatus splitLemma(TNode lemma,
-                                   bool removable = false) override;
-
-    void demandRestart() override {
-      NodeManager* curr = NodeManager::currentNM();
-      Node restartVar = curr->mkSkolem(
-          "restartVar", curr->booleanType(),
-          "A boolean variable asserted to be true to force a restart");
-      Trace("theory::restart")
-          << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar
-          << ")" << std::endl;
-      ++d_statistics.restartDemands;
-      lemma(restartVar, RULE_INVALID, true);
-    }
-
-    void requirePhase(TNode n, bool phase) override {
-      Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", "
-                      << phase << ")" << std::endl;
-      ++d_statistics.requirePhase;
-      d_engine->d_propEngine->requirePhase(n, phase);
-    }
-
-    void setIncomplete() override {
-      Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
-      d_engine->setIncomplete(d_theory);
-    }
-
-    void spendResource(ResourceManager::Resource r) override
-    {
-      d_engine->spendResource(r);
-    }
-
-    void handleUserAttribute(const char* attr, theory::Theory* t) override {
-      d_engine->handleUserAttribute(attr, t);
-    }
-
-   private:
-    /**
-     * A helper function for registering lemma recipes with the proof engine
-     */
-    void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess,
-                             theory::TheoryId theoryId);
-  }; /* class TheoryEngine::EngineOutputChannel */
-
   /**
    * Output channels for individual theories.
    */
-  EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
+  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
 
   /**
    * Are we in conflict.
@@ -450,11 +343,12 @@ class TheoryEngine {
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
 
-  RemoveTermFormulas& d_tform_remover;
-
   /** sort inference module */
   SortInference d_sortInfer;
 
+  /** The theory preprocessor */
+  theory::TheoryPreprocessor d_tpp;
+
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -488,7 +382,7 @@ class TheoryEngine {
   inline void addTheory(theory::TheoryId theoryId)
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
-    d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
+    d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] = new TheoryClass(d_context,
                                               d_userContext,
                                               *d_theoryOut[theoryId],
@@ -543,11 +437,6 @@ class TheoryEngine {
 
  private:
   /**
-   * Helper for preprocess
-   */
-  Node ppTheoryRewrite(TNode term);
-
-  /**
    * Queue of nodes for pre-registration.
    */
   std::queue<TNode> d_preregisterQueue;
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
new file mode 100644
index 000000000..7e5d1904d
--- /dev/null
+++ b/src/theory/theory_preprocessor.cpp
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file theory_preprocessor.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory preprocessor
+ **/
+
+#include "theory/theory_preprocessor.h"
+
+#include "theory/logic_info.h"
+#include "theory/rewriter.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+
+TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
+                                       RemoveTermFormulas& tfr)
+    : d_engine(engine),
+      d_logicInfo(engine.getLogicInfo()),
+      d_ppCache(),
+      d_tfr(tfr)
+{
+}
+
+TheoryPreprocessor::~TheoryPreprocessor() {}
+
+void TheoryPreprocessor::clearCache() { d_ppCache.clear(); }
+
+void TheoryPreprocessor::preprocess(TNode node,
+                                    preprocessing::AssertionPipeline& lemmas,
+                                    bool doTheoryPreprocess)
+{
+  // Run theory preprocessing, maybe
+  Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node);
+
+  // Remove the ITEs
+  Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl;
+  lemmas.push_back(ppNode);
+  lemmas.updateRealAssertionsEnd();
+  d_tfr.run(lemmas.ref(), lemmas.getIteSkolemMap());
+  Trace("te-tform-rm") << "..done " << lemmas[0] << std::endl;
+
+  if (Debug.isOn("lemma-ites"))
+  {
+    Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
+    Debug("lemma-ites") << " + now have the following " << lemmas.size()
+                        << " lemma(s):" << endl;
+    for (std::vector<Node>::const_iterator i = lemmas.begin();
+         i != lemmas.end();
+         ++i)
+    {
+      Debug("lemma-ites") << " + " << *i << endl;
+    }
+    Debug("lemma-ites") << endl;
+  }
+
+  // now, rewrite the lemmas
+  Node retLemma;
+  for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
+  {
+    Node rewritten = Rewriter::rewrite(lemmas[i]);
+    lemmas.replace(i, rewritten);
+  }
+}
+
+struct preprocess_stack_element
+{
+  TNode node;
+  bool children_added;
+  preprocess_stack_element(TNode n) : node(n), children_added(false) {}
+};
+
+Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
+{
+  Trace("theory::preprocess")
+      << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
+  // spendResource();
+
+  // Do a topological sort of the subexpressions and substitute them
+  vector<preprocess_stack_element> toVisit;
+  toVisit.push_back(assertion);
+
+  while (!toVisit.empty())
+  {
+    // The current node we are processing
+    preprocess_stack_element& stackHead = toVisit.back();
+    TNode current = stackHead.node;
+
+    Debug("theory::internal")
+        << "TheoryPreprocessor::theoryPreprocess(" << assertion
+        << "): processing " << current << endl;
+
+    // If node already in the cache we're done, pop from the stack
+    NodeMap::iterator find = d_ppCache.find(current);
+    if (find != d_ppCache.end())
+    {
+      toVisit.pop_back();
+      continue;
+    }
+
+    if (!d_logicInfo.isTheoryEnabled(Theory::theoryOf(current))
+        && Theory::theoryOf(current) != THEORY_SAT_SOLVER)
+    {
+      stringstream ss;
+      ss << "The logic was specified as " << d_logicInfo.getLogicString()
+         << ", which doesn't include " << Theory::theoryOf(current)
+         << ", but got a preprocessing-time fact for that theory." << endl
+         << "The fact:" << endl
+         << current;
+      throw LogicException(ss.str());
+    }
+
+    // If this is an atom, we preprocess its terms with the theory ppRewriter
+    if (Theory::theoryOf(current) != THEORY_BOOL)
+    {
+      Node ppRewritten = ppTheoryRewrite(current);
+      d_ppCache[current] = ppRewritten;
+      Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
+      continue;
+    }
+
+    // Not yet substituted, so process
+    if (stackHead.children_added)
+    {
+      // Children have been processed, so substitute
+      NodeBuilder<> builder(current.getKind());
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        builder << current.getOperator();
+      }
+      for (unsigned i = 0; i < current.getNumChildren(); ++i)
+      {
+        Assert(d_ppCache.find(current[i]) != d_ppCache.end());
+        builder << d_ppCache[current[i]];
+      }
+      // Mark the substitution and continue
+      Node result = builder;
+      if (result != current)
+      {
+        result = Rewriter::rewrite(result);
+      }
+      Debug("theory::internal")
+          << "TheoryPreprocessor::theoryPreprocess(" << assertion
+          << "): setting " << current << " -> " << result << endl;
+      d_ppCache[current] = result;
+      toVisit.pop_back();
+    }
+    else
+    {
+      // Mark that we have added the children if any
+      if (current.getNumChildren() > 0)
+      {
+        stackHead.children_added = true;
+        // We need to add the children
+        for (TNode::iterator child_it = current.begin();
+             child_it != current.end();
+             ++child_it)
+        {
+          TNode childNode = *child_it;
+          NodeMap::iterator childFind = d_ppCache.find(childNode);
+          if (childFind == d_ppCache.end())
+          {
+            toVisit.push_back(childNode);
+          }
+        }
+      }
+      else
+      {
+        // No children, so we're done
+        Debug("substitution::internal")
+            << "SubstitutionMap::internalSubstitute(" << assertion
+            << "): setting " << current << " -> " << current << endl;
+        d_ppCache[current] = current;
+        toVisit.pop_back();
+      }
+    }
+  }
+
+  // Return the substituted version
+  return d_ppCache[assertion];
+}
+
+// Recursively traverse a term and call the theory rewriter on its sub-terms
+Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
+{
+  NodeMap::iterator find = d_ppCache.find(term);
+  if (find != d_ppCache.end())
+  {
+    return (*find).second;
+  }
+  unsigned nc = term.getNumChildren();
+  if (nc == 0)
+  {
+    return d_engine.theoryOf(term)->ppRewrite(term);
+  }
+  Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
+
+  Node newTerm;
+  // do not rewrite inside quantifiers
+  if (term.isClosure())
+  {
+    newTerm = Rewriter::rewrite(term);
+  }
+  else
+  {
+    NodeBuilder<> newNode(term.getKind());
+    if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      newNode << term.getOperator();
+    }
+    unsigned i;
+    for (i = 0; i < nc; ++i)
+    {
+      newNode << ppTheoryRewrite(term[i]);
+    }
+    newTerm = Rewriter::rewrite(Node(newNode));
+  }
+  Node newTerm2 = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
+  if (newTerm != newTerm2)
+  {
+    newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
+  }
+  d_ppCache[term] = newTerm;
+  Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
+  return newTerm;
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
new file mode 100644
index 000000000..f6caa10ec
--- /dev/null
+++ b/src/theory/theory_preprocessor.h
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file theory_preprocessor.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory preprocessor.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H
+#define CVC4__THEORY__THEORY_PREPROCESSOR_H
+
+#include <unordered_map>
+
+#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+
+namespace CVC4 {
+
+class LogicInfo;
+class TheoryEngine;
+class RemoveTermFormulas;
+class LazyCDProof;
+
+namespace theory {
+
+/**
+ * The preprocessor used in TheoryEngine.
+ */
+class TheoryPreprocessor
+{
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+  /** Constructs a theory preprocessor */
+  TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr);
+  /** Destroys a theory preprocessor */
+  ~TheoryPreprocessor();
+  /** Clear the cache of this class */
+  void clearCache();
+  /**
+   * Preprocesses node and stores it along with lemmas generated by
+   * preprocessing into the assertion pipeline lemmas. The (optional) argument
+   * lcp is the proof that stores a proof of all top-level formulas in lemmas,
+   * assuming that lcp initially contains a proof of node. The flag
+   * doTheoryPreprocess is whether we should run theory-specific preprocessing.
+   */
+  void preprocess(TNode node,
+                  preprocessing::AssertionPipeline& lemmas,
+                  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.
+   */
+  Node theoryPreprocess(TNode node);
+
+ private:
+  /** Reference to owning theory engine */
+  TheoryEngine& d_engine;
+  /** Logic info of theory engine */
+  const LogicInfo& d_logicInfo;
+  /** Cache for theory-preprocessing of assertions */
+  NodeMap d_ppCache;
+  /** The term formula remover */
+  RemoveTermFormulas& d_tfr;
+  /** Helper for theoryPreprocess */
+  Node ppTheoryRewrite(TNode term);
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */