Split preprocessor from SmtEngine (#4854)

This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).

It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.

15 files changed, 383 insertions, 230 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 92f197252..6bbc2d29b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -249,6 +249,8 @@ libcvc4_add_sources(
   smt/model_blocker.h
   smt/options_manager.cpp
   smt/options_manager.h
+  smt/preprocessor.cpp
+  smt/preprocessor.h
   smt/preprocess_proof_generator.cpp
   smt/preprocess_proof_generator.h
   smt/process_assertions.cpp
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0963c704b..e69c9a1de 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4952,7 +4952,7 @@ Term Solver::getValue(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_TERM(term);
-  return Term(this, d_smtEngine->getValue(term.d_node->toExpr()));
+  return Term(this, d_smtEngine->getValue(*term.d_node));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 900651e1d..9ec522141 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1185,7 +1185,7 @@ void DeclareFunctionCommandToStream(std::ostream& out,
   {
     out << tn;
   }
-  Node val = Node::fromExpr(model.getSmtEngine()->getValue(n.toExpr()));
+  Node val = model.getSmtEngine()->getValue(n);
   if (options::modelUninterpDtEnum() && val.getKind() == kind::STORE)
   {
     TypeNode type_node = val[1].getType();
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 45cc2426c..7560b2ce4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1455,8 +1455,7 @@ void Smt2Printer::toStream(std::ostream& out,
       // don't print out internal stuff
       return;
     }
-    Node val =
-        Node::fromExpr(theory_model->getSmtEngine()->getValue(n.toExpr()));
+    Node val = theory_model->getSmtEngine()->getValue(n);
     if (val.getKind() == kind::LAMBDA)
     {
       out << "(define-fun " << n << " " << val[0] << " "
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 52a9578dd..4d8f6d910 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1509,7 +1509,7 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    d_result = smtEngine->simplify(d_term);
+    d_result = smtEngine->simplify(Node::fromExpr(d_term)).toExpr();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (UnsafeInterruptException& e)
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
new file mode 100644
index 000000000..ea5ef2bad
--- /dev/null
+++ b/src/smt/preprocessor.cpp
@@ -0,0 +1,156 @@
+/*********************                                                        */
+/*! \file preprocessor.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 preprocessor of the SMT engine.
+ **/
+
+#include "smt/preprocessor.h"
+
+#include "options/smt_options.h"
+#include "smt/abstract_values.h"
+#include "smt/assertions.h"
+#include "smt/command.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+Preprocessor::Preprocessor(SmtEngine& smt,
+                           context::UserContext* u,
+                           AbstractValues& abs)
+    : d_smt(smt),
+      d_absValues(abs),
+      d_propagator(true, true),
+      d_assertionsProcessed(u, false),
+      d_processor(smt, *smt.getResourceManager()),
+      d_rtf(u)
+{
+}
+
+Preprocessor::~Preprocessor()
+{
+  if (d_propagator.getNeedsFinish())
+  {
+    d_propagator.finish();
+    d_propagator.setNeedsFinish(false);
+  }
+}
+
+void Preprocessor::finishInit()
+{
+  d_ppContext.reset(new preprocessing::PreprocessingPassContext(
+      &d_smt, &d_rtf, &d_propagator));
+
+  // initialize the preprocessing passes
+  d_processor.finishInit(d_ppContext.get());
+}
+
+bool Preprocessor::process(Assertions& as)
+{
+  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
+
+  // should not be called if empty
+  Assert(ap.size() != 0) << "Can only preprocess a non-empty list of assertions";
+
+  if (d_assertionsProcessed && options::incrementalSolving())
+  {
+    // TODO(b/1255): Substitutions in incremental mode should be managed with a
+    // proper data structure.
+    ap.enableStoreSubstsInAsserts();
+  }
+  else
+  {
+    ap.disableStoreSubstsInAsserts();
+  }
+
+  // process the assertions, return true if no conflict is discovered
+  return d_processor.apply(as);
+}
+
+void Preprocessor::postprocess(Assertions& as)
+{
+  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
+  // if incremental, compute which variables are assigned
+  if (options::incrementalSolving())
+  {
+    d_ppContext->recordSymbolsInAssertions(ap.ref());
+  }
+
+  // mark that we've processed assertions
+  d_assertionsProcessed = true;
+}
+
+void Preprocessor::clearLearnedLiterals()
+{
+  d_propagator.getLearnedLiterals().clear();
+}
+
+void Preprocessor::cleanup() { d_processor.cleanup(); }
+
+RemoveTermFormulas& Preprocessor::getTermFormulaRemover() { return d_rtf; }
+
+Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
+{
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  return expandDefinitions(n, cache, expandOnly);
+}
+
+Node Preprocessor::expandDefinitions(
+    const Node& node,
+    std::unordered_map<Node, Node, NodeHashFunction>& cache,
+    bool expandOnly)
+{
+  Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
+  // Substitute out any abstract values in node.
+  Node n = d_absValues.substituteAbstractValues(node);
+  if (options::typeChecking())
+  {
+    // Ensure node is type-checked at this point.
+    n.getType(true);
+  }
+  // expand only = true
+  return d_processor.expandDefinitions(n, cache, expandOnly);
+}
+
+Node Preprocessor::simplify(const Node& node, bool removeItes)
+{
+  Trace("smt") << "SMT simplify(" << node << ")" << endl;
+  if (Dump.isOn("benchmark"))
+  {
+    Dump("benchmark") << SimplifyCommand(node.toExpr());
+  }
+  Node nas = d_absValues.substituteAbstractValues(node);
+  if (options::typeChecking())
+  {
+    // ensure node is type-checked at this point
+    nas.getType(true);
+  }
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  Node n = d_processor.expandDefinitions(nas, cache);
+  Node ns = applySubstitutions(n);
+  if (removeItes)
+  {
+    // also remove ites if asked
+    ns = d_rtf.replace(ns);
+  }
+  return ns;
+}
+
+Node Preprocessor::applySubstitutions(TNode node)
+{
+  return Rewriter::rewrite(d_ppContext->getTopLevelSubstitutions().apply(node));
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
new file mode 100644
index 000000000..051fe8bee
--- /dev/null
+++ b/src/smt/preprocessor.h
@@ -0,0 +1,138 @@
+/*********************                                                        */
+/*! \file preprocessor.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 preprocessor of the SmtEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__PREPROCESSOR_H
+#define CVC4__SMT__PREPROCESSOR_H
+
+#include <vector>
+
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/process_assertions.h"
+#include "smt/term_formula_removal.h"
+#include "theory/booleans/circuit_propagator.h"
+
+namespace CVC4 {
+namespace smt {
+
+class AbstractValues;
+
+/**
+ * The preprocessor module of an SMT engine.
+ *
+ * This class is responsible for:
+ * (1) preprocessing the set of assertions from input before they are sent to
+ * the SMT solver,
+ * (2) implementing methods for expanding and simplifying formulas. The latter
+ * takes into account the substitutions inferred by this class.
+ */
+class Preprocessor
+{
+ public:
+  Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs);
+  ~Preprocessor();
+  /**
+   * Finish initialization
+   */
+  void finishInit();
+  /**
+   * Process the assertions that have been asserted in argument as. Returns
+   * true if no conflict was discovered while preprocessing them.
+   */
+  bool process(Assertions& as);
+  /**
+   * Postprocess assertions, called after the SmtEngine has finished
+   * giving the assertions to the SMT solver and before the assertions are
+   * cleared.
+   */
+  void postprocess(Assertions& as);
+  /**
+   * Clear learned literals from the Boolean propagator.
+   */
+  void clearLearnedLiterals();
+  /**
+   * Cleanup, which deletes the processing passes owned by this module. This
+   * is required to be done explicitly so that passes are deleted before the
+   * objects they refer to in the SmtEngine destructor.
+   */
+  void cleanup();
+  /**
+   * Simplify a formula without doing "much" work.  Does not involve
+   * the SAT Engine in the simplification, but uses the current
+   * definitions, assertions, and the current partial model, if one
+   * has been constructed.  It also involves theory normalization.
+   *
+   * @param n The node to simplify
+   * @param removeItes Whether to remove ITE (and other terms with formulas in
+   * term positions) from the result.
+   * @return The simplified term.
+   */
+  Node simplify(const Node& n, bool removeItes = false);
+  /**
+   * Expand the definitions in a term or formula n.  No other
+   * simplification or normalization is done.
+   *
+   * @param n The node to expand
+   * @param expandOnly if true, then the expandDefinitions function of
+   * TheoryEngine is not called on subterms of n.
+   * @return The expanded term.
+   */
+  Node expandDefinitions(const Node& n, bool expandOnly = false);
+  /** Same as above, with a cache of previous results. */
+  Node expandDefinitions(
+      const Node& n,
+      std::unordered_map<Node, Node, NodeHashFunction>& cache,
+      bool expandOnly = false);
+  /**
+   * Get the underlying term formula remover utility.
+   */
+  RemoveTermFormulas& getTermFormulaRemover();
+
+ private:
+  /**
+   * Apply substitutions that have been inferred by preprocessing, return the
+   * substituted form of node.
+   */
+  Node applySubstitutions(TNode node);
+  /** Reference to the parent SmtEngine */
+  SmtEngine& d_smt;
+  /** Reference to the abstract values utility */
+  AbstractValues& d_absValues;
+  /**
+   * A circuit propagator for non-clausal propositional deduction.
+   */
+  theory::booleans::CircuitPropagator d_propagator;
+  /**
+   * User-context-dependent flag of whether any assertions have been processed.
+   */
+  context::CDO<bool> d_assertionsProcessed;
+  /** The preprocessing pass context */
+  std::unique_ptr<preprocessing::PreprocessingPassContext> d_ppContext;
+  /**
+   * Process assertions module, responsible for implementing the preprocessing
+   * passes.
+   */
+  ProcessAssertions d_processor;
+  /**
+   * The term formula remover, responsible for eliminating formulas that occur
+   * in term contexts.
+   */
+  RemoveTermFormulas d_rtf;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 2a7efe1c0..b34682914 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -77,9 +77,11 @@ class ProcessAssertions
   /**
    * Expand definitions in term n. Return the expanded form of n.
    *
-   * If expandOnly is true, then the expandDefinitions function of TheoryEngine
-   * of the SmtEngine this calls is associated with is not called on subterms of
-   * n.
+   * @param n The node to expand
+   * @param cache Cache of previous results
+   * @param expandOnly if true, then the expandDefinitions function of
+   * TheoryEngine is not called on subterms of n.
+   * @return The expanded term.
    */
   Node expandDefinitions(TNode n,
                          NodeToNodeHashMap& cache,
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 43aa3b0c8..585c2819d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,16 +83,16 @@
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/expr_names.h"
 #include "smt/command.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
+#include "smt/expr_names.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/options_manager.h"
-#include "smt/process_assertions.h"
+#include "smt/preprocessor.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_stats.h"
 #include "smt/term_formula_removal.h"
@@ -155,31 +155,8 @@ namespace smt {
  */
 class SmtEnginePrivate
 {
-  SmtEngine& d_smt;
-
-  typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
-  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
-
-  /** A circuit propagator for non-clausal propositional deduction */
-  booleans::CircuitPropagator d_propagator;
-
-  /** Whether any assertions have been processed */
-  CDO<bool> d_assertionsProcessed;
-
-  // Cached true value
-  Node d_true;
-
-  /** The preprocessing pass context */
-  std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
-
-  /** Process assertions module */
-  ProcessAssertions d_processor;
-
  public:
 
-  /** Instance of the ITE remover */
-  RemoveTermFormulas d_iteRemover;
-
   /* Finishes the initialization of the private portion of SMTEngine. */
   void finishInit();
 
@@ -203,66 +180,12 @@ class SmtEnginePrivate
 
  public:
   SmtEnginePrivate(SmtEngine& smt)
-      : d_smt(smt),
-        d_propagator(true, true),
-        d_assertionsProcessed(smt.getUserContext(), false),
-        d_processor(smt, *smt.getResourceManager()),
-        d_iteRemover(smt.getUserContext()),
-        d_sygusConjectureStale(smt.getUserContext(), true)
+      : d_sygusConjectureStale(smt.getUserContext(), true)
   {
-    d_true = NodeManager::currentNM()->mkConst(true);
   }
 
   ~SmtEnginePrivate()
   {
-    if(d_propagator.getNeedsFinish()) {
-      d_propagator.finish();
-      d_propagator.setNeedsFinish(false);
-    }
-  }
-
-  void spendResource(ResourceManager::Resource r)
-  {
-    d_smt.getResourceManager()->spendResource(r);
-  }
-
-  ProcessAssertions* getProcessAssertions() { return &d_processor; }
-
-  Node applySubstitutions(TNode node)
-  {
-    return Rewriter::rewrite(
-        d_preprocessingPassContext->getTopLevelSubstitutions().apply(node));
-  }
-
-  /**
-   * Process the assertions that have been asserted.
-   */
-  void processAssertions(Assertions& as);
-
-  /** Process a user push.
-  */
-  void notifyPush() {
-  }
-
-  /**
-   * Process a user pop.  Clears out the non-context-dependent stuff in this
-   * SmtEnginePrivate.  Necessary to clear out our assertion vectors in case
-   * someone does a push-assert-pop without a check-sat. It also pops the
-   * last map of expression names from notifyPush.
-   */
-  void notifyPop() {
-    d_propagator.getLearnedLiterals().clear();
-  }
-  /**
-   * Simplify node "in" by expanding definitions and applying any
-   * substitutions learned from preprocessing.
-   */
-  Node simplify(TNode in) {
-    // Substitute out any abstract values in ex.
-    // Expand definitions.
-    NodeToNodeHashMap cache;
-    Node n = d_processor.expandDefinitions(in, cache).toExpr();
-    return applySubstitutions(n).toExpr();
   }
 };/* class SmtEnginePrivate */
 
@@ -302,6 +225,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_statisticsRegistry(nullptr),
       d_stats(nullptr),
       d_resourceManager(nullptr),
+      d_optm(nullptr),
+      d_pp(nullptr),
       d_scope(nullptr)
 {
   // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
@@ -327,6 +252,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_resourceManager.reset(
       new ResourceManager(*d_statisticsRegistry.get(), d_options));
   d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
+  d_pp.reset(
+      new smt::Preprocessor(*this, d_userContext.get(), *d_absValues.get()));
   d_private.reset(new smt::SmtEnginePrivate(*this));
   // listen to node manager events
   d_nodeManager->subscribeEvents(d_snmListener.get());
@@ -370,7 +297,7 @@ void SmtEngine::finishInit()
   d_theoryEngine.reset(new TheoryEngine(getContext(),
                                         getUserContext(),
                                         getResourceManager(),
-                                        d_private->d_iteRemover,
+                                        d_pp->getTermFormulaRemover(),
                                         const_cast<const LogicInfo&>(d_logic)));
 
   // Add the theories
@@ -435,7 +362,7 @@ void SmtEngine::finishInit()
           finishRegisterTheory(d_theoryEngine->theoryOf(id));
       }
     });
-  d_private->finishInit();
+  d_pp->finishInit();
   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 }
 
@@ -495,7 +422,7 @@ SmtEngine::~SmtEngine()
     d_definedFunctions->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
-    d_private->getProcessAssertions()->cleanup();
+    d_pp->cleanup();
 
     // d_proofManager is always created when proofs are enabled at configure
     // time.  Because of this, this code should not be wrapped in PROOF() which
@@ -522,6 +449,7 @@ SmtEngine::~SmtEngine()
     d_snmListener.reset(nullptr);
     d_routListener.reset(nullptr);
     d_optm.reset(nullptr);
+    d_pp.reset(nullptr);
     // d_resourceManager must be destroyed before d_statisticsRegistry
     d_resourceManager.reset(nullptr);
     d_statisticsRegistry.reset(nullptr);
@@ -990,15 +918,6 @@ bool SmtEngine::isDefinedFunction( Expr func ){
   return d_definedFunctions->find(nf) != d_definedFunctions->end();
 }
 
-void SmtEnginePrivate::finishInit()
-{
-  d_preprocessingPassContext.reset(
-      new PreprocessingPassContext(&d_smt, &d_iteRemover, &d_propagator));
-
-  // initialize the preprocessing passes
-  d_processor.finishInit(d_preprocessingPassContext.get());
-}
-
 Result SmtEngine::check() {
   Assert(d_fullyInited);
   Assert(d_pendingPops == 0);
@@ -1017,7 +936,7 @@ Result SmtEngine::check() {
 
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
-  d_private->processAssertions(*d_asserts);
+  processAssertionsInternal();
   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
 
   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
@@ -1080,68 +999,52 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   return m;
 }
 
-void SmtEnginePrivate::processAssertions(Assertions& as)
+void SmtEngine::processAssertionsInternal()
 {
-  TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
-  spendResource(ResourceManager::Resource::PreprocessStep);
-  Assert(d_smt.d_fullyInited);
-  Assert(d_smt.d_pendingPops == 0);
+  TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime);
+  d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
+  Assert(d_fullyInited);
+  Assert(d_pendingPops == 0);
 
-  AssertionPipeline& ap = as.getAssertionPipeline();
+  AssertionPipeline& ap = d_asserts->getAssertionPipeline();
 
   if (ap.size() == 0)
   {
     // nothing to do
     return;
   }
-  if (d_assertionsProcessed && options::incrementalSolving()) {
-    // TODO(b/1255): Substitutions in incremental mode should be managed with a
-    // proper data structure.
-
-    ap.enableStoreSubstsInAsserts();
-  }
-  else
-  {
-    ap.disableStoreSubstsInAsserts();
-  }
 
-  // process the assertions
-  bool noConflict = d_processor.apply(as);
+  // process the assertions with the preprocessor
+  bool noConflict = d_pp->process(*d_asserts);
 
   //notify theory engine new preprocessed assertions
-  d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
+  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
 
   // Push the formula to decision engine
   if (noConflict)
   {
     Chat() << "pushing to decision engine..." << endl;
-    d_smt.d_propEngine->addAssertionsToDecisionEngine(ap);
+    d_propEngine->addAssertionsToDecisionEngine(ap);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
-  // if incremental, compute which variables are assigned
-  if (options::incrementalSolving())
-  {
-    d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref());
-  }
+  d_pp->postprocess(*d_asserts);
 
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
+    TimerStat::CodeTimer codeTimer(d_stats->d_cnfConversionTime);
     for (const Node& assertion : ap.ref())
     {
       Chat() << "+ " << assertion << std::endl;
-      d_smt.d_propEngine->assertFormula(assertion);
+      d_propEngine->assertFormula(assertion);
     }
   }
 
-  d_assertionsProcessed = true;
-
   // clear the current assertions
-  as.clearCurrent();
+  d_asserts->clearCurrent();
 }
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
@@ -1617,85 +1520,42 @@ Result SmtEngine::checkSynth()
    --------------------------------------------------------------------------
 */
 
-Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
-  return node;
-}
-
-Expr SmtEngine::simplify(const Expr& ex)
+Node SmtEngine::simplify(const Node& ex)
 {
-  Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  Trace("smt") << "SMT simplify(" << ex << ")" << endl;
-
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SimplifyCommand(ex);
-  }
-
-  Expr e = d_absValues->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-  if( options::typeChecking() ) {
-    e.getType(true); // ensure expr is type-checked at this point
-  }
-
-  // Make sure all preprocessing is done
-  d_private->processAssertions(*d_asserts);
-  Node n = d_private->simplify(Node::fromExpr(e));
-  n = postprocess(n, TypeNode::fromType(e.getType()));
-  return n.toExpr();
+  // ensure we've processed assertions
+  processAssertionsInternal();
+  return d_pp->simplify(ex);
 }
 
 Node SmtEngine::expandDefinitions(const Node& ex)
 {
-  d_private->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
 
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl;
-
-  // Substitute out any abstract values in ex.
-  Node e = d_absValues->substituteAbstractValues(ex);
-  if(options::typeChecking()) {
-    // Ensure expr is type-checked at this point.
-    e.getType(true);
-  }
-
-  unordered_map<Node, Node, NodeHashFunction> cache;
-  Node n = d_private->getProcessAssertions()->expandDefinitions(
-      e, cache, /* expandOnly = */ true);
-  n = postprocess(n, e.getType());
-
-  return n;
+  // set expandOnly flag to true
+  return d_pp->expandDefinitions(ex, true);
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
-Expr SmtEngine::getValue(const Expr& ex) const
+Node SmtEngine::getValue(const Node& ex) const
 {
-  Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetValueCommand(ex);
+    Dump("benchmark") << GetValueCommand(ex.toExpr());
   }
+  TypeNode expectedType = ex.getType();
 
-  // Substitute out any abstract values in ex.
-  Expr e = d_absValues->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-
-  // Ensure expr is type-checked at this point.
-  e.getType(options::typeChecking());
-
-  // do not need to apply preprocessing substitutions (should be recorded
-  // in model already)
+  // Substitute out any abstract values in ex and expand
+  Node n = d_pp->expandDefinitions(ex);
 
-  Node n = Node::fromExpr(e);
   Trace("smt") << "--- getting value of " << n << endl;
-  TypeNode expectedType = n.getType();
-
-  // Expand, then normalize
-  unordered_map<Node, Node, NodeHashFunction> cache;
-  n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
   // There are two ways model values for terms are computed (for historical
   // reasons).  One way is that used in check-model; the other is that
   // used by the Model classes.  It's not clear to me exactly how these
@@ -1714,10 +1574,8 @@ Expr SmtEngine::getValue(const Expr& ex) const
     resultNode = m->getValue(n);
   }
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
-  resultNode = postprocess(resultNode, expectedType);
-  Trace("smt") << "--- model-post returned " << resultNode << endl;
-  Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
-  Trace("smt") << "--- model-post expected " << expectedType << endl;
+  Trace("smt") << "--- type " << resultNode.getType() << endl;
+  Trace("smt") << "--- expected type " << expectedType << endl;
 
   // type-check the result we got
   // Notice that lambdas have function type, which does not respect the subtype
@@ -1736,7 +1594,7 @@ Expr SmtEngine::getValue(const Expr& ex) const
     Trace("smt") << "--- abstract value >> " << resultNode << endl;
   }
 
