Split ProcessAssertions module from SmtEngine (#4210)

This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.

The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:

A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.

10 files changed, 1288 insertions, 899 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 447ca90f8..dec5a7f16 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -223,6 +223,7 @@ libcvc4_add_sources(
   smt/command.h
   smt/command_list.cpp
   smt/command_list.h
+  smt/defined_function.h
   smt/dump.cpp
   smt/dump.h
   smt/logic_exception.h
@@ -236,12 +237,16 @@ libcvc4_add_sources(
   smt/model_core_builder.h
   smt/model_blocker.cpp
   smt/model_blocker.h
+  smt/process_assertions.cpp
+  smt/process_assertions.h
   smt/set_defaults.cpp
   smt/set_defaults.h
   smt/smt_engine.cpp
   smt/smt_engine.h
   smt/smt_engine_scope.cpp
   smt/smt_engine_scope.h
+  smt/smt_engine_stats.cpp
+  smt/smt_engine_stats.h
   smt/smt_statistics_registry.cpp
   smt/smt_statistics_registry.h
   smt/term_formula_removal.cpp
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 1c0351bcb..4865ccead 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -149,7 +149,6 @@ header = "options/arith_options.h"
   long       = "miplib-trick"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "turns on the preprocessing step of attempting to infer bounds on miplib problems"
 
 [[option]]
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
new file mode 100644
index 000000000..b141ef9cb
--- /dev/null
+++ b/src/smt/defined_function.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file defined_function.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 Defined function data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__DEFINED_FUNCTION_H
+#define CVC4__SMT__DEFINED_FUNCTION_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * Representation of a defined function.  We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction
+{
+ public:
+  DefinedFunction() {}
+  DefinedFunction(Node func, std::vector<Node>& formals, Node formula)
+      : d_func(func), d_formals(formals), d_formula(formula)
+  {
+  }
+  /** get the function */
+  Node getFunction() const { return d_func; }
+  /** get the formal argument list of the function */
+  const std::vector<Node>& getFormals() const { return d_formals; }
+  /** get the formula that defines it */
+  Node getFormula() const { return d_formula; }
+
+ private:
+  /** the function */
+  Node d_func;
+  /** the formal argument list */
+  std::vector<Node> d_formals;
+  /** the formula */
+  Node d_formula;
+}; /* class DefinedFunction */
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__DEFINED_FUNCTION_H */
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
new file mode 100644
index 000000000..0e2701a1a
--- /dev/null
+++ b/src/smt/process_assertions.cpp
@@ -0,0 +1,871 @@
+/*********************                                                        */
+/*! \file process_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
+ ** 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 Implementation of module for processing assertions for an SMT engine.
+ **/
+
+#include "smt/process_assertions.h"
+
+#include <stack>
+#include <utility>
+
+#include "expr/node_manager_attributes.h"
+#include "options/arith_options.h"
+#include "options/base_options.h"
+#include "options/bv_options.h"
+#include "options/proof_options.h"
+#include "options/quantifiers_options.h"
+#include "options/sep_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_registry.h"
+#include "smt/defined_function.h"
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+#include "theory/quantifiers/fun_def_process.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::preprocessing;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace smt {
+
+/** Useful for counting the number of recursive calls. */
+class ScopeCounter
+{
+ public:
+  ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
+  ~ScopeCounter() { --d_depth; }
+
+ private:
+  unsigned& d_depth;
+};
+
+ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm)
+    : d_smt(smt),
+      d_resourceManager(rm),
+      d_preprocessingPassContext(nullptr),
+      d_fmfRecFunctionsDefined(nullptr)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_fmfRecFunctionsDefined = new (true) NodeList(d_smt.getUserContext());
+}
+
+ProcessAssertions::~ProcessAssertions()
+{
+  d_fmfRecFunctionsDefined->deleteSelf();
+}
+
+void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
+{
+  Assert(d_preprocessingPassContext == nullptr);
+  d_preprocessingPassContext = pc;
+
+  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
+  // TODO: this will likely change when we add support for actually assembling
+  // preprocessing pipelines. For now, we just create an instance of each
+  // available preprocessing pass.
+  std::vector<std::string> passNames = ppReg.getAvailablePasses();
+  for (const std::string& passName : passNames)
+  {
+    d_passes[passName].reset(
+        ppReg.createPass(d_preprocessingPassContext, passName));
+  }
+}
+
+void ProcessAssertions::cleanup() { d_passes.clear(); }
+
+void ProcessAssertions::spendResource(ResourceManager::Resource r)
+{
+  d_resourceManager.spendResource(r);
+}
+
+bool ProcessAssertions::apply(AssertionPipeline& assertions)
+{
+  Assert(d_preprocessingPassContext != nullptr);
+  // Dump the assertions
+  dumpAssertions("pre-everything", assertions);
+
+  Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
+  Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
+
+  Debug("smt") << "#Assertions : " << assertions.size() << endl;
+  Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
+
+  if (assertions.size() == 0)
+  {
+    // nothing to do
+    return true;
+  }
+
+  SubstitutionMap& top_level_substs =
+      d_preprocessingPassContext->getTopLevelSubstitutions();
+
+  if (options::bvGaussElim())
+  {
+    d_passes["bv-gauss"]->apply(&assertions);
+  }
+
+  // Add dummy assertion in last position - to be used as a
+  // placeholder for any new assertions to get added
+  assertions.push_back(d_true);
+  // any assertions added beyond realAssertionsEnd must NOT affect the
+  // equisatisfiability
+  assertions.updateRealAssertionsEnd();
+
+  // Assertions are NOT guaranteed to be rewritten by this point
+
+  Trace("smt-proc")
+      << "ProcessAssertions::processAssertions() : pre-definition-expansion"
+      << endl;
+  dumpAssertions("pre-definition-expansion", assertions);
+  {
+    Chat() << "expanding definitions..." << endl;
+    Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions"
+                      << endl;
+    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
+    unordered_map<Node, Node, NodeHashFunction> cache;
+    for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
+    {
+      assertions.replace(i, expandDefinitions(assertions[i], cache));
+    }
+  }
+  Trace("smt-proc")
+      << "ProcessAssertions::processAssertions() : post-definition-expansion"
+      << endl;
+  dumpAssertions("post-definition-expansion", assertions);
+
+  // save the assertions now
+  THEORY_PROOF(
+      for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) {
+        ProofManager::currentPM()->addAssertion(assertions[i].toExpr());
+      });
+
+  Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+  if (options::globalNegate())
+  {
+    // global negation of the formula
+    d_passes["global-negate"]->apply(&assertions);
+    d_smt.d_globalNegation = !d_smt.d_globalNegation;
+  }
+
+  if (options::nlExtPurify())
+  {
+    d_passes["nl-ext-purify"]->apply(&assertions);
+  }
+
+  if (options::solveRealAsInt())
+  {
+    d_passes["real-to-int"]->apply(&assertions);
+  }
+
+  if (options::solveIntAsBV() > 0)
+  {
+    d_passes["int-to-bv"]->apply(&assertions);
+  }
+
+  if (options::ackermann())
+  {
+    d_passes["ackermann"]->apply(&assertions);
+  }
+
+  if (options::bvAbstraction())
+  {
+    d_passes["bv-abstraction"]->apply(&assertions);
+  }
+
+  Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+  bool noConflict = true;
+
+  if (options::extRewPrep())
+  {
+    d_passes["ext-rew-pre"]->apply(&assertions);
+  }
+
+  // Unconstrained simplification
+  if (options::unconstrainedSimp())
+  {
+    d_passes["rewrite"]->apply(&assertions);
+    d_passes["unconstrained-simplifier"]->apply(&assertions);
+  }
+
+  if (options::bvIntroducePow2())
+  {
+    d_passes["bv-intro-pow2"]->apply(&assertions);
+  }
+
+  // Since this pass is not robust for the information tracking necessary for
+  // unsat cores, it's only applied if we are not doing unsat core computation
+  if (!options::unsatCores())
+  {
+    d_passes["apply-substs"]->apply(&assertions);
+  }
+
+  // Assertions MUST BE guaranteed to be rewritten by this point
+  d_passes["rewrite"]->apply(&assertions);
+
+  // Lift bit-vectors of size 1 to bool
+  if (options::bitvectorToBool())
+  {
+    d_passes["bv-to-bool"]->apply(&assertions);
+  }
+  if (options::solveBVAsInt() > 0)
+  {
+    d_passes["bv-to-int"]->apply(&assertions);
+  }
+
+  // Convert non-top-level Booleans to bit-vectors of size 1
+  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+  {
+    d_passes["bool-to-bv"]->apply(&assertions);
+  }
+  if (options::sepPreSkolemEmp())
+  {
+    d_passes["sep-skolem-emp"]->apply(&assertions);
+  }
+
+  if (d_smt.d_logic.isQuantified())
+  {
+    // remove rewrite rules, apply pre-skolemization to existential quantifiers
+    d_passes["quantifiers-preprocess"]->apply(&assertions);
+    if (options::macrosQuant())
+    {
+      // quantifiers macro expansion
+      d_passes["quantifier-macros"]->apply(&assertions);
+    }
+
+    // fmf-fun : assume admissible functions, applying preprocessing reduction
+    // to FMF
+    if (options::fmfFunWellDefined())
+    {
+      quantifiers::FunDefFmf fdf;
+      Assert(d_fmfRecFunctionsDefined != NULL);
+      // must carry over current definitions (in case of incremental)
+      for (context::CDList<Node>::const_iterator fit =
+               d_fmfRecFunctionsDefined->begin();
+           fit != d_fmfRecFunctionsDefined->end();
+           ++fit)
+      {
+        Node f = (*fit);
+        Assert(d_fmfRecFunctionsAbs.find(f) != d_fmfRecFunctionsAbs.end());
+        TypeNode ft = d_fmfRecFunctionsAbs[f];
+        fdf.d_sorts[f] = ft;
+        std::map<Node, std::vector<Node>>::iterator fcit =
+            d_fmfRecFunctionsConcrete.find(f);
+        Assert(fcit != d_fmfRecFunctionsConcrete.end());
+        for (const Node& fcc : fcit->second)
+        {
+          fdf.d_input_arg_inj[f].push_back(fcc);
+        }
+      }
+      fdf.simplify(assertions.ref());
+      // must store new definitions (in case of incremental)
+      for (const Node& f : fdf.d_funcs)
+      {
+        d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
+        d_fmfRecFunctionsConcrete[f].clear();
+        for (const Node& fcc : fdf.d_input_arg_inj[f])
+        {
+          d_fmfRecFunctionsConcrete[f].push_back(fcc);
+        }
+        d_fmfRecFunctionsDefined->push_back(f);
+      }
+    }
+  }
+
+  if (options::sortInference() || options::ufssFairnessMonotone())
+  {
+    d_passes["sort-inference"]->apply(&assertions);
+  }
+
+  if (options::pbRewrites())
+  {
+    d_passes["pseudo-boolean-processor"]->apply(&assertions);
+  }
+
+  // rephrasing normal inputs as sygus problems
+  if (!d_smt.d_isInternalSubsolver)
+  {
+    if (options::sygusInference())
+    {
+      d_passes["sygus-infer"]->apply(&assertions);
+    }
+    else if (options::sygusRewSynthInput())
+    {
+      // do candidate rewrite rule synthesis
+      d_passes["synth-rr"]->apply(&assertions);
+    }
+  }
+
+  Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
+                    << endl;
+  dumpAssertions("pre-simplify", assertions);
+  Chat() << "simplifying assertions..." << endl;
+  noConflict = simplifyAssertions(assertions);
+  if (!noConflict)
+  {
+    ++(d_smt.d_stats->d_simplifiedToFalse);
+  }
+  Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
+                    << endl;
+  dumpAssertions("post-simplify", assertions);
+
+  if (options::doStaticLearning())
+  {
+    d_passes["static-learning"]->apply(&assertions);
+  }
+  Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+  {
+    d_smt.d_stats->d_numAssertionsPre += assertions.size();
+    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.
+    d_passes["apply-substs"]->apply(&assertions);
+    d_smt.d_stats->d_numAssertionsPost += assertions.size();
+  }
+
+  dumpAssertions("pre-repeat-simplify", assertions);
+  if (options::repeatSimp())
+  {
+    Trace("smt-proc")
+        << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
+        << endl;
+    Chat() << "re-simplifying assertions..." << endl;
+    ScopeCounter depth(d_simplifyAssertionsDepth);
+    noConflict &= simplifyAssertions(assertions);
+    if (noConflict)
+    {
+      // Need to fix up assertion list to maintain invariants:
+      // Let Sk be the set of Skolem variables introduced by ITE's.  Let <_sk be
+      // the order in which these variables were introduced during ite removal.
+      // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr
+      // mapped to by sk.
+
+      // cache for expression traversal
+      unordered_map<Node, bool, NodeHashFunction> cache;
+
+      IteSkolemMap& iskMap = assertions.getIteSkolemMap();
+      // First, find all skolems that appear in the substitution map - their
+      // associated iteExpr will need to be moved to the main assertion set
+      set<TNode> skolemSet;
+      SubstitutionMap::iterator pos = top_level_substs.begin();
+      for (; pos != top_level_substs.end(); ++pos)
+      {
+        collectSkolems(iskMap, (*pos).first, skolemSet, cache);
+        collectSkolems(iskMap, (*pos).second, skolemSet, cache);
+      }
+      // We need to ensure:
+      // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
+      // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
+      // If either of these is violated, we must add iteExpr as a proper
+      // assertion
+      IteSkolemMap::iterator it = iskMap.begin();
+      IteSkolemMap::iterator iend = iskMap.end();
+      NodeBuilder<> builder(AND);
+      builder << assertions[assertions.getRealAssertionsEnd() - 1];
+      vector<TNode> toErase;
+      for (; it != iend; ++it)
+      {
+        if (skolemSet.find((*it).first) == skolemSet.end())
+        {
+          TNode iteExpr = assertions[(*it).second];
+          if (iteExpr.getKind() == ITE && iteExpr[1].getKind() == EQUAL
+              && iteExpr[1][0] == (*it).first && iteExpr[2].getKind() == EQUAL
+              && iteExpr[2][0] == (*it).first)
+          {
+            cache.clear();
+            bool bad =
+                checkForBadSkolems(iskMap, iteExpr[0], (*it).first, cache);
+            bad = bad
+                  || checkForBadSkolems(
+                         iskMap, iteExpr[1][1], (*it).first, cache);
+            bad = bad
+                  || checkForBadSkolems(
+                         iskMap, iteExpr[2][1], (*it).first, cache);
+            if (!bad)
+            {
+              continue;
+            }
+          }
+        }
+        // Move this iteExpr into the main assertions
+        builder << assertions[(*it).second];
+        assertions[(*it).second] = d_true;
+        toErase.push_back((*it).first);
+      }
+      if (builder.getNumChildren() > 1)
+      {
+        while (!toErase.empty())
+        {
+          iskMap.erase(toErase.back());
+          toErase.pop_back();
+        }
+        assertions[assertions.getRealAssertionsEnd() - 1] =
+            Rewriter::rewrite(Node(builder));
+      }
+      // TODO(b/1256): For some reason this is needed for some benchmarks, such
+      // as
+      // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+      d_passes["ite-removal"]->apply(&assertions);
+      d_passes["apply-substs"]->apply(&assertions);
+    }
+    Trace("smt-proc")
+        << "ProcessAssertions::processAssertions() : post-repeat-simplify"
+        << endl;
+  }
+  dumpAssertions("post-repeat-simplify", assertions);
+
+  if (options::ufHo())
+  {
+    d_passes["ho-elim"]->apply(&assertions);
+  }
+
+  // begin: INVARIANT to maintain: no reordering of assertions or
+  // introducing new ones
+
+  Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+  Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
+               << endl;
+  Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+  d_passes["theory-preprocess"]->apply(&assertions);
+
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    d_passes["bv-eager-atoms"]->apply(&assertions);
+  }
+
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
+  dumpAssertions("post-everything", assertions);
+
+  return noConflict;
+}
+
+// returns false if simplification led to "false"
+bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
+{
+  spendResource(ResourceManager::Resource::PreprocessStep);
+  Assert(d_smt.d_pendingPops == 0);
+  try
+  {
+    ScopeCounter depth(d_simplifyAssertionsDepth);
+
+    Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
+
+    if (options::simplificationMode() != options::SimplificationMode::NONE)
+    {
+      if (!options::unsatCores() && !options::fewerPreprocessingHoles())
+      {
+        // Perform non-clausal simplification
+        PreprocessingPassResult res =
+            d_passes["non-clausal-simp"]->apply(&assertions);
+        if (res == PreprocessingPassResult::CONFLICT)
+        {
+          return false;
+        }
+      }
+
+      // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
+      // do the miplib trick.
+      if (  // check that option is on
+          options::arithMLTrick() &&
+          // only useful in arith
+          d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
+          // we add new assertions and need this (in practice, this
+          // restriction only disables miplib processing during
+          // re-simplification, which we don't expect to be useful anyway)
+          assertions.getRealAssertionsEnd() == assertions.size())
+      {
+        d_passes["miplib-trick"]->apply(&assertions);
+      }
+      else
+      {
+        Trace("simplify") << "SmtEnginePrivate::simplify(): "
+                          << "skipping miplib pseudobooleans pass..." << endl;
+      }
+    }
+
+    Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+    // before ppRewrite check if only core theory for BV theory
+    d_smt.d_theoryEngine->staticInitializeBVOptions(assertions.ref());
+
+    // Theory preprocessing
+    bool doEarlyTheoryPp = !options::arithRewriteEq();
+    if (doEarlyTheoryPp)
+    {
+      d_passes["theory-preprocess"]->apply(&assertions);
+    }
+
+    // ITE simplification
+    if (options::doITESimp()
+        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
+    {
+      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
+      if (res == PreprocessingPassResult::CONFLICT)
+      {
+        Chat() << "...ITE simplification found unsat..." << endl;
+        return false;
+      }
+    }
+
+    Debug("smt") << " assertions     : " << assertions.size() << endl;
+
+    // Unconstrained simplification
+    if (options::unconstrainedSimp())
+    {
+      d_passes["unconstrained-simplifier"]->apply(&assertions);
+    }
+
+    if (options::repeatSimp()
+        && options::simplificationMode() != options::SimplificationMode::NONE
+        && !options::unsatCores() && !options::fewerPreprocessingHoles())
+    {
+      PreprocessingPassResult res =
+          d_passes["non-clausal-simp"]->apply(&assertions);
+      if (res == PreprocessingPassResult::CONFLICT)
+      {
+        return false;
+      }
+    }
+
+    dumpAssertions("post-repeatsimp", assertions);
+    Trace("smt") << "POST repeatSimp" << endl;
+    Debug("smt") << " assertions     : " << assertions.size() << endl;
+  }
+  catch (TypeCheckingExceptionPrivate& tcep)
+  {
+    // Calls to this function should have already weeded out any
+    // typechecking exceptions via (e.g.) ensureBoolean().  But a
+    // theory could still create a new expression that isn't
+    // well-typed, and we don't want the C++ runtime to abort our
+    // process without any error notice.
+    InternalError()
+        << "A bad expression was produced.  Original exception follows:\n"
+        << tcep;
+  }
+  return true;
+}
+
+void ProcessAssertions::dumpAssertions(const char* key,
+                                       const AssertionPipeline& assertionList)
+{
+  if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
+  {
+    // Push the simplified assertions to the dump output stream
+    for (unsigned i = 0; i < assertionList.size(); ++i)
+    {
+      TNode n = assertionList[i];
+      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+    }
+  }
+}
+
+Node ProcessAssertions::expandDefinitions(
+    TNode n,
+    unordered_map<Node, Node, NodeHashFunction>& cache,
+    bool expandOnly)
+{
+  NodeManager* nm = d_smt.d_nodeManager;
+  std::stack<std::tuple<Node, Node, bool>> worklist;
+  std::stack<Node> result;
+  worklist.push(std::make_tuple(Node(n), Node(n), false));
+  // The worklist is made of triples, each is input / original node then the
+  // output / rewritten node and finally a flag tracking whether the children
+  // have been explored (i.e. if this is a downward or upward pass).
+
+  do
+  {
+    spendResource(ResourceManager::Resource::PreprocessStep);
+
+    // n is the input / original
+    // node is the output / result
+    Node node;
+    bool childrenPushed;
+    std::tie(n, node, childrenPushed) = worklist.top();
+    worklist.pop();
+
+    // Working downwards
+    if (!childrenPushed)
+    {
+      Kind k = n.getKind();
+
+      // we can short circuit (variable) leaves
+      if (n.isVar())
+      {
+        SmtEngine::DefinedFunctionMap::const_iterator i =
+            d_smt.d_definedFunctions->find(n);
+        if (i != d_smt.d_definedFunctions->end())
+        {
+          Node f = (*i).second.getFormula();
+          // must expand its definition
+          Node fe = expandDefinitions(f, cache, expandOnly);
+          // replacement must be closed
+          if ((*i).second.getFormals().size() > 0)
+          {
+            result.push(
+                nm->mkNode(LAMBDA,
+                           nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
+                           fe));
+            continue;
+          }
+          // don't bother putting in the cache
+          result.push(fe);
+          continue;
+        }
+        // don't bother putting in the cache
+        result.push(n);
+        continue;
+      }
+
+      // maybe it's in the cache
+      unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
+          cache.find(n);
+      if (cacheHit != cache.end())
+      {
+        TNode ret = (*cacheHit).second;
+        result.push(ret.isNull() ? n : ret);
+        continue;
+      }
+
+      // otherwise expand it
+      bool doExpand = false;
+      if (k == APPLY_UF)
+      {
+        // Always do beta-reduction here. The reason is that there may be
+        // operators such as INTS_MODULUS in the body of the lambda that would
+        // otherwise be introduced by beta-reduction via the rewriter, but are
+        // not expanded here since the traversal in this function does not
+        // traverse the operators of nodes. Hence, we beta-reduce here to
+        // ensure terms in the body of the lambda are expanded during this
+        // call.
+        if (n.getOperator().getKind() == LAMBDA)
+        {
+          doExpand = true;
+        }
+        else
+        {
+          // We always check if this operator corresponds to a defined function.
+          doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
+        }
+      }
+      if (doExpand)
+      {
+        vector<Node> formals;
+        TNode fm;
+        if (n.getOperator().getKind() == LAMBDA)
+        {
+          TNode op = n.getOperator();
+          // lambda
+          for (unsigned i = 0; i < op[0].getNumChildren(); i++)
+          {
+            formals.push_back(op[0][i]);
+          }
+          fm = op[1];
+        }
+        else
+        {
+          // application of a user-defined symbol
+          TNode func = n.getOperator();
+          SmtEngine::DefinedFunctionMap::const_iterator i =
+              d_smt.d_definedFunctions->find(func);
+          if (i == d_smt.d_definedFunctions->end())
+          {
+            throw TypeCheckingException(
+                n.toExpr(),
+                string("Undefined function: `") + func.toString() + "'");
+          }
+          DefinedFunction def = (*i).second;
+          formals = def.getFormals();
+
+          if (Debug.isOn("expand"))
+          {
+            Debug("expand") << "found: " << n << endl;
+            Debug("expand") << " func: " << func << endl;
+            string name = func.getAttribute(expr::VarNameAttr());
+            Debug("expand") << "     : \"" << name << "\"" << endl;
+          }
+          if (Debug.isOn("expand"))
+          {
+            Debug("expand") << " defn: " << def.getFunction() << endl
+                            << "       [";
+            if (formals.size() > 0)
+            {
+              copy(formals.begin(),
+                   formals.end() - 1,
+                   ostream_iterator<Node>(Debug("expand"), ", "));
+              Debug("expand") << formals.back();
+            }
+            Debug("expand") << "]" << endl
+                            << "       " << def.getFunction().getType() << endl
+                            << "       " << def.getFormula() << endl;
+          }
+
+          fm = def.getFormula();
+        }
+
+        Node instance = fm.substitute(formals.begin(),
+                                      formals.end(),
+                                      n.begin(),
+                                      n.begin() + formals.size());
+        Debug("expand") << "made : " << instance << endl;
+
+        Node expanded = expandDefinitions(instance, cache, expandOnly);
+        cache[n] = (n == expanded ? Node::null() : expanded);
+        result.push(expanded);
+        continue;
+      }
+      else if (!expandOnly)
+      {
+        // do not do any theory stuff if expandOnly is true
+
+        theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
+
+        Assert(t != NULL);
+        node = t->expandDefinition(n);
+      }
+
+      // the partial functions can fall through, in which case we still
+      // consider their children
+      worklist.push(std::make_tuple(
+          Node(n), node, true));  // Original and rewritten result
+
+      for (size_t i = 0; i < node.getNumChildren(); ++i)
+      {
+        worklist.push(
+            std::make_tuple(node[i],
+                            node[i],
+                            false));  // Rewrite the children of the result only
+      }
+    }
+    else
+    {
+      // Working upwards
+      // Reconstruct the node from it's (now rewritten) children on the stack
+
+      Debug("expand") << "cons : " << node << endl;
+      if (node.getNumChildren() > 0)
+      {
+        // cout << "cons : " << node << endl;
+        NodeBuilder<> nb(node.getKind());
+        if (node.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          Debug("expand") << "op   : " << node.getOperator() << endl;
+          // cout << "op   : " << node.getOperator() << endl;
+          nb << node.getOperator();
+        }
+        for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i)
+        {
+          Assert(!result.empty());
+          Node expanded = result.top();
+          result.pop();
+          // cout << "exchld : " << expanded << endl;
+          Debug("expand") << "exchld : " << expanded << endl;
+          nb << expanded;
+        }
+        node = nb;
+      }
+      // Only cache once all subterms are expanded
+      cache[n] = n == node ? Node::null() : node;
+      result.push(node);
+    }
+  } while (!worklist.empty());
+
+  AlwaysAssert(result.size() == 1);
+
+  return result.top();
+}
+
+void ProcessAssertions::collectSkolems(
+    IteSkolemMap& iskMap,
+    TNode n,
+    set<TNode>& skolemSet,
+    unordered_map<Node, bool, NodeHashFunction>& cache)
+{
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
+  it = cache.find(n);
+  if (it != cache.end())
+  {
+    return;
+  }
+
+  size_t sz = n.getNumChildren();
+  if (sz == 0)
+  {
+    if (iskMap.find(n) != iskMap.end())
+    {
+      skolemSet.insert(n);
+    }
+    cache[n] = true;
+    return;
+  }
+
+  size_t k = 0;
+  for (; k < sz; ++k)
+  {
+    collectSkolems(iskMap, n[k], skolemSet, cache);
+  }
+  cache[n] = true;
+}
+
+bool ProcessAssertions::checkForBadSkolems(
+    IteSkolemMap& iskMap,
+    TNode n,
+    TNode skolem,
+    unordered_map<Node, bool, NodeHashFunction>& cache)
+{
+  unordered_map<Node, bool, NodeHashFunction>::iterator it;
+  it = cache.find(n);
+  if (it != cache.end())
+  {
+    return (*it).second;
+  }
+
+  size_t sz = n.getNumChildren();
+  if (sz == 0)
+  {
+    IteSkolemMap::iterator iit = iskMap.find(n);
+    bool bad = false;
+    if (iit != iskMap.end())
+    {
+      if (!((*iit).first < n))
+      {
+        bad = true;
+      }
+    }
+    cache[n] = bad;
+    return bad;
+  }
+
+  size_t k = 0;
+  for (; k < sz; ++k)
+  {
+    if (checkForBadSkolems(iskMap, n[k], skolem, cache))
+    {
+      cache[n] = true;
+      return true;
+    }
+  }
+
+  cache[n] = false;
+  return false;
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
new file mode 100644
index 000000000..ddf5a6cba
--- /dev/null
+++ b/src/smt/process_assertions.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file process_assertions.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 module for processing assertions for an SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
+#define CVC4__SMT__PROCESS_ASSERTIONS_H
+
+#include <map>
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/smt_engine_stats.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * Module in charge of processing assertions for an SMT engine.
+ *
+ * Its main features are:
+ * (1) apply(AssertionsPipeline&), which updates the assertions based on our
+ * preprocessing steps,
+ * (2) expandDefinitions(TNode, ...), which returns the expanded formula of a
+ * term.
+ * The method finishInit(...) must be called before these methods are called.
+ *
+ * It is designed to be agnostic to whether we are in incremental mode. That is,
+ * it processes assertions in a way that assumes that apply(...) could be
+ * applied multiple times to different sets of assertions.
+ */
+class ProcessAssertions
+{
+  /** The types for the recursive function definitions */
+  typedef context::CDList<Node> NodeList;
+  typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+
+ public:
+  ProcessAssertions(SmtEngine& smt, ResourceManager& rm);
+  ~ProcessAssertions();
+  /** Finish initialize
+   *
+   * This initializes the preprocessing passes owned by this module.
+   */
+  void finishInit(preprocessing::PreprocessingPassContext* pc);
+  /** Cleanup
+   *
+   * This deletes the processing passes owned by this module.
+   */
+  void cleanup();
+  /**
+   * Process the formulas in assertions. Returns true if there
+   * was no conflict when processing the assertions.
+   */
+  bool apply(preprocessing::AssertionPipeline& assertions);
+  /**
+   * 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.
+   */
+  Node expandDefinitions(TNode n,
+                         NodeToNodeHashMap& cache,
+                         bool expandOnly = false);
+
+ private:
+  /** Reference to the SMT engine */
+  SmtEngine& d_smt;
+  /** Reference to resource manager */
+  ResourceManager& d_resourceManager;
+  /** The preprocess context */
+  preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
+  /** True node */
+  Node d_true;
+  /**
+   * Map of preprocessing pass instances, mapping from names to preprocessing
+   * pass instance
+   */
+  std::unordered_map<std::string,
+                     std::unique_ptr<preprocessing::PreprocessingPass>>
+      d_passes;
+  /**
+   * Number of calls of simplify assertions active.
+   */
+  unsigned d_simplifyAssertionsDepth;
+  /** recursive function definition abstractions for fmf-fun */
+  std::map<Node, TypeNode> d_fmfRecFunctionsAbs;
+  /** map to concrete definitions for fmf-fun */
+  std::map<Node, std::vector<Node>> d_fmfRecFunctionsConcrete;
+  /** List of defined recursive functions processed by fmf-fun */
+  NodeList* d_fmfRecFunctionsDefined;
+  /** Spend resource r by the resource manager of this class. */
+  void spendResource(ResourceManager::Resource r);
+  /**
+   * Perform non-clausal simplification of a Node.  This involves
+   * Theory implementations, but does NOT involve the SAT solver in
+   * any way.
+   *
+   * Returns false if the formula simplifies to "false"
+   */
+  bool simplifyAssertions(preprocessing::AssertionPipeline& assertions);
+  /**
+   * Dump assertions. Print the current assertion list to the dump
+   * assertions:`key` if it is enabled.
+   */
+  void dumpAssertions(const char* key,
+                      const preprocessing::AssertionPipeline& assertionList);
+  /**
+   * Helper function to fix up assertion list to restore invariants needed after
+   * ite removal.
+   */
+  void collectSkolems(IteSkolemMap& iskMap,
+                      TNode n,
+                      set<TNode>& skolemSet,
+                      NodeToBoolHashMap& cache);
+  /**
+   * Helper function to fix up assertion list to restore invariants needed after
+   * ite removal.
+   */
+  bool checkForBadSkolems(IteSkolemMap& iskMap,
+                          TNode n,
+                          TNode skolem,
+                          NodeToBoolHashMap& cache);
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d1eed0748..a0f1b2715 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -140,6 +140,29 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
 
   if (options::solveBVAsInt() > 0)
   {
+    // not compatible with incremental
+    if (options::incrementalSolving())
+    {
+      throw OptionException(
+          "solving bitvectors as integers is currently not supported "
+          "when solving incrementally.");
+    }
+    else if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    {
+      throw OptionException(
+          "solving bitvectors as integers is incompatible with --bool-to-bv.");
+    }
+    if (options::solveBVAsInt() > 8)
+    {
+      /**
+       * The granularity sets the size of the ITE in each element
+       * of the sum that is generated for bitwise operators.
+       * The size of the ITE is 2^{2*granularity}.
+       * Since we don't want to introduce ITEs with unbounded size,
+       * we bound the granularity.
+       */
+      throw OptionException("solve-bv-as-int accepts values from 0 to 8.");
+    }
     if (logic.isTheoryEnabled(THEORY_BV))
     {
       logic = logic.getUnlockedCopy();
@@ -772,6 +795,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     options::ufssFairnessMonotone.set(false);
     options::quantEpr.set(false);
     options::globalNegate.set(false);
+    options::bvAbstraction.set(false);
+    options::arithMLTrick.set(false);
   }
   if (logic.hasCardinalityConstraints())
   {
@@ -1405,6 +1430,17 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       smte.setOption("check-models", SExpr("false"));
     }
   }
+
+  if (options::bitblastMode() == options::BitblastMode::EAGER
+      && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
+      && logic.getLogicString() != "QF_ABV")
+  {
+    throw OptionException(
+        "Eager bit-blasting does not currently support theory combination. "
+        "Note that in a QF_BV problem UF symbols can be introduced for "
+        "division. "
+        "Try --bv-div-zero-const to interpret division by zero as a constant.");
+  }
 }
 
 }  // namespace smt
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dee3365fb..240533fba 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -82,12 +82,15 @@
 #include "prop/prop_engine.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
