Refactor how assertions are added to decision engine (#2396)

Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.

23 files changed, 258 insertions, 230 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index e2109cf1e..caad72fd5 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -61,6 +61,8 @@ libcvc4_la_SOURCES = \
 	decision/decision_strategy.h \
 	decision/justification_heuristic.cpp \
 	decision/justification_heuristic.h \
+	preprocessing/assertion_pipeline.cpp \
+	preprocessing/assertion_pipeline.h \
 	preprocessing/passes/apply_substs.cpp \
 	preprocessing/passes/apply_substs.h \
 	preprocessing/passes/apply_to_const.cpp \
@@ -97,10 +99,10 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/pseudo_boolean_processor.h \
 	preprocessing/passes/miplib_trick.cpp \
 	preprocessing/passes/miplib_trick.h \
-	preprocessing/passes/quantifiers_preprocess.cpp \
-	preprocessing/passes/quantifiers_preprocess.h \
 	preprocessing/passes/quantifier_macros.cpp \
 	preprocessing/passes/quantifier_macros.h \
+	preprocessing/passes/quantifiers_preprocess.cpp \
+	preprocessing/passes/quantifiers_preprocess.h \
 	preprocessing/passes/real_to_int.cpp \
 	preprocessing/passes/real_to_int.h \
 	preprocessing/passes/rewrite.cpp \
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 8aed4fb32..013e2165f 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -610,10 +610,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
 
 namespace {
 
-bool isDefinedKind(Kind k)
-{
-  return k > UNDEFINED_KIND && k < LAST_KIND;
-}
+bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
 
 bool isDefinedIntKind(CVC4::Kind k)
 {
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 8e419e768..01f78f2d6 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -98,31 +98,21 @@ SatValue DecisionEngine::getPolarity(SatVariable var)
   }
 }
 
-void DecisionEngine::addAssertions(const vector<Node> &assertions)
-{
-  Assert(false);  // doing this so that we revisit what to do
-                  // here. Currently not being used.
-
-  // d_result = SAT_VALUE_UNKNOWN;
-  // d_assertions.reserve(assertions.size());
-  // for(unsigned i = 0; i < assertions.size(); ++i)
-  //   d_assertions.push_back(assertions[i]);
-}
-
-void DecisionEngine::addAssertions(const vector<Node> &assertions,
-                                   unsigned assertionsEnd,
-                                   IteSkolemMap iteSkolemMap)
+void DecisionEngine::addAssertions(
+    const preprocessing::AssertionPipeline& assertions)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
 
-  // d_assertions.reserve(assertions.size());
-  for(unsigned i = 0; i < assertions.size(); ++i)
-    d_assertions.push_back(assertions[i]);
+  for (const Node& assertion : assertions)
+  {
+    d_assertions.push_back(assertion);
+  }
 
   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
-    d_needIteSkolemMap[i]->
-      addAssertions(assertions, assertionsEnd, iteSkolemMap);
+  {
+    d_needIteSkolemMap[i]->addAssertions(assertions);
+  }
 }
 
 }/* CVC4 namespace */
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 838e53b5a..c5325bc9a 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -24,11 +24,12 @@
 #include "base/output.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
-#include "smt/term_formula_removal.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
 
 using namespace std;
 using namespace CVC4::prop;
@@ -173,21 +174,10 @@ public:
   /*   return d_needIteSkolemMap.size() > 0; */
   /* } */
 
-  /* add a set of assertions */
-  void addAssertions(const vector<Node> &assertions);
-
   /**
-   * add a set of assertions, while providing a mapping between skolem
-   * variables and corresponding assertions. It is assumed that all
-   * assertions after assertionEnd were generated by ite
-   * removal. Hence, iteSkolemMap maps into only these.
+   * Add a list of assertions from an AssertionPipeline.
    */
