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).

1 files changed, 0 insertions, 7 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index e37680538..37744151c 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -71,10 +71,6 @@ 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()
   {
@@ -101,9 +97,6 @@ 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;