Connect combination engine to theory engine (#4940)

This connects the implementation of CombinationEngine into TheoryEngine. By default, the combination engine of theory engine is CombinationCareGraph.

This PR also consolidates and simplifies how models are built, note that:

The TheoryModel object no longer tracks whether it is built, instead that is the job of ModelManager,
The TheoryModelBuilder object is no longer responsible for calling TheoryEngine's collect model info method.
Quantifiers engine uses a simpler interface for ensuring that TheoryEngine's model is built.
This PR also makes some minor simplifications to TheoryEngine from the centralEe branch.

Note that no significant behavior changes are intended in this PR.

1 files changed, 125 insertions, 274 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 647a40999..0979d447b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -41,8 +41,8 @@
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/care_graph.h"
+#include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
-#include "theory/ee_manager_distributed.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -131,27 +131,32 @@ std::string getTheoryString(theory::TheoryId id)
 }
 
 void TheoryEngine::finishInit() {
-  // initialize the quantifiers engine
-  if (d_logicInfo.isQuantified())
+  // NOTE: This seems to be required since
+  // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
+  // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
+  std::vector<theory::Theory*> paraTheories;
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)   \
+  if (theory::TheoryTraits<THEORY>::isParametric \
+      && d_logicInfo.isTheoryEnabled(THEORY))    \
+  {                                              \
+    paraTheories.push_back(theoryOf(THEORY));    \
+  }
+  // Collect the parametric theories, which are given to the theory combination
+  // manager below
+  CVC4_FOR_EACH_THEORY;
+
+  // Initialize the theory combination architecture
+  if (options::tcMode() == options::TcMode::CARE_GRAPH)
   {
-    // initialize the quantifiers engine
-    d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+    d_tc.reset(new CombinationCareGraph(*this, paraTheories));
   }
-
-  // Initialize the equality engine architecture for all theories, which
-  // includes the master equality engine.
-  d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
-  d_eeDistributed->initializeTheories();
-
-  // Initialize the model and model builder.
-  if (d_logicInfo.isQuantified())
+  else
   {
-    d_curr_model_builder = d_quantEngine->getModelBuilder();
-    d_curr_model = d_quantEngine->getModel();
-  } else {
-    d_curr_model = new theory::TheoryModel(
-        d_userContext, "DefaultModel", options::assignFunctionValues());
-    d_aloc_curr_model = true;
+    Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
+                    << options::tcMode() << " not supported";
   }
   // create the relevance filter if any option requires it
   if (options::relevanceFilter())
@@ -160,24 +165,24 @@ void TheoryEngine::finishInit() {
         new RelevanceManager(d_userContext, theory::Valuation(this)));
   }
 
-  //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
-  if( d_curr_model_builder==NULL ){
-    d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
-    d_aloc_curr_model_builder = true;
+  // initialize the quantifiers engine
+  if (d_logicInfo.isQuantified())
+  {
+    // initialize the quantifiers engine
+    d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
   }
-
-  // Initialize the model
-  // !!!! temporary, will be part of combination engine initialization
-  d_eeDistributed->initializeModel(d_curr_model, nullptr);
+  // initialize the theory combination manager, which decides and allocates the
+  // equality engines to use for all theories.
+  d_tc->finishInit();
 
   // set the core equality engine on quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->setMasterEqualityEngine(
-        d_eeDistributed->getCoreEqualityEngine());
+    d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
   }
 
-  // finish initializing the theories
+  // finish initializing the theories by linking them with the appropriate
+  // utilities and then calling their finishInit method.
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     Theory* t = d_theoryTable[theoryId];
     if (t == nullptr)
@@ -185,7 +190,7 @@ void TheoryEngine::finishInit() {
       continue;
     }
     // setup the pointers to the utilities
-    const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
+    const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
     Assert(eeti != nullptr);
     // the theory's official equality engine is the one specified by the
     // equality engine manager
@@ -209,14 +214,12 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_userContext(userContext),
       d_logicInfo(logicInfo),
       d_sharedTerms(this, context),
-      d_eeDistributed(nullptr),
+      d_tc(nullptr),
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(userContext)),
       d_relManager(nullptr),
-      d_curr_model(nullptr),
-      d_aloc_curr_model(false),
-      d_curr_model_builder(nullptr),
-      d_aloc_curr_model_builder(false),
+      d_preRegistrationVisitor(this, context),
+      d_sharedTermsVisitor(d_sharedTerms),
       d_eager_model_building(false),
       d_possiblePropagations(context),
       d_hasPropagated(context),
@@ -237,8 +240,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_resourceManager(rm),
       d_inPreregister(false),
       d_factsAsserted(context, false),