+#include "smt/defined_function.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
+#include "smt/process_assertions.h"
 #include "smt/set_defaults.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/smt_engine_stats.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
@@ -143,122 +146,6 @@ void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
   commands.clear();
 }
 
-/** Useful for counting the number of recursive calls. */
-class ScopeCounter {
-private:
-  unsigned& d_depth;
-public:
-  ScopeCounter(unsigned& d) : d_depth(d) {
-    ++d_depth;
-  }
-  ~ScopeCounter(){
-    --d_depth;
-  }
-};
-
-/**
- * Representation of a defined function.  We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction {
-  Node d_func;
-  vector<Node> d_formals;
-  Node d_formula;
-public:
-  DefinedFunction() {}
-  DefinedFunction(Node func, vector<Node>& formals, Node formula)
-      : d_func(func), d_formals(formals), d_formula(formula)
-  {
-  }
-  Node getFunction() const { return d_func; }
-  vector<Node> getFormals() const { return d_formals; }
-  Node getFormula() const { return d_formula; }
-};/* class DefinedFunction */
-
-struct SmtEngineStatistics {
-  /** time spent in definition-expansion */
-  TimerStat d_definitionExpansionTime;
-  /** number of constant propagations found during nonclausal simp */
-  IntStat d_numConstantProps;
-  /** time spent converting to CNF */
-  TimerStat d_cnfConversionTime;
-  /** Num of assertions before ite removal */
-  IntStat d_numAssertionsPre;
-  /** Num of assertions after ite removal */
-  IntStat d_numAssertionsPost;
-  /** Size of all proofs generated */
-  IntStat d_proofsSize;
-  /** time spent in checkModel() */
-  TimerStat d_checkModelTime;
-  /** time spent checking the proof with LFSC */
-  TimerStat d_lfscCheckProofTime;
-  /** time spent in checkUnsatCore() */
-  TimerStat d_checkUnsatCoreTime;
-  /** time spent in PropEngine::checkSat() */
-  TimerStat d_solveTime;
-  /** time spent in pushing/popping */
-  TimerStat d_pushPopTime;
-  /** time spent in processAssertions() */
-  TimerStat d_processAssertionsTime;
-
-  /** Has something simplified to false? */
-  IntStat d_simplifiedToFalse;
-  /** Number of resource units spent. */
-  ReferenceStat<uint64_t> d_resourceUnitsUsed;
-
-  SmtEngineStatistics()
-      : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
-        d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
-        d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
-        d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
-        d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
-        d_proofsSize("smt::SmtEngine::proofsSize", 0),
-        d_checkModelTime("smt::SmtEngine::checkModelTime"),
-        d_lfscCheckProofTime("smt::SmtEngine::lfscCheckProofTime"),
-        d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
-        d_solveTime("smt::SmtEngine::solveTime"),
-        d_pushPopTime("smt::SmtEngine::pushPopTime"),
-        d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
-        d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
-        d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
-  {
-    smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
-    smtStatisticsRegistry()->registerStat(&d_numConstantProps);
-    smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
-    smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
-    smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
-    smtStatisticsRegistry()->registerStat(&d_proofsSize);
-    smtStatisticsRegistry()->registerStat(&d_checkModelTime);
-    smtStatisticsRegistry()->registerStat(&d_lfscCheckProofTime);
-    smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
-    smtStatisticsRegistry()->registerStat(&d_solveTime);
-    smtStatisticsRegistry()->registerStat(&d_pushPopTime);
-    smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
-    smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
-    smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
-  }
-
-  ~SmtEngineStatistics() {
-    smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
-    smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
-    smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
-    smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
-    smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
-    smtStatisticsRegistry()->unregisterStat(&d_proofsSize);
-    smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
-    smtStatisticsRegistry()->unregisterStat(&d_lfscCheckProofTime);
-    smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
-    smtStatisticsRegistry()->unregisterStat(&d_solveTime);
-    smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
-    smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
-    smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
-    smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
-  }
-};/* struct SmtEngineStatistics */
-
-
 class SoftResourceOutListener : public Listener {
  public:
   SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
@@ -442,13 +329,15 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   NodeToNodeHashMap d_abstractValues;
 
-  /** Number of calls of simplify assertions active.
-   */
-  unsigned d_simplifyAssertionsDepth;
-
   /** TODO: whether certain preprocess steps are necessary */
   //bool d_needsExpandDefs;
 
+  /** The preprocessing pass context */
+  std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
+
+  /** Process assertions module */
+  ProcessAssertions d_processor;
+
   //------------------------------- expression names
   /** mapping from expressions to name */
   context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
@@ -480,39 +369,10 @@ class SmtEnginePrivate : public NodeManagerListener {
   CDO<bool> d_sygusConjectureStale;
   /*------------------- end of sygus utils ------------------*/
 
- private:
-  std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
-
-  /**
-   * Map of preprocessing pass instances, mapping from names to preprocessing
-   * pass instance
-   */
-  std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>> d_passes;
-
-  /**
-   * Helper function to fix up assertion list to restore invariants needed after
-   * ite removal.
-   */
-  void collectSkolems(TNode n, set<TNode>& skolemSet, NodeToBoolHashMap& cache);
-
-  /**
-   * Helper function to fix up assertion list to restore invariants needed after
-   * ite removal.
-   */
-  bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
-
-  /**
-   * Perform non-clausal simplification of a Node.  This involves
-   * Theory implementations, but does NOT involve the SAT solver in
-   * any way.
-   *
-   * Returns false if the formula simplifies to "false"
-   */
-  bool simplifyAssertions();
-
  public:
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
+        d_resourceManager(NodeManager::currentResourceManager()),
         d_managedRegularChannel(),
         d_managedDiagnosticChannel(),
         d_managedDumpChannel(),
@@ -523,7 +383,7 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_fakeContext(),
         d_abstractValueMap(&d_fakeContext),
         d_abstractValues(),
-        d_simplifyAssertionsDepth(0),
+        d_processor(smt, *d_resourceManager),
         // d_needsExpandDefs(true),  //TODO?
         d_exprNames(smt.getUserContext()),
         d_iteRemover(smt.getUserContext()),
@@ -531,7 +391,6 @@ class SmtEnginePrivate : public NodeManagerListener {
   {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
-    d_resourceManager = NodeManager::currentResourceManager();
 
     d_listenerRegistrations->add(d_resourceManager->registerSoftListener(
         new SoftResourceOutListener(d_smt)));
@@ -607,8 +466,6 @@ class SmtEnginePrivate : public NodeManagerListener {
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
-  void cleanupPreprocessingPasses() { d_passes.clear(); }
-
   ResourceManager* getResourceManager() { return d_resourceManager; }
 
   void spendResource(ResourceManager::Resource r)
@@ -616,6 +473,8 @@ class SmtEnginePrivate : public NodeManagerListener {
     d_resourceManager->spendResource(r);
   }
 
+  ProcessAssertions* getProcessAssertions() { return &d_processor; }
+
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
   {
     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
@@ -724,12 +583,6 @@ class SmtEnginePrivate : public NodeManagerListener {
                   bool inInput = true,
                   bool isAssumption = false,
                   bool maybeHasFv = false);
-
-  /** Expand definitions in n. */
-  Node expandDefinitions(TNode n,
-                         NodeToNodeHashMap& cache,
-                         bool expandOnly = false);
-
   /**
    * Simplify node "in" by expanding definitions and applying any
    * substitutions learned from preprocessing.
@@ -738,7 +591,7 @@ class SmtEnginePrivate : public NodeManagerListener {
     // Substitute out any abstract values in ex.
     // Expand definitions.
     NodeToNodeHashMap cache;
-    Node n = expandDefinitions(in, cache).toExpr();
+    Node n = d_processor.expandDefinitions(in, cache).toExpr();
     // Make sure we've done all preprocessing, etc.
     Assert(d_assertions.size() == 0);
     return applySubstitutions(n).toExpr();
@@ -804,7 +657,6 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_proofManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
-      d_fmfRecFunctionsDefined(nullptr),
       d_assertionList(nullptr),
       d_assignments(nullptr),
       d_modelGlobalCommands(),
@@ -847,7 +699,6 @@ SmtEngine::SmtEngine(ExprManager* em)
 #endif
 
   d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
-  d_fmfRecFunctionsDefined = new (true) NodeList(getUserContext());
   d_modelCommands = new (true) smt::CommandList(getUserContext());
 }
 
@@ -1011,10 +862,9 @@ SmtEngine::~SmtEngine()
     }
 
     d_definedFunctions->deleteSelf();
-    d_fmfRecFunctionsDefined->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
-    d_private->cleanupPreprocessingPasses();
+    d_private->getProcessAssertions()->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
@@ -1437,319 +1287,11 @@ bool SmtEngine::isDefinedFunction( Expr func ){
 
 void SmtEnginePrivate::finishInit()
 {
-  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
   d_preprocessingPassContext.reset(new PreprocessingPassContext(
       &d_smt, d_resourceManager, &d_iteRemover, &d_propagator));
 
-  // TODO: this will likely change when we add support for actually assembling
-  // preprocessing pipelines. For now, we just create an instance of each
-  // available preprocessing pass.
-  std::vector<std::string> passNames = ppReg.getAvailablePasses();
-  for (const std::string& passName : passNames)
-  {
-    d_passes[passName].reset(
-        ppReg.createPass(d_preprocessingPassContext.get(), passName));
-  }
-}
-
-Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
-{
-  stack<std::tuple<Node, Node, bool>> worklist;
-  stack<Node> result;
-  worklist.push(std::make_tuple(Node(n), Node(n), false));
-  // The worklist is made of triples, each is input / original node then the output / rewritten node
-  // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
-  // or upward pass).
-
-  do {
-    spendResource(ResourceManager::Resource::PreprocessStep);
-
-    // n is the input / original
-    // node is the output / result
-    Node node;
-    bool childrenPushed;
-    std::tie(n, node, childrenPushed) = worklist.top();
-    worklist.pop();
-
-    // Working downwards
-    if(!childrenPushed) {
-      Kind k = n.getKind();
-
-      // we can short circuit (variable) leaves
-      if(n.isVar()) {
-        SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
-        if(i != d_smt.d_definedFunctions->end()) {
-          Node f = (*i).second.getFormula();
-          // must expand its definition
-          Node fe = expandDefinitions(f, cache, expandOnly);
-          // replacement must be closed
-          if((*i).second.getFormals().size() > 0) {
-            result.push(d_smt.d_nodeManager->mkNode(
-                kind::LAMBDA,
-                d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
-                                            (*i).second.getFormals()),
-                fe));
-            continue;
-          }
-          // don't bother putting in the cache
-          result.push(fe);
-          continue;
-        }
-        // don't bother putting in the cache
-        result.push(n);
-        continue;
-      }
-
-      // maybe it's in the cache
-      unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
-      if(cacheHit != cache.end()) {
-        TNode ret = (*cacheHit).second;
-        result.push(ret.isNull() ? n : ret);
-        continue;
-      }
-
-      // otherwise expand it
-      bool doExpand = false;
-      if (k == kind::APPLY_UF)
-      {
-        // Always do beta-reduction here. The reason is that there may be
-        // operators such as INTS_MODULUS in the body of the lambda that would
-        // otherwise be introduced by beta-reduction via the rewriter, but are
-        // not expanded here since the traversal in this function does not
-        // traverse the operators of nodes. Hence, we beta-reduce here to
-        // ensure terms in the body of the lambda are expanded during this
-        // call.
-        if (n.getOperator().getKind() == kind::LAMBDA)
-        {
-          doExpand = true;
-        }
-        else
-        {
-          // We always check if this operator corresponds to a defined function.
-          doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
-        }
-      }
-      if (doExpand) {
-        vector<Node> formals;
-        TNode fm;
-        if( n.getOperator().getKind() == kind::LAMBDA ){
-          TNode op = n.getOperator();
-          // lambda
-          for( unsigned i=0; i<op[0].getNumChildren(); i++ ){
-            formals.push_back( op[0][i] );
-          }
-          fm = op[1];
-        }else{
-          // application of a user-defined symbol
-          TNode func = n.getOperator();
-          SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
-          if(i == d_smt.d_definedFunctions->end()) {
-            throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
-          }
-          DefinedFunction def = (*i).second;
-          formals = def.getFormals();
-
-          if(Debug.isOn("expand")) {
-            Debug("expand") << "found: " << n << endl;
-            Debug("expand") << " func: " << func << endl;
-            string name = func.getAttribute(expr::VarNameAttr());
-            Debug("expand") << "     : \"" << name << "\"" << endl;
-          }
-          if(Debug.isOn("expand")) {
-            Debug("expand") << " defn: " << def.getFunction() << endl
-                            << "       [";
-            if(formals.size() > 0) {
-              copy( formals.begin(), formals.end() - 1,
-                    ostream_iterator<Node>(Debug("expand"), ", ") );
-              Debug("expand") << formals.back();
-            }
-            Debug("expand") << "]" << endl
-                            << "       " << def.getFunction().getType() << endl
-                            << "       " << def.getFormula() << endl;
-          }
-
-          fm = def.getFormula();
-        }
-
-        Node instance = fm.substitute(formals.begin(),
-                                      formals.end(),
-                                      n.begin(),
-                                      n.begin() + formals.size());
-        Debug("expand") << "made : " << instance << endl;
-
-        Node expanded = expandDefinitions(instance, cache, expandOnly);
-        cache[n] = (n == expanded ? Node::null() : expanded);
-        result.push(expanded);
-        continue;
-
-      } else if(! expandOnly) {
-        // do not do any theory stuff if expandOnly is true
-
-        theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
-
-        Assert(t != NULL);
-        node = t->expandDefinition(n);
-      }
-
-      // the partial functions can fall through, in which case we still
-      // consider their children
-      worklist.push(std::make_tuple(
-          Node(n), node, true));  // Original and rewritten result
-
-      for(size_t i = 0; i < node.getNumChildren(); ++i) {
-        worklist.push(
-            std::make_tuple(node[i],
-                            node[i],
-                            false));  // Rewrite the children of the result only
-      }
-
-    } else {
-      // Working upwards
-      // Reconstruct the node from it's (now rewritten) children on the stack
-
-      Debug("expand") << "cons : " << node << endl;
-      if(node.getNumChildren()>0) {
-        //cout << "cons : " << node << endl;
-        NodeBuilder<> nb(node.getKind());
-        if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-          Debug("expand") << "op   : " << node.getOperator() << endl;
-          //cout << "op   : " << node.getOperator() << endl;
-          nb << node.getOperator();
-        }
-        for(size_t i = 0; i < node.getNumChildren(); ++i) {
-          Assert(!result.empty());
-          Node expanded = result.top();
-          result.pop();
-          //cout << "exchld : " << expanded << endl;
-          Debug("expand") << "exchld : " << expanded << endl;
-          nb << expanded;
-        }
-        node = nb;
-      }
-      cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
-      result.push(node);
-    }
-  } while(!worklist.empty());
-
-  AlwaysAssert(result.size() == 1);
-
-  return result.top();
-}
-
-// do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key,
-                           const AssertionPipeline& assertionList) {
-  if( Dump.isOn("assertions") &&
-      Dump.isOn(string("assertions:") + key) ) {
-    // Push the simplified assertions to the dump output stream
-    for(unsigned i = 0; i < assertionList.size(); ++ i) {
-      TNode n = assertionList[i];
-      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
-    }
-  }
-}
-
-// returns false if simplification led to "false"
-bool SmtEnginePrivate::simplifyAssertions()
-{
-  spendResource(ResourceManager::Resource::PreprocessStep);
-  Assert(d_smt.d_pendingPops == 0);
-  try {
-    ScopeCounter depth(d_simplifyAssertionsDepth);
-
-    Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
-
-    if (options::simplificationMode() != options::SimplificationMode::NONE)
-    {
-      if (!options::unsatCores() && !options::fewerPreprocessingHoles())
-      {
-        // Perform non-clausal simplification
-        PreprocessingPassResult res =
-            d_passes["non-clausal-simp"]->apply(&d_assertions);
-        if (res == PreprocessingPassResult::CONFLICT)
-        {
-          return false;
-        }
-      }
-
-      // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
-      // do the miplib trick.
-      if (  // check that option is on
-          options::arithMLTrick() &&
-          // miplib rewrites aren't safe in incremental mode
-          !options::incrementalSolving() &&
-          // only useful in arith
-          d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
-          // we add new assertions and need this (in practice, this
-          // restriction only disables miplib processing during
-          // re-simplification, which we don't expect to be useful anyway)
-          d_assertions.getRealAssertionsEnd() == d_assertions.size())
-      {
-        d_passes["miplib-trick"]->apply(&d_assertions);
-      } else {
-        Trace("simplify") << "SmtEnginePrivate::simplify(): "
-                          << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
-      }
-    }
-
-    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-    // before ppRewrite check if only core theory for BV theory
-    d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
-
-    // Theory preprocessing
-    bool doEarlyTheoryPp = !options::arithRewriteEq();
-    if (doEarlyTheoryPp)
-    {
-      d_passes["theory-preprocess"]->apply(&d_assertions);
-    }
-
-    // ITE simplification
-    if (options::doITESimp()
-        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
-    {
-      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&d_assertions);
-      if (res == PreprocessingPassResult::CONFLICT)
-      {
-        Chat() << "...ITE simplification found unsat..." << endl;
-        return false;
-      }
-    }
-
-    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-    // Unconstrained simplification
-    if(options::unconstrainedSimp()) {
-      d_passes["unconstrained-simplifier"]->apply(&d_assertions);
-    }
-
-    if (options::repeatSimp()
-        && options::simplificationMode() != options::SimplificationMode::NONE
-        && !options::unsatCores() && !options::fewerPreprocessingHoles())
-    {
-      PreprocessingPassResult res =
-          d_passes["non-clausal-simp"]->apply(&d_assertions);
-      if (res == PreprocessingPassResult::CONFLICT)
-      {
-        return false;
-      }
-    }
-
-    dumpAssertions("post-repeatsimp", d_assertions);
-    Trace("smt") << "POST repeatSimp" << endl;
-    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  } catch(TypeCheckingExceptionPrivate& tcep) {
-    // Calls to this function should have already weeded out any
-    // typechecking exceptions via (e.g.) ensureBoolean().  But a
-    // theory could still create a new expression that isn't
-    // well-typed, and we don't want the C++ runtime to abort our
-    // process without any error notice.
-    InternalError()
-        << "A bad expression was produced.  Original exception follows:\n"
-        << tcep;
-  }
-  return true;
+  // initialize the preprocessing passes
+  d_processor.finishInit(d_preprocessingPassContext.get());
 }
 
 Result SmtEngine::check() {
@@ -1835,93 +1377,16 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   return m;
 }
 
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
-{
-  unordered_map<Node, bool, NodeHashFunction>::iterator it;
-  it = cache.find(n);
-  if (it != cache.end()) {
-    return;
-  }
-
-  size_t sz = n.getNumChildren();
-  if (sz == 0) {
-    if (getIteSkolemMap().find(n) != getIteSkolemMap().end())
-    {
-      skolemSet.insert(n);
-    }
-    cache[n] = true;
-    return;
-  }
-
-  size_t k = 0;
-  for (; k < sz; ++k) {
-    collectSkolems(n[k], skolemSet, cache);
-  }
-  cache[n] = true;
-}
-
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
-{
-  unordered_map<Node, bool, NodeHashFunction>::iterator it;
-  it = cache.find(n);
-  if (it != cache.end()) {
-    return (*it).second;
-  }
-
-  size_t sz = n.getNumChildren();
-  if (sz == 0) {
-    IteSkolemMap::iterator iit = getIteSkolemMap().find(n);
-    bool bad = false;
-    if (iit != getIteSkolemMap().end())
-    {
-      if (!((*iit).first < n))
-      {
-        bad = true;
-      }
-    }
-    cache[n] = bad;
-    return bad;
-  }
-
-  size_t k = 0;
-  for (; k < sz; ++k) {
-    if (checkForBadSkolems(n[k], skolem, cache)) {
-      cache[n] = true;
-      return true;
-    }
-  }
-
-  cache[n] = false;
-  return false;
-}
-
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
   spendResource(ResourceManager::Resource::PreprocessStep);
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
-  SubstitutionMap& top_level_substs =
-      d_preprocessingPassContext->getTopLevelSubstitutions();
-
-  // Dump the assertions
-  dumpAssertions("pre-everything", d_assertions);
-
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
-  Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
-
-  Debug("smt") << "#Assertions : " << d_assertions.size() << endl;
-  Debug("smt") << "#Assumptions: " << d_assertions.getNumAssumptions() << endl;
 
   if (d_assertions.size() == 0) {
     // nothing to do
     return;
   }
-
-  if (options::bvGaussElim())
-  {
-    d_passes["bv-gauss"]->apply(&d_assertions);
-  }
-
   if (d_assertionsProcessed && options::incrementalSolving()) {
     // TODO(b/1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
@@ -1933,334 +1398,8 @@ void SmtEnginePrivate::processAssertions() {
     d_assertions.disableStoreSubstsInAsserts();
   }
 
-  // Add dummy assertion in last position - to be used as a
-  // placeholder for any new assertions to get added
-  d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
-  // any assertions added beyond realAssertionsEnd must NOT affect the
-  // equisatisfiability
-  d_assertions.updateRealAssertionsEnd();
-
-  // Assertions are NOT guaranteed to be rewritten by this point
-
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
-  dumpAssertions("pre-definition-expansion", d_assertions);
-  {
-    Chat() << "expanding definitions..." << endl;
-    Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
-    unordered_map<Node, Node, NodeHashFunction> cache;
-    for(unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
-    }
-  }
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
-  dumpAssertions("post-definition-expansion", d_assertions);
-
-  // save the assertions now
-  THEORY_PROOF
-    (
-     for (unsigned i = 0; i < d_assertions.size(); ++i) {
-       ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
-     }
-     );
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  if (options::globalNegate())
-  {
-    // global negation of the formula
-    d_passes["global-negate"]->apply(&d_assertions);
-    d_smt.d_globalNegation = !d_smt.d_globalNegation;
-  }
-
-  if( options::nlExtPurify() ){
-    d_passes["nl-ext-purify"]->apply(&d_assertions);
-  }
-
-  if (options::solveRealAsInt()) {
-    d_passes["real-to-int"]->apply(&d_assertions);
-  }
-  
-  if (options::solveIntAsBV() > 0)
-  {
-    d_passes["int-to-bv"]->apply(&d_assertions);
-  }
-
-  if (options::bitblastMode() == options::BitblastMode::EAGER
-      && !d_smt.d_logic.isPure(THEORY_BV)
-      && d_smt.d_logic.getLogicString() != "QF_UFBV"
-      && d_smt.d_logic.getLogicString() != "QF_ABV")
-  {
-    throw ModalException("Eager bit-blasting does not currently support theory combination. "
-                         "Note that in a QF_BV problem UF symbols can be introduced for division. "
-                         "Try --bv-div-zero-const to interpret division by zero as a constant.");
-  }
-
-  if (options::ackermann())
-  {
-    d_passes["ackermann"]->apply(&d_assertions);
-  }
-
-  if (options::bvAbstraction() && !options::incrementalSolving())
-  {
-    d_passes["bv-abstraction"]->apply(&d_assertions);
-  }
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  bool noConflict = true;
-
-  if (options::extRewPrep())
-  {
-    d_passes["ext-rew-pre"]->apply(&d_assertions);
-  }
-
-  // Unconstrained simplification
-  if(options::unconstrainedSimp()) {
-    d_passes["rewrite"]->apply(&d_assertions);
-    d_passes["unconstrained-simplifier"]->apply(&d_assertions);
-  }
-
-  if(options::bvIntroducePow2())
-  {
-    d_passes["bv-intro-pow2"]->apply(&d_assertions);
-  }
-
-  // Since this pass is not robust for the information tracking necessary for
-  // unsat cores, it's only applied if we are not doing unsat core computation
-  if (!options::unsatCores())
-  {
-    d_passes["apply-substs"]->apply(&d_assertions);
-  }
-
-  // Assertions MUST BE guaranteed to be rewritten by this point
-  d_passes["rewrite"]->apply(&d_assertions);
-
-  // Lift bit-vectors of size 1 to bool
-  if (options::bitvectorToBool())
-  {
-    d_passes["bv-to-bool"]->apply(&d_assertions);
-  }
-  if (options::solveBVAsInt() > 0)
-  {
-    if (options::incrementalSolving())
-    {
-      throw ModalException(
-          "solving bitvectors as integers is currently not supported "
-          "when solving incrementally.");
-    } else if (options::boolToBitvector() != options::BoolToBVMode::OFF) {
-      throw ModalException(
-          "solving bitvectors as integers is incompatible with --bool-to-bv.");
-    }
-    else if (options::solveBVAsInt() > 8)
-    {
-      /**
-       * The granularity sets the size of the ITE in each element
-       * of the sum that is generated for bitwise operators.
-       * The size of the ITE is 2^{2*granularity}.
-       * Since we don't want to introduce ITEs with unbounded size,
-       * we bound the granularity.
-       */
-      throw ModalException("solve-bv-as-int accepts values from 0 to 8.");
-    }
-    else
-    {
-      d_passes["bv-to-int"]->apply(&d_assertions);
-    }
-  }
-
-  // Convert non-top-level Booleans to bit-vectors of size 1
-  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
-  {
-    d_passes["bool-to-bv"]->apply(&d_assertions);
-  }
-  if(options::sepPreSkolemEmp()) {
-    d_passes["sep-skolem-emp"]->apply(&d_assertions);
-  }
-
-  if( d_smt.d_logic.isQuantified() ){
-    //remove rewrite rules, apply pre-skolemization to existential quantifiers
-    d_passes["quantifiers-preprocess"]->apply(&d_assertions);
-    if( options::macrosQuant() ){
-      //quantifiers macro expansion
-      d_passes["quantifier-macros"]->apply(&d_assertions);
-    }
-
-    //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
-    if( options::fmfFunWellDefined() ){
-      quantifiers::FunDefFmf fdf;
-      Assert(d_smt.d_fmfRecFunctionsDefined != NULL);
-      //must carry over current definitions (for incremental)
-      for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
-           fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
-        Node f = (*fit);
-        Assert(d_smt.d_fmfRecFunctionsAbs.find(f)
-               != d_smt.d_fmfRecFunctionsAbs.end());
-        TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
-        fdf.d_sorts[f] = ft;
-        std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
-        Assert(fcit != d_smt.d_fmfRecFunctionsConcrete.end());
-        for( unsigned j=0; j<fcit->second.size(); j++ ){
-          fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
-        }
-      }
-      fdf.simplify( d_assertions.ref() );
-      //must store new definitions (for incremental)
-      for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
-        Node f = fdf.d_funcs[i];
-        d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
-        d_smt.d_fmfRecFunctionsConcrete[f].clear();
-        for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
-          d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
-        }
-        d_smt.d_fmfRecFunctionsDefined->push_back( f );
-      }
-    }
-  }
-
-  if( options::sortInference() || options::ufssFairnessMonotone() ){
-    d_passes["sort-inference"]->apply(&d_assertions);
-  }
-
-  if( options::pbRewrites() ){
-    d_passes["pseudo-boolean-processor"]->apply(&d_assertions);
-  }
-
-  // rephrasing normal inputs as sygus problems
-  if (!d_smt.d_isInternalSubsolver)
-  {
-    if (options::sygusInference())
-    {
-      d_passes["sygus-infer"]->apply(&d_assertions);
-    }
-    else if (options::sygusRewSynthInput())
-    {
-      // do candidate rewrite rule synthesis
-      d_passes["synth-rr"]->apply(&d_assertions);
-    }
-  }
-
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
-  dumpAssertions("pre-simplify", d_assertions);
-  Chat() << "simplifying assertions..." << endl;
-  noConflict = simplifyAssertions();
-  if(!noConflict){
-    ++(d_smt.d_stats->d_simplifiedToFalse);
-  }
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
-  dumpAssertions("post-simplify", d_assertions);
-
-  if(options::doStaticLearning()) {
-    d_passes["static-learning"]->apply(&d_assertions);
-  }
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  {
-    d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
-    d_passes["ite-removal"]->apply(&d_assertions);
-    // This is needed because when solving incrementally, removeITEs may introduce
-    // skolems that were solved for earlier and thus appear in the substitution
-    // map.
-    d_passes["apply-substs"]->apply(&d_assertions);
-    d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
-  }
-
-  dumpAssertions("pre-repeat-simplify", d_assertions);
-  if(options::repeatSimp()) {
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
-    Chat() << "re-simplifying assertions..." << endl;
-    ScopeCounter depth(d_simplifyAssertionsDepth);
-    noConflict &= simplifyAssertions();
-    if (noConflict) {
-      // Need to fix up assertion list to maintain invariants:
-      // Let Sk be the set of Skolem variables introduced by ITE's.  Let <_sk be the order in which these variables were introduced
-      // during ite removal.
-      // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
-
-      // cache for expression traversal
-      unordered_map<Node, bool, NodeHashFunction> cache;
-
-      // First, find all skolems that appear in the substitution map - their associated iteExpr will need
-      // to be moved to the main assertion set
-      set<TNode> skolemSet;
-      SubstitutionMap::iterator pos = top_level_substs.begin();
-      for (; pos != top_level_substs.end(); ++pos)
-      {
-        collectSkolems((*pos).first, skolemSet, cache);
-        collectSkolems((*pos).second, skolemSet, cache);
-      }
-
-      // We need to ensure:
-      // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
-      // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
-      // If either of these is violated, we must add iteExpr as a proper assertion
-      IteSkolemMap::iterator it = getIteSkolemMap().begin();
-      IteSkolemMap::iterator iend = getIteSkolemMap().end();
-      NodeBuilder<> builder(kind::AND);
-      builder << d_assertions[d_assertions.getRealAssertionsEnd() - 1];
-      vector<TNode> toErase;
-      for (; it != iend; ++it) {
-        if (skolemSet.find((*it).first) == skolemSet.end()) {
-          TNode iteExpr = d_assertions[(*it).second];
-          if (iteExpr.getKind() == kind::ITE &&
-              iteExpr[1].getKind() == kind::EQUAL &&
-              iteExpr[1][0] == (*it).first &&
-              iteExpr[2].getKind() == kind::EQUAL &&
-              iteExpr[2][0] == (*it).first) {
-            cache.clear();
-            bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache);
-            bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache);
-            bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache);
-            if (!bad) {
-              continue;
-            }
-          }
-        }
-        // Move this iteExpr into the main assertions
-        builder << d_assertions[(*it).second];
-        d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
-        toErase.push_back((*it).first);
-      }
-      if(builder.getNumChildren() > 1) {
-        while (!toErase.empty()) {
-          getIteSkolemMap().erase(toErase.back());
-          toErase.pop_back();
-        }
-        d_assertions[d_assertions.getRealAssertionsEnd() - 1] =
-            Rewriter::rewrite(Node(builder));
-      }
-      // TODO(b/1256): For some reason this is needed for some benchmarks, such as
-      // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
-      d_passes["ite-removal"]->apply(&d_assertions);
-      d_passes["apply-substs"]->apply(&d_assertions);
-      //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
-    }
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
-  }
-  dumpAssertions("post-repeat-simplify", d_assertions);
-
-  if (options::ufHo())
-  {
-    d_passes["ho-elim"]->apply(&d_assertions);
-  }
-
-  // begin: INVARIANT to maintain: no reordering of assertions or
-  // introducing new ones
-#ifdef CVC4_ASSERTIONS
-  unsigned iteRewriteAssertionsEnd = d_assertions.size();
-#endif
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
-  d_passes["theory-preprocess"]->apply(&d_assertions);
-
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    d_passes["bv-eager-atoms"]->apply(&d_assertions);
-  }
+  // process the assertions
+  bool noConflict = d_processor.apply(d_assertions);
 
   //notify theory engine new preprocessed assertions
   d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