-  return resultNode.toExpr();
+  return resultNode;
 }
 
 vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs)
@@ -1744,7 +1602,7 @@ vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs)
   vector<Expr> result;
   for (const Expr& e : exprs)
   {
-    result.push_back(getValue(e));
+    result.push_back(getValue(e).toExpr());
   }
   return result;
 }
@@ -1817,8 +1675,8 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
       Trace("smt") << "--- getting value of " << as << endl;
 
       // Expand, then normalize
-      unordered_map<Node, Node, NodeHashFunction> cache;
-      Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache);
+      std::unordered_map<Node, Node, NodeHashFunction> cache;
+      Node n = d_pp->expandDefinitions(as, cache);
       n = Rewriter::rewrite(n);
 
       Trace("smt") << "--- getting value of " << n << endl;
@@ -1955,7 +1813,7 @@ std::vector<Expr> SmtEngine::getExpandedAssertions()
   for (const Expr& e : easserts)
   {
     Node ea = Node::fromExpr(e);
-    Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache);
+    Node eae = d_pp->expandDefinitions(ea, cache);
     eassertsProc.push_back(eae.toExpr());
   }
   return eassertsProc;
@@ -2208,7 +2066,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     // Apply any define-funs from the problem.
     {
       unordered_map<Node, Node, NodeHashFunction> cache;
-      n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
+      n = d_pp->expandDefinitions(n, cache);
     }
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
@@ -2224,13 +2082,12 @@ void SmtEngine::checkModel(bool hardFailure) {
     n = m->getValue(n);
     Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
 
-    // Simplify the result.
-    n = d_private->simplify(n);
-    Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
-
-    // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
-    n = d_private->d_iteRemover.replace(n);
-    Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
+    // Simplify the result and replace the already-known ITEs (this is important
+    // for ground ITEs under quantifiers).
+    n = d_pp->simplify(n, true);
+    Notice()
+        << "SmtEngine::checkModel(): -- simplifies with ite replacement to  "
+        << n << endl;
 
     // Apply our model value substitutions (again), as things may have been simplified.
     Debug("boolean-terms") << "applying subses to " << n << endl;
@@ -2362,8 +2219,7 @@ void SmtEngine::checkSynthSolution()
              << assertion << endl;
     Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
     // Apply any define-funs from the problem.
-    Node n =
-        d_private->getProcessAssertions()->expandDefinitions(assertion, cache);
+    Node n = d_pp->expandDefinitions(assertion, cache);
     Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << n << endl;
     Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
     if (conjs.find(n) == conjs.end())
@@ -2714,8 +2570,7 @@ void SmtEngine::push()
   finalOptionsAreSet();
   doPendingPops();
   Trace("smt") << "SMT push()" << endl;
-  d_private->notifyPush();
-  d_private->processAssertions(*d_asserts);
+  processAssertionsInternal();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand();
   }
