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

6 files changed, 77 insertions, 27 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 382b1eb63..7408f4ba3 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,12 +18,17 @@
 #include "expr/node_manager.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
 AssertionPipeline::AssertionPipeline()
-    : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0)
+    : d_realAssertionsEnd(0),
+      d_storeSubstsInAsserts(false),
+      d_substsIndex(0),
+      d_assumptionsStart(0),
+      d_numAssumptions(0)
 {
 }
 
@@ -84,5 +89,27 @@ void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
   }
 }
 
+void AssertionPipeline::enableStoreSubstsInAsserts()
+{
+  d_storeSubstsInAsserts = true;
+  d_substsIndex = d_nodes.size();
+  d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+}
+
+void AssertionPipeline::disableStoreSubstsInAsserts()
+{
+  d_storeSubstsInAsserts = false;
+}
+
+void AssertionPipeline::addSubstitutionNode(Node n)
+{
+  Assert(d_storeSubstsInAsserts);
+  Assert(n.getKind() == kind::EQUAL);
+  d_nodes[d_substsIndex] = theory::Rewriter::rewrite(
+      NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex]));
+  Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex])
+         == d_nodes[d_substsIndex]);
+}
+
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index cc9d1c2af..b133bc490 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -95,6 +95,37 @@ class AssertionPipeline
 
   void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
 
+  /**
+   * Returns true if substitutions must be stored as assertions. This is for
+   * example the case when we do incremental solving.
+   */
+  bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; }
+
+  /**
+   * Enables storing substitutions as assertions.
+   */
+  void enableStoreSubstsInAsserts();
+
+  /**
+   * Disables storing substitutions as assertions.
+   */
+  void disableStoreSubstsInAsserts();
+
+  /**
+   * Adds a substitution node of the form (= lhs rhs) to the assertions.
+   */
+  void addSubstitutionNode(Node n);
+
+  /**
+   * Checks whether the assertion at a given index represents substitutions.
+   *
+   * @param i The index in question
+   */
+  bool isSubstsIndex(size_t i)
+  {
+    return d_storeSubstsInAsserts && i == d_substsIndex;
+  }
+
  private:
   /** The list of current assertions */
   std::vector<Node> d_nodes;
@@ -108,6 +139,20 @@ class AssertionPipeline
   /** Size of d_nodes when preprocessing starts */
   size_t d_realAssertionsEnd;
 
+  /**
+   * If true, we store the substitutions as assertions. This is necessary when
+   * doing incremental solving because we cannot apply them to existing
+   * assertions while preprocessing new assertions.
+   */
+  bool d_storeSubstsInAsserts;
+
+  /**
+   * The index of the assertions that holds the substitutions.
+   *
+   * TODO(#2473): replace by separate vector of substitution assertions.
+   */
+  size_t d_substsIndex;
+
   /** Index of the first assumption */
   size_t d_assumptionsStart;
   /** The number of assumptions */
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()
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 2d25502d1..b04c05b9e 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -29,7 +29,6 @@ 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 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;