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.

16 files changed, 81 insertions, 106 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.
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 22c91b5bb..7ed3093b7 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -273,7 +273,6 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){
   Debug("arith::ite") << "adding " << f << " -> " << t << endl;
   d_subcount = d_subcount + 1;
   d_subs->addSubstitution(f, t);
-  d_model->addSubstitution(f, t);
 }
 
 Node ArithIteUtils::applySubstitutions(TNode f){
diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 4a6a1f150..fa020e96b 100644
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -26,9 +26,10 @@ namespace theory {
 
 CombinationCareGraph::CombinationCareGraph(
     TheoryEngine& te,
+    Env& env,
     const std::vector<Theory*>& paraTheories,
     ProofNodeManager* pnm)
-    : CombinationEngine(te, paraTheories, pnm)
+    : CombinationEngine(te, env, paraTheories, pnm)
 {
 }
 
diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h
index 437831678..971b81d1d 100644
--- a/src/theory/combination_care_graph.h
+++ b/src/theory/combination_care_graph.h
@@ -36,6 +36,7 @@ class CombinationCareGraph : public CombinationEngine
 {
  public:
   CombinationCareGraph(TheoryEngine& te,
+                       Env& env,
                        const std::vector<Theory*>& paraTheories,
                        ProofNodeManager* pnm);
   ~CombinationCareGraph();
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 4b04188f1..33300ead8 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -29,9 +29,11 @@ namespace cvc5 {
 namespace theory {
 
 CombinationEngine::CombinationEngine(TheoryEngine& te,
+                                     Env& env,
                                      const std::vector<Theory*>& paraTheories,
                                      ProofNodeManager* pnm)
     : d_te(te),
+      d_env(env),
       d_valuation(&te),
       d_pnm(pnm),
       d_logicInfo(te.getLogicInfo()),
@@ -51,7 +53,8 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
     d_eemanager.reset(
         new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
     // make the distributed model manager
-    d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
+    d_mmanager.reset(
+        new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
   }
   else
   {
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 6430e2325..063cefd49 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -27,6 +27,7 @@
 namespace cvc5 {
 
 class TheoryEngine;
+class Env;
 
 namespace theory {
 
@@ -45,6 +46,7 @@ class CombinationEngine
 {
  public:
   CombinationEngine(TheoryEngine& te,
+                    Env& env,
                     const std::vector<Theory*>& paraTheories,
                     ProofNodeManager* pnm);
   virtual ~CombinationEngine();
@@ -107,6 +109,8 @@ class CombinationEngine
   void sendLemma(TrustNode trn, TheoryId atomsTo);
   /** Reference to the theory engine */
   TheoryEngine& d_te;
+  /** Reference to the environment */
+  Env& d_env;
   /** Valuation for the engine */
   Valuation d_valuation;
   /** The proof node manager */
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index b7499447f..c1c488f65 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -18,23 +18,23 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
-#include "theory/quantifiers_engine.h"
+#include "smt/env.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 namespace cvc5 {
 namespace theory {
 
-ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem)
+ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
     : d_te(te),
-      d_logicInfo(te.getLogicInfo()),
+      d_env(env),
       d_eem(eem),
       d_modelEqualityEngine(nullptr),
       d_modelEqualityEngineAlloc(nullptr),
-      d_model(new TheoryModel(te.getUserContext(),
-                              "DefaultModel",
-                              options::assignFunctionValues())),
+      d_model(new TheoryModel(
+          env, "DefaultModel", options::assignFunctionValues())),
       d_modelBuilder(nullptr),
       d_modelBuilt(false),
       d_modelBuiltSuccess(false)
@@ -46,7 +46,7 @@ ModelManager::~ModelManager() {}
 void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
 {
   // construct the model
-  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  const LogicInfo& logicInfo = d_env.getLogicInfo();
   // Initialize the model and model builder.
   if (logicInfo.isQuantified())
   {
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 41559e7b6..ff8459fcb 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -26,6 +26,7 @@
 namespace cvc5 {
 
 class TheoryEngine;
+class Env;
 
 namespace theory {
 
@@ -42,7 +43,7 @@ class TheoryModel;
 class ModelManager
 {
  public:
-  ModelManager(TheoryEngine& te, EqEngineManager& eem);
+  ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem);
   virtual ~ModelManager();
   /**
    * Finish initializing this class, which allocates the model, the model
@@ -125,8 +126,8 @@ class ModelManager
   void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
   /** Reference to the theory engine */
   TheoryEngine& d_te;
-  /** Logic info of theory engine (cached) */
-  const LogicInfo& d_logicInfo;
+  /** Reference to the environment */
+  Env& d_env;
   /** The equality engine manager */
   EqEngineManager& d_eem;
   /**
diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index f3a501f94..4124407be 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/model_manager_distributed.h"
 
+#include "smt/env.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 #include "theory/theory_model_builder.h"
@@ -23,8 +24,9 @@ namespace cvc5 {
 namespace theory {
 
 ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
+                                                 Env& env,
                                                  EqEngineManager& eem)
-    : ModelManager(te, eem)
+    : ModelManager(te, env, eem)
 {
 }
 
@@ -69,10 +71,11 @@ bool ModelManagerDistributed::prepareModel()
   // model, which includes both dump their equality information and assigning
   // values. Notice the order of theories here is important and is the same
   // as the list in CVC5_FOR_EACH_THEORY in theory_engine.cpp.
+  const LogicInfo& logicInfo = d_env.getLogicInfo();
   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
        ++theoryId)
   {
-    if (!d_logicInfo.isTheoryEnabled(theoryId))
+    if (!logicInfo.isTheoryEnabled(theoryId))
     {
       // theory not active, skip
       continue;
diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h
index 1a79eec9a..322e61a98 100644
--- a/src/theory/model_manager_distributed.h
+++ b/src/theory/model_manager_distributed.h
@@ -22,9 +22,6 @@
 #include "theory/model_manager.h"
 
 namespace cvc5 {
-
-class TheoryEngine;
-
 namespace theory {
 
 /**
@@ -41,7 +38,7 @@ namespace theory {
 class ModelManagerDistributed : public ModelManager
 {
  public:
-  ModelManagerDistributed(TheoryEngine& te, EqEngineManager& eem);
+  ModelManagerDistributed(TheoryEngine& te, Env& env, EqEngineManager& eem);
   ~ModelManagerDistributed();
 
   /** Prepare the model, as described above. */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ccdd2bf4b..1acaca34f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -146,7 +146,7 @@ void TheoryEngine::finishInit()
   // Initialize the theory combination architecture
   if (options::tcMode() == options::TcMode::CARE_GRAPH)
   {
-    d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
+    d_tc.reset(new CombinationCareGraph(*this, d_env, paraTheories, d_pnm));
   }
   else
   {
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 1543739e0..a95546cf5 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -19,8 +19,10 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "theory/rewriter.h"
+#include "theory/trust_substitutions.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -29,11 +31,9 @@ using namespace cvc5::context;
 namespace cvc5 {
 namespace theory {
 
-TheoryModel::TheoryModel(context::Context* c,
-                         std::string name,
-                         bool enableFuncModels)
-    : d_name(name),
-      d_substitutions(c),
+TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels)
+    : d_env(env),
+      d_name(name),
       d_equalityEngine(nullptr),
       d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
@@ -137,7 +137,7 @@ std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
 Node TheoryModel::getValue(TNode n) const
 {
   //apply substitutions
-  Node nn = d_substitutions.apply(n);
+  Node nn = d_env.getTopLevelSubstitutions().apply(n);
   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
   //get value in model
   nn = getModelValue(nn);
@@ -367,26 +367,6 @@ Node TheoryModel::getModelValue(TNode n) const
   return n;
 }
 
-/** add substitution */
-void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
-  if( !d_substitutions.hasSubstitution( x ) ){
-    Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl;
-    d_substitutions.addSubstitution( x, t, invalidateCache );
-  } else {
-#ifdef CVC5_ASSERTIONS
-    Node oldX = d_substitutions.getSubstitution(x);
-    // check that either the old substitution is the same, or it now maps to the new substitution
-    if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
-      InternalError()
-          << "Two incompatible substitutions added to TheoryModel:\n"
-          << "the term:    " << x << "\n"
-          << "old mapping: " << d_substitutions.apply(oldX) << "\n"
-          << "new mapping: " << d_substitutions.apply(t);
-    }
-#endif /* CVC5_ASSERTIONS */
-  }
-}
-
 /** add term */
 void TheoryModel::addTermInternal(TNode n)
 {
@@ -747,7 +727,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
     Node n = it->first;
     Assert(!n.isNull());
     // should not have been solved for in a substitution
-    Assert(d_substitutions.apply(n) == n);
+    Assert(d_env.getTopLevelSubstitutions().apply(n) == n);
     if( !hasAssignedFunctionDefinition( n ) ){
       Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
       if( options::ufHo() ){
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index b4a089767..ab66e8fe7 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -23,12 +23,14 @@
 
 #include "theory/ee_setup_info.h"
 #include "theory/rep_set.h"
-#include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
 #include "theory/type_set.h"
 #include "theory/uf/equality_engine.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 
 /** Theory Model class.
@@ -38,16 +40,16 @@ namespace theory {
  * (1) d_equalityEngine : an equality engine object, which stores
  *     an equivalence relation over all terms that exist in
  *     the current set of assertions.
- * (2) d_substitutions : a substitution map storing cases of
- *     explicitly solved terms, for instance during preprocessing.
- * (3) d_reps : a map from equivalence class representatives of
+ * (2) d_reps : a map from equivalence class representatives of
  *     the equality engine to the (constant) representatives
  *     assigned to that equivalence class.
- * (4) d_uf_models : a map from uninterpreted functions to their
+ * (3) d_uf_models : a map from uninterpreted functions to their
  *     lambda representation.
- * (5) d_rep_set : a data structure that allows interpretations
+ * (4) d_rep_set : a data structure that allows interpretations
  *     for types to be represented as terms. This is useful for
  *     finite model finding.
+ * Additionally, models are dependent on top-level substitutions stored in the
+ * d_env class.
  *
  * These data structures are built after a full effort check with
  * no lemmas sent, within a call to:
@@ -79,8 +81,9 @@ namespace theory {
 class TheoryModel
 {
   friend class TheoryEngineModelBuilder;
-public:
-  TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
+
+ public:
+  TheoryModel(Env& env, std::string name, bool enableFuncModels);
   virtual ~TheoryModel();
   /**
    * Finish init, where ee is the equality engine the model should use.
@@ -90,8 +93,6 @@ public:
   /** reset the model */
   virtual void reset();
   //---------------------------- for building the model
-  /** Adds a substitution from x to t. */
-  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
   /** assert equality holds in the model
    *
    * This method returns true if and only if the equality engine of this model
@@ -355,10 +356,10 @@ public:
   std::string debugPrintModelEqc() const;
 
  protected:
+  /** Reference to the environmanet */
+  Env& d_env;
   /** Unique name of this model */
   std::string d_name;
-  /** substitution map for this model */
-  SubstitutionMap d_substitutions;
   /** equality engine containing all known equalities/disequalities */
   eq::EqualityEngine* d_equalityEngine;
   /** approximations (see recordApproximation) */