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.

3 files changed, 9 insertions, 11 deletions

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;