Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.

1 files changed, 32 insertions, 38 deletions

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 3fb5fc0ce..496b04a52 100644
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -47,6 +47,19 @@ void EqEngineManagerDistributed::initializeTheories()
     Unhandled() << "Expected shared solver to use equality engine";
   }
 
+  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  if (logicInfo.isQuantified())
+  {
+    // construct the master equality engine
+    Assert(d_masterEqualityEngine == nullptr);
+    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
+    Assert(qe != nullptr);
+    d_masterEENotify.reset(new MasterNotifyClass(qe));
+    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
+                                                        d_te.getSatContext(),
+                                                        "theory::master",
+                                                        false));
+  }
   // allocate equality engines per theory
   for (TheoryId theoryId = theory::THEORY_FIRST;
        theoryId != theory::THEORY_LAST;
@@ -63,48 +76,34 @@ void EqEngineManagerDistributed::initializeTheories()
     EeSetupInfo esi;
     if (!t->needsEqualityEngine(esi))
     {
-      // theory said it doesn't need an equality engine, skip
+      // the theory said it doesn't need an equality engine, skip
+      continue;
+    }
+    if (esi.d_useMaster)
+    {
+      // the theory said it wants to use the master equality engine
+      eet.d_usedEe = d_masterEqualityEngine.get();
       continue;
     }
     // allocate the equality engine
     eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
     // the theory uses the equality engine
     eet.d_usedEe = eet.d_allocEe.get();
+    // if there is a master equality engine
+    if (d_masterEqualityEngine != nullptr)
+    {
+      // set the master equality engine of the theory's equality engine
+      eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get());
+    }
   }
+}
 
-  const LogicInfo& logicInfo = d_te.getLogicInfo();
-  if (logicInfo.isQuantified())
+void EqEngineManagerDistributed::notifyModel(bool incomplete)
+{
+  // should have a consistent master equality engine
+  if (d_masterEqualityEngine.get() != nullptr)
   {
-    // construct the master equality engine
-    Assert(d_masterEqualityEngine == nullptr);
-    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
-    Assert(qe != nullptr);
-    d_masterEENotify.reset(new MasterNotifyClass(qe));
-    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
-                                                        d_te.getSatContext(),
-                                                        "theory::master",
-                                                        false));
-
-    for (TheoryId theoryId = theory::THEORY_FIRST;
-         theoryId != theory::THEORY_LAST;
-         ++theoryId)
-    {
-      Theory* t = d_te.theoryOf(theoryId);
-      if (t == nullptr)
-      {
-        // theory not active, skip
-        continue;
-      }
-      EeTheoryInfo& eet = d_einfo[theoryId];
-      // Get the allocated equality engine, and connect it to the master
-      // equality engine.
-      eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
-      if (eeAlloc != nullptr)
-      {
-        // set the master equality engine of the theory's equality engine
-        eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
-      }
-    }
+    AlwaysAssert(d_masterEqualityEngine->consistent());
   }
 }
 
@@ -114,10 +113,5 @@ void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
   d_quantEngine->eqNotifyNewClass(t);
 }
 
-eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine()
-{
-  return d_masterEqualityEngine.get();
-}
-
 }  // namespace theory
 }  // namespace CVC4