Make substitution index context-independent (#2474)

When we do solving in incremental mode, we store substitutions at a
special index in our list of assertions. Previously, we used a
context-dependent variable for that. However, this is not needed since
the list of assertions just consists of the assertions currently being
processed, which are independent of the assertions seen so far. This
commit changes the index to be an ordinary integer and moves it to the
AssertionPipeline. Additionally, it abstracts access to the index in
preparation for splitting AssertionPipeline into three vectors (see
issue #2473).

2 files changed, 4 insertions, 18 deletions

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index ddacc20c0..791bb2dc7 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -41,17 +41,12 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     // TODO(#1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
 
-    // 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.
-    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)
     {
-      if (i == substitutionAssertion)
+      if (assertionsToPreprocess->isSubstsIndex(i))
       {
         continue;
       }
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 4a0f38689..139bf96a9 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -76,13 +76,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
 
   // Assert all the assertions to the propagator
   Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
-  unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
            == (*assertionsToPreprocess)[i]);
     // Don't reprocess substitutions
-    if (substs_index > 0 && i == substs_index)
+    if (assertionsToPreprocess->isSubstsIndex(i))
     {
       continue;
     }
@@ -344,14 +343,13 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
   Assert(m != nullptr);
   NodeManager* nm = NodeManager::currentNM();
-  NodeBuilder<> substitutionsBuilder(kind::AND);
   for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos)
   {
     Node lhs = (*pos).first;
     Node rhs = newSubstitutions.apply((*pos).second);
     // If using incremental, we must check whether this variable has occurred
     // before now. If it hasn't we can add this as a substitution.
-    if (substs_index == 0
+    if (!assertionsToPreprocess->storeSubstsInAsserts()
         || d_preprocContext->getSymsInAssertions().find(lhs)
                == d_preprocContext->getSymsInAssertions().end())
     {
@@ -366,16 +364,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       Trace("non-clausal-simplify")
           << "substitute: will notify SAT layer of substitution: " << eq
           << std::endl;
-      substitutionsBuilder << eq;
+      assertionsToPreprocess->addSubstitutionNode(eq);
     }
   }
-  // add to the last assertion if necessary
-  if (substitutionsBuilder.getNumChildren() > 0)
-  {
-    substitutionsBuilder << (*assertionsToPreprocess)[substs_index];
-    assertionsToPreprocess->replace(
-        substs_index, Rewriter::rewrite(Node(substitutionsBuilder)));
-  }
 
   NodeBuilder<> learnedBuilder(kind::AND);
   Assert(assertionsToPreprocess->getRealAssertionsEnd()