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.

7 files changed, 164 insertions, 401 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9dc483f93..dd59628c1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -670,23 +670,15 @@ void QuantifiersEngine::check( Theory::Effort e ){
       QuantifiersModule::QEffort quant_e =
           static_cast<QuantifiersModule::QEffort>(qef);
       d_curr_effort_level = quant_e;
-      //build the model if any module requested it
+      // Force the theory engine to build the model if any module requested it.
       if (needsModelE == quant_e)
       {
-        if (!d_model->isBuilt())
-        {
-          // theory engine's model builder is quantifier engine's builder if it
-          // has one
-          Assert(!getModelBuilder()
-                 || getModelBuilder() == d_te->getModelBuilder());
-          Trace("quant-engine-debug") << "Build model..." << std::endl;
-          if (!d_te->getModelBuilder()->buildModel(d_model.get()))
-          {
-            flushLemmas();
-          }
-        }
-        if (!d_model->isBuiltSuccess())
+        Trace("quant-engine-debug") << "Build model..." << std::endl;
+        if (!d_te->buildModel())
         {
+          // If we failed to build the model, flush all pending lemmas and
+          // finish.
+          flushLemmas();
           break;
         }
       }
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;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ff4c3bdf9..61ee30bc8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -38,7 +38,6 @@
 #include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
 #include "theory/sort_inference.h"
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
@@ -87,11 +86,8 @@ struct NodeTheoryPairHashFunction {
 
 /* Forward declarations */
 namespace theory {
-class CombinationEngine;
 class TheoryModel;
-class TheoryEngineModelBuilder;
-class EqEngineManagerDistributed;
-
+class CombinationEngine;
 class DecisionManager;
 class RelevanceManager;
 
@@ -122,6 +118,7 @@ class TheoryEngine {
   friend class theory::CombinationEngine;
   friend class theory::quantifiers::TermDb;
   friend class theory::EngineOutputChannel;
+  friend class theory::CombinationEngine;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
@@ -152,15 +149,8 @@ class TheoryEngine {
    */
   SharedTermsDatabase d_sharedTerms;
 
-  /**
-   * The distributed equality manager. This class is responsible for
-   * configuring the theories of this class for handling equalties
-   * in a "distributed" fashion, i.e. each theory maintains a unique
-   * instance of an equality engine. These equality engines are memory
-   * managed by this class.
-   */
-  std::unique_ptr<theory::EqEngineManagerDistributed> d_eeDistributed;
-
+  /** The combination manager we are using */
+  std::unique_ptr<theory::CombinationEngine> d_tc;
   /**
    * The quantifiers engine
    */
@@ -172,16 +162,12 @@ class TheoryEngine {
   /** The relevance manager */
   std::unique_ptr<theory::RelevanceManager> d_relManager;
 
-  /**
-   * Default model object
-   */
-  theory::TheoryModel* d_curr_model;
-  bool d_aloc_curr_model;
-  /**
-   * Model builder object
-   */
-  theory::TheoryEngineModelBuilder* d_curr_model_builder;
-  bool d_aloc_curr_model_builder;
+  /** Default visitor for pre-registration */
+  PreRegisterVisitor d_preRegistrationVisitor;
+
+  /** Visitor for collecting shared terms */
+  SharedTermsVisitor d_sharedTermsVisitor;
+
   /** are we in eager model building mode? (see setEagerModelBuilding). */
   bool d_eager_model_building;
 
@@ -242,7 +228,6 @@ class TheoryEngine {
     d_incomplete = true;
   }
 
-
   /**
    * Mapping of propagations from recievers to senders.
    */
@@ -428,11 +413,6 @@ class TheoryEngine {
   context::CDO<bool> d_factsAsserted;
 
   /**
-   * Map from equality atoms to theories that would like to be notified about them.
-   */
-
-
-  /**
    * Assert the formula to the given theory.
    * @param assertion the assertion to send (not necesserily normalized)
    * @param original the assertion as it was sent in from the propagating theory
@@ -466,8 +446,7 @@ class TheoryEngine {
    */
   void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
 
-public:
-
+ public:
   /**
    * Signal the start of a new round of assertion preprocessing
    */
@@ -510,7 +489,6 @@ public:
    * or during LAST_CALL effort.
    */
   bool isRelevant(Node lit) const;
-
   /**
    * This is called at shutdown time by the SmtEngine, just before
    * destruction.  It is important because there are destruction
@@ -543,11 +521,6 @@ public:
   void check(theory::Theory::Effort effort);
 
   /**
-   * Run the combination framework.
-   */
-  void combineTheories();
-
-  /**
    * Calls ppStaticLearn() on all theories, accumulating their
    * combined contributions in the "learned" builder.
    */
@@ -585,8 +558,6 @@ public:
   Node getNextDecisionRequest();
 
   bool properConflict(TNode conflict) const;
-  bool properPropagation(TNode lit) const;
-  bool properExplanation(TNode node, TNode expl) const;
 
   /**
    * Returns an explanation of the node propagated to the SAT solver.
@@ -600,13 +571,6 @@ public:
   Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
 
   /**
-   * collect model info
-   */
-  bool collectModelInfo(theory::TheoryModel* m);
-  /** post process model */
-  void postProcessModel( theory::TheoryModel* m );
-
-  /**
    * Get the pointer to the model object used by this theory engine.
    */
   theory::TheoryModel* getModel();
@@ -622,6 +586,15 @@ public:
    * was interrupted), then this returns the null pointer.
    */
   theory::TheoryModel* getBuiltModel();
+  /**
+   * This forces the model maintained by the combination engine to be built
+   * if it has not been done so already. This should be called only during a
+   * last call effort check after theory combination is run.
+   *
+   * @return true if the model was successfully built (possibly prior to this
+   * call).
+   */
+  bool buildModel();
   /** set eager model building
    *
    * If this method is called, then this TheoryEngine will henceforth build
@@ -650,11 +623,6 @@ public:
   bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 
   /**
-   * Get the model builder
-   */
-  theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; }
-
-  /**
    * Get the theory associated to a given Node.
    *
    * @returns the theory, or NULL if the TNode is
@@ -735,11 +703,6 @@ public:
   std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 
  private:
-  /** Default visitor for pre-registration */
-  PreRegisterVisitor d_preRegistrationVisitor;
-
-  /** Visitor for collecting shared terms */
-  SharedTermsVisitor d_sharedTermsVisitor;
 
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
@@ -747,8 +710,6 @@ public:
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
 public:
 
-  SharedTermsDatabase* getSharedTermsDatabase();
-
   SortInference* getSortInference() { return &d_sortInfer; }
 
   /** Prints the assertions to the debug stream */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 725a932a2..31b44aa70 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -75,8 +75,6 @@ void TheoryModel::finishInit()
 }
 
 void TheoryModel::reset(){
-  d_modelBuilt = false;
-  d_modelBuiltSuccess = false;
   d_modelCache.clear();
   d_comment_str.clear();
   d_sep_heap = Node::null();
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index f465cec88..b725cfa09 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -95,21 +95,6 @@ public:
 
   /** reset the model */
   virtual void reset();
-  /** is built
-   *
-   * Have we attempted to build this model since the last
-   * call to reset? Notice for model building techniques
-   * that are not guaranteed to succeed (such as
-   * when quantified formulas are enabled), a true return
-   * value does not imply that this is a model of the
-   * current assertions.
-   */
-  bool isBuilt() { return d_modelBuilt; }
-  /** is built success
-   *
-   * Was this model successfully built since the last call to reset?
-   */
-  bool isBuiltSuccess() { return d_modelBuiltSuccess; }
   //---------------------------- for building the model
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
@@ -363,10 +348,6 @@ public:
   std::string d_name;
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
-  /** whether we have tried to build this model in the current context */
-  bool d_modelBuilt;
-  /** whether this model has been built successfully */
-  bool d_modelBuiltSuccess;
   /** equality engine containing all known equalities/disequalities */
   eq::EqualityEngine* d_equalityEngine;
   /** approximations (see recordApproximation) */
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index c82486bdd..31ba60be1 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -372,32 +372,11 @@ void TheoryEngineModelBuilder::addToTypeList(
   }
 }
 
-bool TheoryEngineModelBuilder::buildModel(Model* m)
+bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
 {
   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
-  TheoryModel* tm = (TheoryModel*)m;
   eq::EqualityEngine* ee = tm->d_equalityEngine;
 
-  // buildModel should only be called once per check
-  Assert(!tm->isBuilt());
-
-  // Reset model
-  tm->reset();
-
-  // mark as built
-  tm->d_modelBuilt = true;
-  tm->d_modelBuiltSuccess = false;
-
-  // Collect model info from the theories
-  Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
-                         << std::endl;
-  if (!d_te->collectModelInfo(tm))
-  {
-    Trace("model-builder")
-        << "TheoryEngineModelBuilder: fail collect model info" << std::endl;
-    return false;
-  }
-
   Trace("model-builder")
       << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
   // model-builder specific initialization
@@ -943,7 +922,6 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     return false;
   }
   Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
-  tm->d_modelBuiltSuccess = true;
   return true;
 }
 void TheoryEngineModelBuilder::computeAssignableInfo(
@@ -1124,7 +1102,6 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
 {
 #ifdef CVC4_ASSERTIONS
-  Assert(tm->isBuilt());
   if (tm->hasApproximations())
   {
     // models with approximations may fail the assertions below
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 0be92c95c..898ca7dbc 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -46,19 +46,22 @@ class TheoryEngineModelBuilder
  public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder() {}
-  /** Build model function.
-   *
-   * Should be called only on TheoryModels m.
+  /**
+   * Should be called only on models m after they have been prepared
+   * (e.g. using ModelManager). In other words, the equality engine of model
+   * m contains all relevant information from each theory that is needed
+   * for building a model. This class is responsible simply for ensuring
+   * that all equivalence classes of the equality engine of m are assigned
+   * constants.
    *
    * This constructs the model m, via the following steps:
-   * (1) call TheoryEngine::collectModelInfo,
-   * (2) builder-specified pre-processing,
-   * (3) find the equivalence classes of m's
+   * (1) builder-specified pre-processing,
+   * (2) find the equivalence classes of m's
    *     equality engine that initially contain constants,
-   * (4) assign constants to all equivalence classes
+   * (3) assign constants to all equivalence classes
    *     of m's equality engine, through alternating
    *     iterations of evaluation and enumeration,
-   * (5) builder-specific processing, which includes assigning total
+   * (4) builder-specific processing, which includes assigning total
    *     interpretations to uninterpreted functions.
    *
    * This function returns false if any of the above
@@ -67,7 +70,7 @@ class TheoryEngineModelBuilder
    * builder in steps (2) or (5), for instance, if the model we
    * are building fails to satisfy a quantified formula.
    */
-  bool buildModel(Model* m);
+  bool buildModel(TheoryModel* m);
 
   /** postprocess model
    *