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. 

2 files changed, 68 insertions, 46 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 862a906a0..4f9c3bed5 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -54,16 +54,12 @@ TheoryUF::TheoryUF(context::Context* c,
        * so make sure it's initialized first. */
       d_thss(nullptr),
       d_ho(nullptr),
-      d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
       d_conflict(c, false),
       d_functionsTerms(c),
       d_symb(u, instanceName)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
 
-  // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
-
   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
   if (pc != nullptr)
   {
@@ -74,11 +70,17 @@ TheoryUF::TheoryUF(context::Context* c,
 TheoryUF::~TheoryUF() {
 }
 
-void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = d_instanceName + "theory::uf::ee";
+  return true;
 }
 
 void TheoryUF::finishInit() {
+  Assert(d_equalityEngine != nullptr);
   // combined cardinality constraints are not evaluated in getModelValue
   d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
   // Initialize the cardinality constraints solver if the logic includes UF,
@@ -90,9 +92,11 @@ void TheoryUF::finishInit() {
     d_thss.reset(new CardinalityExtension(
         getSatContext(), getUserContext(), *d_out, this));
   }
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
   if (options::ufHo())
   {
-    d_equalityEngine.addFunctionKind(kind::HO_APPLY);
+    d_equalityEngine->addFunctionKind(kind::HO_APPLY);
     d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext()));
   }
 }
@@ -148,7 +152,7 @@ void TheoryUF::check(Effort level) {
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
-      d_equalityEngine.assertEquality(atom, polarity, fact);
+      d_equalityEngine->assertEquality(atom, polarity, fact);
       if( options::ufHo() && options::ufHoExt() ){
         if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
           // apply extensionality eagerly using the ho extension
@@ -169,10 +173,10 @@ void TheoryUF::check(Effort level) {
       }
       //needed for models
       if( options::produceModels() ){
-        d_equalityEngine.assertPredicate(atom, polarity, fact);
+        d_equalityEngine->assertPredicate(atom, polarity, fact);
       }
     } else {
-      d_equalityEngine.assertPredicate(atom, polarity, fact);
+      d_equalityEngine->assertPredicate(atom, polarity, fact);
     }
   }
 
@@ -198,7 +202,7 @@ Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
   if( node.getKind()==kind::APPLY_UF ){
     return node.getOperator();
   }else{
-    return d_equalityEngine.getRepresentative( node[0] );
+    return d_equalityEngine->getRepresentative(node[0]);
   }
 }
 
@@ -242,17 +246,17 @@ void TheoryUF::preRegisterTerm(TNode node) {
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
-    d_equalityEngine.addTriggerEquality(node);
+    d_equalityEngine->addTriggerEquality(node);
     break;
   case kind::APPLY_UF:
   case kind::HO_APPLY:
     // Maybe it's a predicate
     if (node.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
-      d_equalityEngine.addTriggerPredicate(node);
+      d_equalityEngine->addTriggerPredicate(node);
     } else {
       // Function applications/predicates
-      d_equalityEngine.addTerm(node);
+      d_equalityEngine->addTerm(node);
     }
     // Remember the function and predicate terms
     d_functionsTerms.push_back(node);
@@ -263,7 +267,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
     break;
   default:
     // Variables etc
-    d_equalityEngine.addTerm(node);
+    d_equalityEngine->addTerm(node);
     break;
   }
 }/* TheoryUF::preRegisterTerm() */
@@ -294,9 +298,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   if (atom.getKind() == kind::EQUAL) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
+    d_equalityEngine->explainEquality(
+        atom[0], atom[1], polarity, assumptions, pf);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
+    d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf);
   }
   if( pf ){
     Debug("pf::uf") << std::endl;
@@ -331,7 +336,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
 
-  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
     Trace("uf") << "Collect model info fail UF" << std::endl;
     return false;
@@ -495,13 +500,15 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
   // Check for equality (simplest)
-  if (d_equalityEngine.areEqual(a, b)) {
+  if (d_equalityEngine->areEqual(a, b))
+  {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
 
   // Check for disequality
-  if (d_equalityEngine.areDisequal(a, b, false)) {
+  if (d_equalityEngine->areDisequal(a, b, false))
+  {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
@@ -512,15 +519,19 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
 void TheoryUF::addSharedTerm(TNode t) {
   Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_UF);
+  d_equalityEngine->addTriggerTerm(t, THEORY_UF);
 }
 
 bool TheoryUF::areCareDisequal(TNode x, TNode y){
-  Assert(d_equalityEngine.hasTerm(x));
-  Assert(d_equalityEngine.hasTerm(y));
-  if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
-    TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
-    TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+  Assert(d_equalityEngine->hasTerm(x));
+  Assert(d_equalityEngine->hasTerm(y));
+  if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+      && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+  {
+    TNode x_shared =
+        d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+    TNode y_shared =
+        d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
     EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
     if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
       return true;
@@ -538,21 +549,27 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
     if( t2!=NULL ){
       Node f1 = t1->getData();
       Node f2 = t2->getData();
-      if( !d_equalityEngine.areEqual( f1, f2 ) ){
+      if (!d_equalityEngine->areEqual(f1, f2))
+      {
         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
         unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
         for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
           TNode x = f1[k];
           TNode y = f2[k];
-          Assert(d_equalityEngine.hasTerm(x));
-          Assert(d_equalityEngine.hasTerm(y));
-          Assert(!d_equalityEngine.areDisequal(x, y, false));
+          Assert(d_equalityEngine->hasTerm(x));
+          Assert(d_equalityEngine->hasTerm(y));
+          Assert(!d_equalityEngine->areDisequal(x, y, false));
           Assert(!areCareDisequal(x, y));
-          if( !d_equalityEngine.areEqual( x, y ) ){
-            if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
-              TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
-              TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+          if (!d_equalityEngine->areEqual(x, y))
+          {
+            if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
+                && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
+            {
+              TNode x_shared =
+                  d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
+              TNode y_shared =
+                  d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
               currentPairs.push_back(make_pair(x_shared, y_shared));
             }
           }
@@ -580,7 +597,8 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
         std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+          {
             if( !areCareDisequal(it->first, it2->first) ){
               addCarePairs( &it->second, &it2->second, arity, depth+1 );
             }
@@ -593,7 +611,7 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
       {
         for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
         {
-          if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
           {
             if (!areCareDisequal(tt1.first, tt2.first))
             {
@@ -621,8 +639,9 @@ void TheoryUF::computeCareGraph() {
       std::vector< TNode > reps;
       bool has_trigger_arg = false;
       for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
-        reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
-        if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
+        reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+        if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_UF))
+        {
           has_trigger_arg = true;
         }
       }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 345547301..001c947e9 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -116,9 +116,6 @@ private:
   /** the higher-order solver extension (or nullptr if it does not exist) */
   std::unique_ptr<HoExtension> d_ho;
 
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
-
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
 
@@ -186,10 +183,18 @@ private:
 
   ~TheoryUF();
 
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
   void finishInit() override;
+  //--------------------------------- end initialization
 
   void check(Effort) override;
   TrustNode expandDefinition(Node node) override;
@@ -210,8 +215,6 @@ private:
 
   std::string identify() const override { return "THEORY_UF"; }
 
-  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
   /** get a pointer to the uf with cardinality */
   CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
   /** are we in conflict? */