@@ -2766,7 +2621,8 @@ void SmtEngine::pop() {
 
   // Clear out assertion queues etc., in case anything is still in there
   d_asserts->clearCurrent();
-  d_private->notifyPop();
+  // clear the learned literals from the preprocessor
+  d_pp->clearLearnedLiterals();
 
   Trace("userpushpop") << "SmtEngine: popped to level "
                        << d_userContext->getLevel() << endl;
@@ -2779,7 +2635,7 @@ void SmtEngine::internalPush() {
   Trace("smt") << "SmtEngine::internalPush()" << endl;
   doPendingPops();
   if(options::incrementalSolving()) {
-    d_private->processAssertions(*d_asserts);
+    processAssertionsInternal();
     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
     d_userContext->push();
     // the d_context push is done inside of the SAT solver
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5dc0d74fa..3ae04a720 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -99,6 +99,7 @@ class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
 class OptionsManager;
+class Preprocessor;
 /** Subsolvers */
 class AbductionSolver;
 /**
@@ -506,7 +507,7 @@ class CVC4_PUBLIC SmtEngine
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(const Expr& e);
+  Node simplify(const Node& e);
 
   /**
    * Expand the definitions in a term or formula.  No other
@@ -524,7 +525,7 @@ class CVC4_PUBLIC SmtEngine
    * @throw ModalException, TypeCheckingException, LogicException,
    *        UnsafeInterruptException
    */
-  Expr getValue(const Expr& e) const;
+  Node getValue(const Node& e) const;
 
   /**
    * Same as getValue but for a vector of expressions
@@ -987,13 +988,6 @@ class CVC4_PUBLIC SmtEngine
   void checkAbduct(Node a);
 
   /**
-   * Postprocess a value for output to the user.  Involves doing things
-   * like turning datatypes back into tuples, length-1-bitvectors back
-   * into booleans, etc.
-   */
-  Node postprocess(TNode n, TypeNode expectedType) const;
-
-  /**
    * This is something of an "init" procedure, but is idempotent; call
    * as often as you like.  Should be called whenever the final options
    * and logic for the problem are set (at least, those options that are
@@ -1053,6 +1047,14 @@ class CVC4_PUBLIC SmtEngine
   void setLogicInternal();
 
   /**
+   * Process the assertions that have been asserted. This moves the set of
+   * assertions that have been buffered into the smt::Assertions object,
+   * preprocesses them, pushes them into the SMT solver, and clears the
+   * buffer.
+   */
+  void processAssertionsInternal();
+
+  /**
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
@@ -1197,12 +1199,6 @@ class CVC4_PUBLIC SmtEngine
    */
   bool d_needPostsolve;
 
-  /*
-   * Whether to call theory preprocessing during simplification - on
-   * by default* but gets turned off if arithRewriteEq is on
-   */
-  bool d_earlyTheoryPP;
-
   /**
    * Most recent result of last checkSatisfiability/checkEntailed or
    * (set-info :status).
@@ -1248,6 +1244,10 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<smt::OptionsManager> d_optm;
   /**
+   * The preprocessor.
+   */
+  std::unique_ptr<smt::Preprocessor> d_pp;
+  /**
    * The global scope object. Upon creation of this SmtEngine, it becomes the
    * SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
    * or another SmtEngine is created.
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 835dc1dba..07d798901 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -172,7 +172,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
             if (val.isNull())
             {
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
-              val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
+              val = rrChecker->getValue(refv);
             }
             Trace("rr-check") << "  " << v << " -> " << val << std::endl;
             pt.push_back(val);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index a7f32155c..9126aad94 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -597,7 +597,7 @@ void CegisCoreConnective::getModel(SmtEngine& smt,
 {
   for (const Node& v : d_vars)
   {
-    Node mv = Node::fromExpr(smt.getValue(v.toExpr()));
+    Node mv = smt.getValue(v);
     Trace("sygus-ccore-model") << v << " -> " << mv << " ";
     vals.push_back(mv);
   }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 2514b05e2..5ceac24b6 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -250,7 +250,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   {
     Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
     Node fov = d_sk_to_fo[v];
-    Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
+    Node fov_m = repcChecker->getValue(fov);
     Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
     // convert to sygus
     Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 2419962aa..8810acbe8 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -112,8 +112,8 @@ Result checkWithSubsolver(Node query,
   {
     for (const Node& v : vars)
     {
-      Expr val = smte->getValue(v.toExpr());
-      modelVals.push_back(Node::fromExpr(val));
+      Node val = smte->getValue(v);
+      modelVals.push_back(val);
     }
   }
   return r;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 70f46d6e5..4c7600da2 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -174,7 +174,7 @@ bool TheoryModel::isModelCoreSymbol(Expr sym) const
 Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
-  return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
+  return ret.toExpr();
 }
 
 /** get cardinality for sort */