@@ -2269,16 +1408,12 @@ void SmtEnginePrivate::processAssertions() {
   if (noConflict)
   {
     Chat() << "pushing to decision engine..." << endl;
-    Assert(iteRewriteAssertionsEnd == d_assertions.size());
     d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
-  dumpAssertions("post-everything", d_assertions);
-
   // if incremental, compute which variables are assigned
   if (options::incrementalSolving())
   {
@@ -2917,7 +2052,8 @@ Expr SmtEngine::expandDefinitions(const Expr& ex)
   }
 
   unordered_map<Node, Node, NodeHashFunction> cache;
-  Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
+  Node n = d_private->getProcessAssertions()->expandDefinitions(
+      Node::fromExpr(e), cache, /* expandOnly = */ true);
   n = postprocess(n, TypeNode::fromType(e.getType()));
 
   return n.toExpr();
@@ -2949,7 +2085,7 @@ Expr SmtEngine::getValue(const Expr& ex) const
 
   // Expand, then normalize
   unordered_map<Node, Node, NodeHashFunction> cache;
-  n = d_private->expandDefinitions(n, 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
@@ -3073,7 +2209,7 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
 
       // Expand, then normalize
       unordered_map<Node, Node, NodeHashFunction> cache;
-      Node n = d_private->expandDefinitions(as, cache);
+      Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache);
       n = Rewriter::rewrite(n);
 
       Trace("smt") << "--- getting value of " << n << endl;
@@ -3239,7 +2375,7 @@ std::vector<Expr> SmtEngine::getExpandedAssertions()
   for (const Expr& e : easserts)
   {
     Node ea = Node::fromExpr(e);
-    Node eae = d_private->expandDefinitions(ea, cache);
+    Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache);
     eassertsProc.push_back(eae.toExpr());
   }
   return eassertsProc;
@@ -3481,7 +2617,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     // Apply any define-funs from the problem.
     {
       unordered_map<Node, Node, NodeHashFunction> cache;
-      n = d_private->expandDefinitions(n, cache);
+      n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
     }
     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
@@ -3635,7 +2771,8 @@ void SmtEngine::checkSynthSolution()
     Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n";
     Node assertion = Node::fromExpr(*i);
     // Apply any define-funs from the problem.
-    assertion = d_private->expandDefinitions(assertion, cache);
+    assertion =
+        d_private->getProcessAssertions()->expandDefinitions(assertion, cache);
     Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion
              << endl;
     Trace("check-synth-sol") << "Expanded assertion " << assertion << "\n";
@@ -3952,7 +3089,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   Node conjn = Node::fromExpr(conj);
   // must expand definitions
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  conjn = d_private->expandDefinitions(conjn, cache);
+  conjn = d_private->getProcessAssertions()->expandDefinitions(conjn, cache);
   // now negate
   conjn = conjn.negate();
   d_abdConj = conjn.toExpr();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3f24c8bab..672bec821 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -96,7 +96,7 @@ namespace smt {
   struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
-  class BooleanTermConverter;
+  class ProcessAssertions;
 
   ProofManager* currentProofManager();
 
@@ -130,7 +130,7 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::preprocessing::PreprocessingPassContext;
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
-  friend class ::CVC4::smt::BooleanTermConverter;
+  friend class ::CVC4::smt::ProcessAssertions;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::Model;  // to access d_modelCommands
@@ -1131,11 +1131,6 @@ class CVC4_PUBLIC SmtEngine
    */
   Expr d_abdConj;
 
-  /** recursive function definition abstractions for --fmf-fun */
-  std::map<Node, TypeNode> d_fmfRecFunctionsAbs;
-  std::map<Node, std::vector<Node> > d_fmfRecFunctionsConcrete;
-  NodeList* d_fmfRecFunctionsDefined;
-
   /**
    * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in interactive mode.
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
new file mode 100644
index 000000000..c45f77b9b
--- /dev/null
+++ b/src/smt/smt_engine_stats.cpp
@@ -0,0 +1,73 @@
+/*********************                                                        */
+/*! \file smt_engine_stats.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 Implementation of statistics for SMT engine
+ **/
+
+#include "smt/smt_engine_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace smt {
+
+SmtEngineStatistics::SmtEngineStatistics()
+    : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+      d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
+      d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
+      d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
+      d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
+      d_proofsSize("smt::SmtEngine::proofsSize", 0),
+      d_checkModelTime("smt::SmtEngine::checkModelTime"),
+      d_lfscCheckProofTime("smt::SmtEngine::lfscCheckProofTime"),
+      d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
+      d_solveTime("smt::SmtEngine::solveTime"),
+      d_pushPopTime("smt::SmtEngine::pushPopTime"),
+      d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
+      d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
+{
+  smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
+  smtStatisticsRegistry()->registerStat(&d_numConstantProps);
+  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
+  smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
+  smtStatisticsRegistry()->registerStat(&d_proofsSize);
+  smtStatisticsRegistry()->registerStat(&d_checkModelTime);
+  smtStatisticsRegistry()->registerStat(&d_lfscCheckProofTime);
+  smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
+  smtStatisticsRegistry()->registerStat(&d_solveTime);
+  smtStatisticsRegistry()->registerStat(&d_pushPopTime);
+  smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
+  smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
+  smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
+}
+
+SmtEngineStatistics::~SmtEngineStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
+  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
+  smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
+  smtStatisticsRegistry()->unregisterStat(&d_proofsSize);
+  smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
+  smtStatisticsRegistry()->unregisterStat(&d_lfscCheckProofTime);
+  smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+  smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
+  smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
+  smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
+  smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
new file mode 100644
index 000000000..cebf85d95
--- /dev/null
+++ b/src/smt/smt_engine_stats.h
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file smt_engine_stats.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 Statistics for SMT engine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__SMT_ENGINE_STATS_H
+#define CVC4__SMT__SMT_ENGINE_STATS_H
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace smt {
+
+struct SmtEngineStatistics
+{
+  SmtEngineStatistics();
+  ~SmtEngineStatistics();
+  /** time spent in definition-expansion */
+  TimerStat d_definitionExpansionTime;
+  /** number of constant propagations found during nonclausal simp */
+  IntStat d_numConstantProps;
+  /** time spent converting to CNF */
+  TimerStat d_cnfConversionTime;
+  /** Number of assertions before ite removal */
+  IntStat d_numAssertionsPre;
+  /** Number of assertions after ite removal */
+  IntStat d_numAssertionsPost;
+  /** Size of all proofs generated */
+  IntStat d_proofsSize;
+  /** time spent in checkModel() */
+  TimerStat d_checkModelTime;
+  /** time spent checking the proof with LFSC */
+  TimerStat d_lfscCheckProofTime;
+  /** time spent in checkUnsatCore() */
+  TimerStat d_checkUnsatCoreTime;
+  /** time spent in PropEngine::checkSat() */
+  TimerStat d_solveTime;
+  /** time spent in pushing/popping */
+  TimerStat d_pushPopTime;
+  /** time spent in processAssertions() */
+  TimerStat d_processAssertionsTime;
+
+  /** Has something simplified to false? */
+  IntStat d_simplifiedToFalse;
+  /** Number of resource units spent. */
+  ReferenceStat<uint64_t> d_resourceUnitsUsed;
+}; /* struct SmtEngineStatistics */
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__SMT_ENGINE_STATS_H */