-  void addAssertions(const vector<Node> &assertions,
-                     unsigned assertionsEnd,
-                     IteSkolemMap iteSkolemMap);
-
-  /* add a single assertion */
-  void addAssertion(Node n);
+  void addAssertions(const preprocessing::AssertionPipeline& assertions);
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index bad80d4ef..d26b28eeb 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__DECISION__DECISION_STRATEGY_H
 #define __CVC4__DECISION__DECISION_STRATEGY_H
 
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
@@ -57,9 +58,8 @@ public:
 
   bool needIteSkolemMap() override { return true; }
 
-  virtual void addAssertions(const std::vector<Node> &assertions,
-                             unsigned assertionsEnd,
-                             IteSkolemMap iteSkolemMap) = 0;
+  virtual void addAssertions(
+      const preprocessing::AssertionPipeline& assertions) = 0;
 };/* class ITEDecisionStrategy */
 
 class RelevancyStrategy : public ITEDecisionStrategy {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 7d19d3363..b4fbe1cbd 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -163,12 +163,10 @@ inline void computeXorIffDesiredValues
   }
 }
 
-
-
-void JustificationHeuristic::addAssertions
-(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) {
+void JustificationHeuristic::addAssertions(
+    const preprocessing::AssertionPipeline &assertions)
+{
+  size_t assertionsEnd = assertions.getRealAssertionsEnd();
 
   Trace("decision")
     << "JustificationHeuristic::addAssertions()"
@@ -177,19 +175,19 @@ void JustificationHeuristic::addAssertions
     << std::endl;
 
   // Save the 'real' assertions locally
-  for(unsigned i = 0; i < assertionsEnd; ++i)
+  for (size_t i = 0; i < assertionsEnd; i++)
+  {
     d_assertions.push_back(assertions[i]);
+  }
 
   // Save mapping between ite skolems and ite assertions
-  for(IteSkolemMap::iterator i = iteSkolemMap.begin();
-      i != iteSkolemMap.end(); ++i) {
-
-    Trace("decision::jh::ite")
-      << " jh-ite: " << (i->first) << " maps to "
-      << assertions[(i->second)] << std::endl;
-    Assert(i->second >= assertionsEnd && i->second < assertions.size());
+  for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+  {
+    Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
+                               << assertions[(i.second)] << std::endl;
+    Assert(i.second >= assertionsEnd && i.second < assertions.size());
 
-    d_iteAssertions[i->first] = assertions[i->second];
+    d_iteAssertions[i.first] = assertions[i.second];
   }
 
   // Automatic weight computation
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a70bee02c..0cd45ada7 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -32,6 +32,7 @@
 #include "decision/decision_engine.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/sat_solver_types.h"
 
 namespace CVC4 {
@@ -119,9 +120,8 @@ public:
 
   prop::SatLiteral getNext(bool &stopSearch) override;
 
-  void addAssertions(const std::vector<Node> &assertions,
-                     unsigned assertionsEnd,
-                     IteSkolemMap iteSkolemMap) override;
+  void addAssertions(
+      const preprocessing::AssertionPipeline &assertions) override;
 
  private:
   /* getNext with an option to specify threshold */
diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h
index 92ed555fd..23bf0e01f 100644
--- a/src/include/cvc4_private_library.h
+++ b/src/include/cvc4_private_library.h
@@ -19,7 +19,10 @@
 #ifndef __CVC4_PRIVATE_LIBRARY_H
 #define __CVC4_PRIVATE_LIBRARY_H
 
-#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER))
+#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \
+      || defined(__BUILDING_CVC4PARSERLIB)                                 \
+      || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)                       \
+      || defined(__BUILDING_CVC4DRIVER))
 #  error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
 #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */
 
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
new file mode 100644
index 000000000..0bce3b8cd
--- /dev/null
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file assertion_pipeline.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "preprocessing/assertion_pipeline.h"
+
+#include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "proof/proof_manager.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {}
+
+void AssertionPipeline::replace(size_t i, Node n)
+{
+  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
+  d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i,
+                                Node n,
+                                const std::vector<Node>& addnDeps)
+{
+  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+        for (const auto& addnDep
+             : addnDeps) {
+          ProofManager::currentPM()->addDependence(n, addnDep);
+        });
+  d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
+{
+  PROOF(
+      for (const auto& n
+           : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
+  d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
+
+  for (const auto& n : ns)
+  {
+    d_nodes.push_back(n);
+  }
+}
+
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
new file mode 100644
index 000000000..af7a8dce3
--- /dev/null
+++ b/src/preprocessing/assertion_pipeline.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file assertion_pipeline.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/term_formula_removal.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+/**
+ * Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes. It is assumed that all assertions after d_realAssertionsEnd were
+ * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
+ */
+class AssertionPipeline
+{
+ public:
+  AssertionPipeline();
+
+  size_t size() const { return d_nodes.size(); }
+
+  void resize(size_t n) { d_nodes.resize(n); }
+
+  void clear()
+  {
+    d_nodes.clear();
+    d_realAssertionsEnd = 0;
+  }
+
+  Node& operator[](size_t i) { return d_nodes[i]; }
+  const Node& operator[](size_t i) const { return d_nodes[i]; }
+  void push_back(Node n) { d_nodes.push_back(n); }
+
+  std::vector<Node>& ref() { return d_nodes; }
+  const std::vector<Node>& ref() const { return d_nodes; }
+
+  std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
+  std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
+
+  /*
+   * Replaces assertion i with node n and records the dependency between the
+   * original assertion and its replacement.
+   */
+  void replace(size_t i, Node n);
+
+  /*
+   * Replaces assertion i with node n and records that this replacement depends
+   * on assertion i and the nodes listed in addnDeps. The dependency
+   * information is used for unsat cores and proofs.
+   */
+  void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
+
+  /*
+   * Replaces an assertion with a vector of assertions and records the
+   * dependencies.
+   */
+  void replace(size_t i, const std::vector<Node>& ns);
+
+  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+  const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
+
+  size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
+
+  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
+
+ private:
+  std::vector<Node> d_nodes;
+
+  /**
+   * Map from skolem variables to index in d_assertions containing
+   * corresponding introduced Boolean ite
+   */
+  IteSkolemMap d_iteSkolemMap;
+
+  /** Size of d_nodes when preprocessing starts */
+  size_t d_realAssertionsEnd;
+}; /* class AssertionPipeline */
+
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 6fb4b7793..f5c3520d0 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -44,8 +44,9 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     // When solving incrementally, all substitutions are piled into the
     // assertion at d_substitutionsIndex: we don't want to apply substitutions
     // to this assertion or information will be lost.
-    context::CDO<unsigned>& substs_index =
-        assertionsToPreprocess->getSubstitutionsIndex();
+    unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
+    theory::SubstitutionMap& substMap =
+        d_preprocContext->getTopLevelSubstitutions();
     unsigned size = assertionsToPreprocess->size();
     unsigned substitutionAssertion = substs_index > 0 ? substs_index : size;
     for (unsigned i = 0; i < size; ++i)
@@ -57,11 +58,9 @@ PreprocessingPassResult ApplySubsts::applyInternal(
       Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
                         << std::endl;
       d_preprocContext->spendResource(options::preprocessStep());
-      assertionsToPreprocess->replace(
-          i,
-          theory::Rewriter::rewrite(
-              assertionsToPreprocess->getTopLevelSubstitutions().apply(
-                  (*assertionsToPreprocess)[i])));
+      assertionsToPreprocess->replace(i,
+                                      theory::Rewriter::rewrite(substMap.apply(
+                                          (*assertionsToPreprocess)[i])));
       Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
                         << std::endl;
     }
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 81588d039..616ecd969 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
       propagator->getBackEdges();
   unordered_set<unsigned long> removeAssertions;
   SubstitutionMap& top_level_substs =
-      assertionsToPreprocess->getTopLevelSubstitutions();
+      d_preprocContext->getTopLevelSubstitutions();
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index e2ce1c301..653aed8ad 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -76,8 +76,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
 
   // Assert all the assertions to the propagator
   Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
-  context::CDO<unsigned>& substs_index =
-      assertionsToPreprocess->getSubstitutionsIndex();
+  unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
@@ -114,7 +113,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   SubstitutionMap& top_level_substs =
-      assertionsToPreprocess->getTopLevelSubstitutions();
+      d_preprocContext->getTopLevelSubstitutions();
   SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
   SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
   SubstitutionMap::iterator pos;
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 6a7078696..6a1d89d33 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -16,51 +16,12 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-#include "expr/node_manager.h"
-#include "proof/proof.h"
 #include "smt/dump.h"
 #include "smt/smt_statistics_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
-AssertionPipeline::AssertionPipeline(context::Context* context)
-    : d_substitutionsIndex(context, 0),
-      d_topLevelSubstitutions(context),
-      d_realAssertionsEnd(0)
-{
-}
-
-void AssertionPipeline::replace(size_t i, Node n) {
-  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
-  d_nodes[i] = n;
-}
-
-void AssertionPipeline::replace(size_t i,
-                                Node n,
-                                const std::vector<Node>& addnDeps)
-{
-  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
-        for (const auto& addnDep
-             : addnDeps) {
-          ProofManager::currentPM()->addDependence(n, addnDep);
-        });
-  d_nodes[i] = n;
-}
-
-void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
-{
-  PROOF(
-      for (const auto& n
-           : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
-  d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
-
-  for (const auto& n : ns)
-  {
-    d_nodes.push_back(n);
-  }
-}
-
 PreprocessingPassResult PreprocessingPass::apply(
     AssertionPipeline* assertionsToPreprocess) {
   TimerStat::CodeTimer codeTimer(d_timer);
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 4143f2d4b..448cacb87 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -32,103 +32,16 @@
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
 
 #include <string>
-#include <vector>
 
-#include "context/cdo.h"
-#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine_scope.h"
-#include "smt/term_formula_removal.h"
 #include "theory/logic_info.h"
-#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
 /**
- * Assertion Pipeline stores a list of assertions modified by preprocessing
- * passes.
- */
-class AssertionPipeline
-{
- public:
-  AssertionPipeline(context::Context* context);
-
-  size_t size() const { return d_nodes.size(); }
-
-  void resize(size_t n) { d_nodes.resize(n); }
-
-  void clear()
-  {
-    d_nodes.clear();
-    d_realAssertionsEnd = 0;
-  }
-
-  Node& operator[](size_t i) { return d_nodes[i]; }
-  const Node& operator[](size_t i) const { return d_nodes[i]; }
-  void push_back(Node n) { d_nodes.push_back(n); }
-
-  std::vector<Node>& ref() { return d_nodes; }
-  const std::vector<Node>& ref() const { return d_nodes; }
-
-  std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
-  std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
-
-  /*
-   * Replaces assertion i with node n and records the dependency between the
-   * original assertion and its replacement.
-   */
-  void replace(size_t i, Node n);
-
-  /*
-   * Replaces assertion i with node n and records that this replacement depends
-   * on assertion i and the nodes listed in addnDeps. The dependency
-   * information is used for unsat cores and proofs.
-   */
-  void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
-
-  /*
-   * Replaces an assertion with a vector of assertions and records the
-   * dependencies.
-   */
-  void replace(size_t i, const std::vector<Node>& ns);
-
-  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
-
-  context::CDO<unsigned>& getSubstitutionsIndex()
-  {
-    return d_substitutionsIndex;
-  }
-
-  theory::SubstitutionMap& getTopLevelSubstitutions()
-  {
-    return d_topLevelSubstitutions;
-  }
-
-  size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
-
-  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
-
- private:
-  std::vector<Node> d_nodes;
-
-  /**
-   * Map from skolem variables to index in d_assertions containing
-   * corresponding introduced Boolean ite
-   */
-  IteSkolemMap d_iteSkolemMap;
-
-  /* Index for where to store substitutions */
-  context::CDO<unsigned> d_substitutionsIndex;
-
-  /* The top level substitutions */
-  theory::SubstitutionMap d_topLevelSubstitutions;
-
-  /** Size of d_nodes when preprocessing starts */
-  size_t d_realAssertionsEnd;
-}; /* class AssertionPipeline */
-
-/**
  * Preprocessing passes return a result which indicates whether a conflict has
  * been detected during preprocessing.
  */
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 15f5d3eb0..3f72a4559 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -29,6 +29,8 @@ PreprocessingPassContext::PreprocessingPassContext(
     : d_smt(smt),
       d_resourceManager(resourceManager),
       d_iteRemover(iteRemover),
+      d_substitutionsIndex(smt->d_userContext, 0),
+      d_topLevelSubstitutions(smt->d_userContext),
       d_circuitPropagator(circuitPropagator),
       d_symsInAssertions(smt->d_userContext)
 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index ae989d700..3eb0f10b5 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,6 +21,7 @@
 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
+#include "context/cdo.h"
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "preprocessing/util/ite_utilities.h"
@@ -70,6 +71,16 @@ class PreprocessingPassContext
   /* Widen the logic to include the given theory. */
   void widenLogic(theory::TheoryId id);
 
+  unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); }
+
+  void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; }
+
+  /** Gets a reference to the top-level substitution map */
+  theory::SubstitutionMap& getTopLevelSubstitutions()
+  {
+    return d_topLevelSubstitutions;
+  }
+
   /* Enable Integers. */
   void enableIntegers();
 
@@ -90,6 +101,12 @@ class PreprocessingPassContext
   /** Instance of the ITE remover */
   RemoveTermFormulas* d_iteRemover;
 
+  /* Index for where to store substitutions */
+  context::CDO<unsigned> d_substitutionsIndex;
+
+  /* The top level substitutions */
+  theory::SubstitutionMap d_topLevelSubstitutions;
+
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 73264daa5..eeacb9c3f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -568,7 +568,7 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_managedReplayLog(),
         d_listenerRegistrations(new ListenerRegistrationList()),
         d_propagator(true, true),
-        d_assertions(d_smt.d_userContext),
+        d_assertions(),
         d_assertionsProcessed(smt.d_userContext, false),
         d_fakeContext(),
         d_abstractValueMap(&d_fakeContext),
@@ -715,7 +715,7 @@ class SmtEnginePrivate : public NodeManagerListener {
   Node applySubstitutions(TNode node)
   {
     return Rewriter::rewrite(
-        d_assertions.getTopLevelSubstitutions().apply(node));
+        d_preprocessingPassContext->getTopLevelSubstitutions().apply(node));
   }
 
   /**
@@ -3113,7 +3113,8 @@ void SmtEnginePrivate::processAssertions() {
   spendResource(options::preprocessStep());
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
-  SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions();
+  SubstitutionMap& top_level_substs =
+      d_preprocessingPassContext->getTopLevelSubstitutions();
 
   // Dump the assertions
   dumpAssertions("pre-everything", d_assertions);
@@ -3138,7 +3139,7 @@ void SmtEnginePrivate::processAssertions() {
     // proper data structure.
 
     // Placeholder for storing substitutions
-    d_assertions.getSubstitutionsIndex() = d_assertions.size();
+    d_preprocessingPassContext->setSubstitutionsIndex(d_assertions.size());
     d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
   }
 
@@ -3478,9 +3479,7 @@ void SmtEnginePrivate::processAssertions() {
   if(noConflict) {
     Chat() << "pushing to decision engine..." << endl;
     Assert(iteRewriteAssertionsEnd == d_assertions.size());
-    d_smt.d_decisionEngine->addAssertions(d_assertions.ref(),
-                                          d_assertions.getRealAssertionsEnd(),
-                                          getIteSkolemMap());
+    d_smt.d_decisionEngine->addAssertions(d_assertions);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 95a60afac..8c9b39ea4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -67,10 +67,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
   d_check_vts_lemma_lc = false;
 }
 
-InstStrategyCegqi::~InstStrategyCegqi()
-{
-
-}
+InstStrategyCegqi::~InstStrategyCegqi() {}
 
 bool InstStrategyCegqi::needsCheck(Theory::Effort e)
 {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 92a355348..95ec24df9 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1194,16 +1194,17 @@ bool MatchGen::reset_round(QuantConflictFind* p)
     d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
   }
   if( d_type==typ_ground ){
-    //int e = p->evaluate( d_n );
-    //if( e==1 ){
+    // int e = p->evaluate( d_n );
+    // if( e==1 ){
     //  d_ground_eval[0] = p->d_true;
     //}else if( e==-1 ){
     //  d_ground_eval[0] = p->d_false;
     //}
-    //modified
+    // modified
     TermDb* tdb = p->getTermDatabase();
     QuantifiersEngine* qe = p->getQuantifiersEngine();
-    for( unsigned i=0; i<2; i++ ){
+    for (unsigned i = 0; i < 2; i++)
+    {
       if (tdb->isEntailed(d_n, i == 0))
       {
         d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
@@ -1220,7 +1221,7 @@ bool MatchGen::reset_round(QuantConflictFind* p)
     {
       if (!expr::hasBoundVar(d_n[i]))
       {
-        TNode t = tdb->getEntailedTerm(d_n[i]);        
+        TNode t = tdb->getEntailedTerm(d_n[i]);
         if (qe->inConflict())
         {
           return false;
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index fe1dc30a4..09525712f 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -307,8 +307,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   }
   Trace("cegqi-engine") << "...success:" << std::endl;
   Trace("cegqi-engine") << ss.str();
-  Trace("sygus-repair-const") << "Repaired constants in solution : "
-                              << std::endl;
+  Trace("sygus-repair-const")
+      << "Repaired constants in solution : " << std::endl;
   Trace("sygus-repair-const") << ss.str();
   return true;
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 37276ac5e..b9c3ccc4e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -29,6 +29,7 @@
 #include "options/options.h"
 #include "options/proof_options.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "proof/cnf_proof.h"
 #include "proof/lemma_proof.h"
 #include "proof/proof_manager.h"
@@ -53,6 +54,7 @@
 
 using namespace std;
 
+using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 
 namespace CVC4 {
@@ -1818,8 +1820,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
-  std::vector<Node> additionalLemmas;
-  IteSkolemMap iteSkolemMap;
+  AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
   Node ppNode = preprocess ? this->preprocess(node) : Node(node);
@@ -1827,9 +1828,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   // Remove the ITEs
   Debug("ite") << "Remove ITE from " << ppNode << std::endl;
   additionalLemmas.push_back(ppNode);
-  d_tform_remover.run(additionalLemmas, iteSkolemMap);
+  additionalLemmas.updateRealAssertionsEnd();
+  d_tform_remover.run(additionalLemmas.ref(),
+                      additionalLemmas.getIteSkolemMap());
   Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
-  additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
+  additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0]));
 
   if(Debug.isOn("lemma-ites")) {
     Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
@@ -1846,19 +1849,19 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   // assert to prop engine
   d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
-    additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
+    additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i]));
     d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
   if(negated) {
-    additionalLemmas[0] = additionalLemmas[0].notNode();
+    additionalLemmas.replace(0, additionalLemmas[0].notNode());
     negated = false;
   }
 
   // assert to decision engine
   if(!removable) {
-    d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
+    d_decisionEngine->addAssertions(additionalLemmas);
   }
 
   // Mark that we added some lemmas
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index f238ba8be..8ba6da0bf 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -2378,8 +2378,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3);
 
-    context::Context context;
-    AssertionPipeline apipe(&context);
+    AssertionPipeline apipe;
     apipe.push_back(a);
     passes::BVGauss bgauss(nullptr);
     std::unordered_map<Node, Node, NodeHashFunction> res;
@@ -2461,8 +2460,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3);
 
-    context::Context context;
-    AssertionPipeline apipe(&context);
+    AssertionPipeline apipe;
     apipe.push_back(a);
     apipe.push_back(eq4);
     apipe.push_back(eq5);
@@ -2513,8 +2511,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
             d_p),
         d_nine);
 
-    context::Context context;
-    AssertionPipeline apipe(&context);
+    AssertionPipeline apipe;
     apipe.push_back(eq1);
     apipe.push_back(eq2);
     passes::BVGauss bgauss(nullptr);