Quantifiers engine stores a pointer to the master equality engine (#4908)

This is work towards a configurable approach to theory combination.

Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.

1 files changed, 8 insertions, 7 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 07c160058..e86a09112 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -159,6 +159,13 @@ void TheoryEngine::finishInit() {
     d_aloc_curr_model_builder = true;
   }
 
+  // set the core equality engine on quantifiers engine
+  if (d_logicInfo.isQuantified())
+  {
+    d_quantEngine->setMasterEqualityEngine(
+        d_eeDistributed->getMasterEqualityEngine());
+  }
+
   // finish initializing the theories
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     Theory* t = d_theoryTable[theoryId];
@@ -545,7 +552,7 @@ void TheoryEngine::check(Theory::Effort effort) {
     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 = getMasterEqualityEngine();
+      eq::EqualityEngine* mee = d_eeDistributed->getMasterEqualityEngine();
       if (mee != NULL)
       {
         AlwaysAssert(mee->consistent());
@@ -1807,12 +1814,6 @@ SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
   return &d_sharedTerms;
 }
 
-theory::eq::EqualityEngine* TheoryEngine::getMasterEqualityEngine()
-{
-  Assert(d_eeDistributed != nullptr);
-  return d_eeDistributed->getMasterEqualityEngine();
-}
-
 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
   Assert(explanationVector.size() > 0);