Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout. 

1 files changed, 48 insertions, 28 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a88db4494..07c160058 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,6 +42,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/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"
@@ -129,20 +130,21 @@ std::string getTheoryString(theory::TheoryId id)
 }
 
 void TheoryEngine::finishInit() {
-  //initialize the quantifiers engine, master equality engine, model, model builder
-  if( d_logicInfo.isQuantified() ) {
+  // initialize the quantifiers engine
+  if (d_logicInfo.isQuantified())
+  {
     // initialize the quantifiers engine
     d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
-    Assert(d_masterEqualityEngine == 0);
-    d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
+  }
 
-    for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
-      if (d_theoryTable[theoryId]) {
-        d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine);
-        d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
-      }
-    }
+  // Initialize the equality engine architecture for all theories, which
+  // includes the master equality engine.
+  d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
+  d_eeDistributed->finishInit();
 
+  // Initialize the model and model builder.
+  if (d_logicInfo.isQuantified())
+  {
     d_curr_model_builder = d_quantEngine->getModelBuilder();
     d_curr_model = d_quantEngine->getModel();
   } else {
@@ -150,25 +152,32 @@ void TheoryEngine::finishInit() {
         d_userContext, "DefaultModel", options::assignFunctionValues());
     d_aloc_curr_model = true;
   }
+
   //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;
   }
 
+  // finish initializing the theories
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
-    if (d_theoryTable[theoryId]) {
-      // set the decision manager for the theory
-      d_theoryTable[theoryId]->setDecisionManager(d_decManager.get());
-      // finish initializing the theory
-      d_theoryTable[theoryId]->finishInit();
+    Theory* t = d_theoryTable[theoryId];
+    if (t == nullptr)
+    {
+      continue;
     }
-  }
-}
-
-void TheoryEngine::eqNotifyNewClass(TNode t){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyNewClass( t );
+    // setup the pointers to the utilities
+    const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
+    Assert(eeti != nullptr);
+    // the theory's official equality engine is the one specified by the
+    // equality engine manager
+    t->setEqualityEngine(eeti->d_usedEe);
+    // set the quantifiers engine
+    t->setQuantifiersEngine(d_quantEngine);
+    // set the decision manager for the theory
+    t->setDecisionManager(d_decManager.get());
+    // finish initializing the theory
+    t->finishInit();
   }
 }
 
@@ -182,8 +191,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_userContext(userContext),
       d_logicInfo(logicInfo),
       d_sharedTerms(this, context),
-      d_masterEqualityEngine(nullptr),
-      d_masterEENotify(*this),
+      d_eeDistributed(nullptr),
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(userContext)),
       d_curr_model(nullptr),
@@ -252,8 +260,6 @@ TheoryEngine::~TheoryEngine() {
 
   delete d_quantEngine;
 
-  delete d_masterEqualityEngine;
-
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }
@@ -537,9 +543,12 @@ 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
-      if( d_masterEqualityEngine != NULL ){
-        AlwaysAssert(d_masterEqualityEngine->consistent());
+      // case where we are about to answer SAT, the master equality engine,
+      // if it exists, must be consistent.
+      eq::EqualityEngine* mee = getMasterEqualityEngine();
+      if (mee != NULL)
+      {
+        AlwaysAssert(mee->consistent());
       }
       if (d_curr_model->isBuilt())
       {
@@ -1793,6 +1802,17 @@ void TheoryEngine::staticInitializeBVOptions(
   }
 }
 
+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);