-      d_preRegistrationVisitor(this, context),
-      d_sharedTermsVisitor(d_sharedTerms),
       d_attr_handle(),
       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 {
@@ -270,13 +271,6 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
-  if( d_aloc_curr_model_builder ){
-    delete d_curr_model_builder;
-  }
-  if( d_aloc_curr_model ){
-    delete d_curr_model;
-  }
-
   delete d_quantEngine;
 
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
@@ -311,34 +305,46 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
       Assert(!expr::hasFreeVar(preprocessed));
+
       // Pre-register the terms in the atom
-      Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+      Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(
+          d_preRegistrationVisitor, preprocessed);
       theories = Theory::setRemove(THEORY_BOOL, theories);
-      // Remove the top theory, if any more that means multiple theories were involved
+      // Remove the top theory, if any more that means multiple theories were
+      // involved
       bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
-      TheoryId i;
-      // These checks don't work with finite model finding, because it
-      // uses Rational constants to represent cardinality constraints,
-      // even though arithmetic isn't actually involved.
-      if(!options::finiteModelFind()) {
-        while((i = Theory::setPop(theories)) != THEORY_LAST) {
-          if(!d_logicInfo.isTheoryEnabled(i)) {
-            LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
-            newLogicInfo.enableTheory(i);
-            newLogicInfo.lock();
-            stringstream ss;
-            ss << "The logic was specified as " << d_logicInfo.getLogicString()
-               << ", which doesn't include " << i
-               << ", but found a term in that theory." << endl
-               << "You might want to extend your logic to "
-               << newLogicInfo.getLogicString() << endl;
-            throw LogicException(ss.str());
+      if (Configuration::isAssertionBuild())
+      {
+        TheoryId i;
+        // This should never throw an exception, since theories should be
+        // guaranteed to be initialized.
+        // These checks don't work with finite model finding, because it
+        // uses Rational constants to represent cardinality constraints,
+        // even though arithmetic isn't actually involved.
+        if (!options::finiteModelFind())
+        {
+          while ((i = Theory::setPop(theories)) != THEORY_LAST)
+          {
+            if (!d_logicInfo.isTheoryEnabled(i))
+            {
+              LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
+              newLogicInfo.enableTheory(i);
+              newLogicInfo.lock();
+              std::stringstream ss;
+              ss << "The logic was specified as " << d_logicInfo.getLogicString()
+                << ", which doesn't include " << i
+                << ", but found a term in that theory." << std::endl
+                << "You might want to extend your logic to "
+                << newLogicInfo.getLogicString() << std::endl;
+              throw LogicException(ss.str());
+            }
           }
         }
       }
       if (multipleTheories) {
         // Collect the shared terms if there are multiple theories
-        NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+        NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor,
+                                             preprocessed);
       }
     }
 
@@ -444,14 +450,17 @@ void TheoryEngine::check(Theory::Effort effort) {
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
-       theoryOf(THEORY)->check(effort); \
-       if (d_inConflict) { \
-         Debug("conflict") << THEORY << " in conflict. " << std::endl; \
-         break; \
-       } \
-    }
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)                      \
+  if (theory::TheoryTraits<THEORY>::hasCheck                        \
+      && d_logicInfo.isTheoryEnabled(THEORY))                       \
+  {                                                                 \
+    theoryOf(THEORY)->check(effort);                                \
+    if (d_inConflict)                                               \
+    {                                                               \
+      Debug("conflict") << THEORY << " in conflict. " << std::endl; \
+      break;                                                        \
+    }                                                               \
+  }
 
   // Do the checking
   try {
@@ -474,6 +483,7 @@ void TheoryEngine::check(Theory::Effort effort) {
       {
         d_relManager->resetRound();
       }
+      d_tc->resetRound();
     }
 
     // Check until done
@@ -514,7 +524,10 @@ void TheoryEngine::check(Theory::Effort effort) {
       if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
-        combineTheories();
+        {
+          TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
+          d_tc->combineTheories();
+        }
         if(d_logicInfo.isQuantified()){
           d_quantEngine->notifyCombineTheories();
         }
@@ -527,21 +540,17 @@ void TheoryEngine::check(Theory::Effort effort) {
       if (Trace.isOn("theory::assertions-model")) {
         printAssertions("theory::assertions-model");
       }
+      // reset the model in the combination engine
+      d_tc->resetModel();
       //checks for theories requiring the model go at last call
-      d_curr_model->reset();
-      // !!! temporary, will be part of distributed model manager
-      context::Context* meec = d_eeDistributed->getModelEqualityEngineContext();
-      meec->pop();
-      meec->push();
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
         if( theoryId!=THEORY_QUANTIFIERS ){
           Theory* theory = d_theoryTable[theoryId];
           if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
             if( theory->needsCheckLastEffort() ){
-              if( !d_curr_model->isBuilt() ){
-                if( !d_curr_model_builder->buildModel(d_curr_model) ){
-                  break;
-                }
+              if (!d_tc->buildModel())
+              {
+                break;
               }
               theory->check(Theory::EFFORT_LAST_CALL);
             }
@@ -561,9 +570,9 @@ void TheoryEngine::check(Theory::Effort effort) {
         // are in "SAT mode". We build the model later only if the user asks
         // for it via getBuiltModel.
         d_inSatMode = true;
-        if (d_eager_model_building && !d_curr_model->isBuilt())
+        if (d_eager_model_building)
         {
-          d_curr_model_builder->buildModel(d_curr_model);
+          d_tc->buildModel();
         }
       }
     }
@@ -572,27 +581,9 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
-      // case where we are about to answer SAT, the master equality engine,
-      // if it exists, must be consistent.
-      eq::EqualityEngine* mee = d_eeDistributed->getCoreEqualityEngine();
-      if (mee != NULL)
-      {
-        AlwaysAssert(mee->consistent());
-      }
-      if (d_curr_model->isBuilt())
-      {
-        // model construction should always succeed unless lemmas were added
-        AlwaysAssert(d_curr_model->isBuiltSuccess());
-        if (options::produceModels())
-        {
-          // Do post-processing of model from the theories (used for THEORY_SEP
-          // to construct heap model)
-          postProcessModel(d_curr_model);
-          // also call the model builder's post-process model
-          d_curr_model_builder->postProcessModel(d_incomplete.get(),
-                                                 d_curr_model);
-        }
-      }
+      // Do post-processing of model from the theories (e.g. used for THEORY_SEP
+      // to construct heap model)
+      d_tc->postProcessModel(d_incomplete.get());
     }
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
@@ -605,80 +596,8 @@ void TheoryEngine::check(Theory::Effort effort) {
   }
 }
 
-void TheoryEngine::combineTheories() {
-
-  Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl;
-
-  TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
-
-  // Care graph we'll be building
-  CareGraph careGraph;
-
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
-    theoryOf(THEORY)->getCareGraph(&careGraph); \
-  }
-
-  // Call on each parametric theory to give us its care graph
-  CVC4_FOR_EACH_THEORY;
-
-  Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
-
-  // Now add splitters for the ones we are interested in
-  CareGraph::const_iterator care_it = careGraph.begin();
-  CareGraph::const_iterator care_it_end = careGraph.end();
-
-  for (; care_it != care_it_end; ++ care_it) {
-    const CarePair& carePair = *care_it;
-
-    Debug("combineTheories")
-        << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
-        << carePair.d_b << " from " << carePair.d_theory << endl;
-
-    Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst());
-    Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst());
-
-    // The equality in question (order for no repetition)
-    Node equality = carePair.d_a.eqNode(carePair.d_b);
-    // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
-    // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
-    //   (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
-    //   es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
-    //   es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
-    //   es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
-    //   es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
-    //   es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
-    //   es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
-    //    "Unexpected case") << endl;
-
-    // We need to split on it
-    Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-
-    lemma(equality.orNode(equality.notNode()),
-          RULE_INVALID,
-          false,
-          LemmaProperty::NONE,
-          carePair.d_theory);
-
-    // This code is supposed to force preference to follow what the theory models already have
-    // but it doesn't seem to make a big difference - need to explore more -Clark
-    // if (true) {
-    //   if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
-    Node e = ensureLiteral(equality);
-    d_propEngine->requirePhase(e, true);
-    //   }
-    //   else if (es == EQUALITY_FALSE_IN_MODEL) {
-    //     Node e = ensureLiteral(equality);
-    //     d_propEngine->requirePhase(e, false);
-    //   }
-    // }
-  }
-}
-
-void TheoryEngine::propagate(Theory::Effort effort) {
+void TheoryEngine::propagate(Theory::Effort effort)
+{
   // Reset the interrupt flag
   d_interrupted = false;
 
@@ -762,99 +681,37 @@ bool TheoryEngine::properConflict(TNode conflict) const {
   return true;
 }
 
-bool TheoryEngine::properPropagation(TNode lit) const {
-  if(!getPropEngine()->isSatLiteral(lit)) {
-    return false;
-  }
-  bool b;
-  return !getPropEngine()->hasValue(lit, b);
-}
-
-bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
-  // Explanation must be either a conjunction of true literals that have true SAT values already
-  // or a singled literal that has a true SAT value already.
-  if (expl.getKind() == kind::AND) {
-    for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
-      bool value;
-      if (!d_propEngine->hasValue(expl[i], value) || !value) {
-        return false;
-      }
-    }
-  } else {
-    bool value;
-    return d_propEngine->hasValue(expl, value) && value;
-  }
-  return true;
+TheoryModel* TheoryEngine::getModel()
+{
+  Assert(d_tc != nullptr);
+  TheoryModel* m = d_tc->getModel();
+  Assert(m != nullptr);
+  return m;
 }
 
-bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+TheoryModel* TheoryEngine::getBuiltModel()
 {
-  //have shared term engine collectModelInfo
-  //  d_sharedTerms.collectModelInfo( m );
-  // Consult each active theory to get all relevant information
-  // concerning the model.
-  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
-    if(d_logicInfo.isTheoryEnabled(theoryId)) {
-      Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
-      if (!d_theoryTable[theoryId]->collectModelInfo(m))
-      {
-        return false;
-      }
-    }
-  }
-  Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
-  // Get the Boolean variables
-  vector<TNode> boolVars;
-  d_propEngine->getBooleanVariables(boolVars);
-  vector<TNode>::iterator it, iend = boolVars.end();
-  bool hasValue, value;
-  for (it = boolVars.begin(); it != iend; ++it) {
-    TNode var = *it;
-    hasValue = d_propEngine->hasValue(var, value);
-    // TODO: Assert that hasValue is true?
-    if (!hasValue) {
-      Trace("model-builder-assertions")
-          << "    has no value : " << var << std::endl;
-      value = false;
-    }
-    Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
-    if (!m->assertPredicate(var, value))
-    {
-      return false;
-    }
+  Assert(d_tc != nullptr);
+  // If this method was called, we should be in SAT mode, and produceModels
+  // should be true.
+  AlwaysAssert(options::produceModels());
+  if (!d_inSatMode)
+  {
+    // not available, perhaps due to interuption.
+    return nullptr;
   }
-  return true;
-}
-
-void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
-  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
-    if(d_logicInfo.isTheoryEnabled(theoryId)) {
-      Trace("model-builder-debug") << "  PostProcessModel on theory: " << theoryId << endl;
-      d_theoryTable[theoryId]->postProcessModel( m );
-    }
+  // must build model at this point
+  if (!d_tc->buildModel())
+  {
+    return nullptr;
   }
+  return d_tc->getModel();
 }
 
