Unify top-level substitutions and model substitutions (#6499)

This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.

The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.

There is no reason to have these two things be separate.

4 files changed, 32 insertions, 47 deletions

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 893cf0239..e9819072d 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -550,7 +550,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
                   << "unexpected solution from arith's ppAssert()";
               Assert(nullMap.empty())
                   << "unexpected substitution from arith's ppAssert()";
-              d_preprocContext->addModelSubstitution(*ii, newVar.eqNode(one));
               newVars.push_back(newVar);
               varRef = newVar;
             }
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 2fcc6f76f..d68c30a11 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -327,34 +327,32 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         << "non-clausal preprocessed: " << assertion << std::endl;
   }
 
-  // add substitutions to model, or as assertions if needed (when incremental)
-  NodeManager* nm = NodeManager::currentNM();
-  for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
+  // If necessary, add as assertions if needed (when incremental). This is
+  // necessary because certain variables cannot truly be eliminated when
+  // we are in incremental mode. For example, say our first call to check-sat
+  // is a formula F containing variable x. On the second call to check-sat,
+  // say we solve a top-level assertion (= x t). Since the solver already has
+  // constraints involving x, we must still keep (= x t) as an assertion.
+  // However, notice that we do not retract the substitution { x -> t }. This
+  // means that all *subsequent* assertions after (= x t) will replace x by t.
+  if (assertionsToPreprocess->storeSubstsInAsserts())
   {
-    Node lhs = (*pos).first;
-    TrustNode trhs = newSubstitutions->applyTrusted((*pos).second);
-    Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode();
-    // 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 (!assertionsToPreprocess->storeSubstsInAsserts()
-        || d_preprocContext->getSymsInAssertions().find(lhs)
-               == d_preprocContext->getSymsInAssertions().end())
+    for (const std::pair<const Node, const Node>& pos: nss)
     {
-      Trace("non-clausal-simplify")
-          << "substitute: " << lhs << " " << rhs << std::endl;
-      d_preprocContext->addModelSubstitution(lhs, rhs);
-    }
-    else
-    {
-      // if it has, the substitution becomes an assertion
-      Node eq = nm->mkNode(kind::EQUAL, lhs, rhs);
-      Trace("non-clausal-simplify")
-          << "substitute: will notify SAT layer of substitution: " << eq
-          << std::endl;
-      trhs = newSubstitutions->applyTrusted((*pos).first);
-      Assert(!trhs.isNull());
-      assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
-                                                  trhs.getGenerator());
+      Node lhs = pos.first;
+      // If using incremental, we must check whether this variable has occurred
+      // before now. If it has, we must add as an assertion.
+      if (d_preprocContext->getSymsInAssertions().contains(lhs))
+      {
+        // if it has, the substitution becomes an assertion
+        TrustNode trhs = newSubstitutions->applyTrusted(lhs);
+        Assert(!trhs.isNull());
+        Trace("non-clausal-simplify")
+            << "substitute: will notify SAT layer of substitution: "
+            << trhs.getProven() << std::endl;
+        assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
+                                                    trhs.getGenerator());
+      }
     }
   }
 
@@ -438,6 +436,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   }
 
   propagator->setNeedsFinish(true);
+
+  // Note that typically ttls.apply(assert)==assert here.
+  // However, this invariant is invalidated for cases where we use explicit
+  // equality assertions for variables solved in incremental mode that already
+  // exist in assertions, as described above.
+
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 139fa4153..9e8a4efc8 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -67,20 +67,11 @@ void PreprocessingPassContext::recordSymbolsInAssertions(
   }
 }
 
-void PreprocessingPassContext::addModelSubstitution(const Node& lhs,
-                                                    const Node& rhs)
-{
-  getTheoryEngine()->getModel()->addSubstitution(lhs,
-                                                 d_smt->expandDefinitions(rhs));
-}
-
 void PreprocessingPassContext::addSubstitution(const Node& lhs,
                                                const Node& rhs,
                                                ProofGenerator* pg)
 {
   getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg);
-  // also add as a model substitution
-  addModelSubstitution(lhs, rhs);
 }
 
 void PreprocessingPassContext::addSubstitution(const Node& lhs,
@@ -89,8 +80,6 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs,
                                                const std::vector<Node>& args)
 {
   getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
-  // also add as a model substitution
-  addModelSubstitution(lhs, rhs);
 }
 
 ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a4ca166d8..a14fafb47 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -78,15 +78,8 @@ class PreprocessingPassContext
   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
 
   /**
-   * Add substitution to theory model. This method should only be called if
-   * we have already added the substitution to the top-level substitutions
-   * class. Otherwise, addSubstitution should be called instead.
-   * @param lhs The node replaced by node 'rhs'
-   * @param rhs The node to substitute node 'lhs'
-   */
-  void addModelSubstitution(const Node& lhs, const Node& rhs);
-  /**
-   * Add substitution to the top-level substitutions and to the theory model.
+   * Add substitution to the top-level substitutions, which also as a
+   * consequence is used by the theory model.
    * @param lhs The node replaced by node 'rhs'
    * @param rhs The node to substitute node 'lhs'
    * @param pg The proof generator that can provide a proof of lhs == rhs.