-TheoryModel* TheoryEngine::getModel() {
-  return d_curr_model;
-}
-
-TheoryModel* TheoryEngine::getBuiltModel()
+bool TheoryEngine::buildModel()
 {
-  if (!d_curr_model->isBuilt())
-  {
-    // If this method was called, we should be in SAT mode, and produceModels
-    // should be true.
-    AlwaysAssert(options::produceModels());
-    if (!d_inSatMode)
-    {
-      // not available, perhaps due to interuption.
-      return nullptr;
-    }
-    // must build model at this point
-    d_curr_model_builder->buildModel(d_curr_model);
-  }
-  return d_curr_model;
+  Assert(d_tc != nullptr);
+  return d_tc->buildModel();
 }
 
 bool TheoryEngine::getSynthSolutions(
@@ -1209,7 +1066,6 @@ void TheoryEngine::assertFact(TNode literal)
   TNode atom = polarity ? literal : literal[0];
 
   if (d_logicInfo.isSharingEnabled()) {
-
     // If any shared terms, it's time to do sharing work
     if (d_sharedTerms.hasSharedTerms(atom)) {
       // Notify the theories the shared terms
@@ -1233,7 +1089,8 @@ void TheoryEngine::assertFact(TNode literal)
     if (atom.getKind() == kind::EQUAL) {
       // Assert it to the the owning theory
       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
-      // Shared terms manager will assert to interested theories directly, as the terms become shared
+      // Shared terms manager will assert to interested theories directly, as
+      // the terms become shared
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
 
       // Now, let's check for any atom triggers from lemmas
@@ -1259,7 +1116,6 @@ void TheoryEngine::assertFact(TNode literal)
 }
 
 bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
-
   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
 
   Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
@@ -1821,11 +1677,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     });
 }
 
-SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
-{
-  return &d_sharedTerms;
-}
-
 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
   Assert(explanationVector.size() > 0);
 
@@ -2048,7 +1899,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
           // not relevant, skip
           continue;
         }
-        Node val = getModel()->getValue(assertion);
+        Node val = d_tc->getModel()->getValue(assertion);
         if (val != d_true)
         {
           std::stringstream ss;