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, 51 insertions, 35 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 4dfdb9fa5..edb5dd0ae 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -48,7 +48,6 @@ TheorySep::TheorySep(context::Context* c,
     : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
       d_lemmas_produced_c(u),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, "theory::sep::ee", true),
       d_conflict(c, false),
       d_reduce(u),
       d_infer(c),
@@ -58,10 +57,6 @@ TheorySep::TheorySep(context::Context* c,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
   d_bounds_init = false;
-  
-  // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::SEP_PTO);
-  //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
 }
 
 TheorySep::~TheorySep() {
@@ -70,8 +65,21 @@ TheorySep::~TheorySep() {
   }
 }
 
-void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = "theory::sep::ee";
+  return true;
+}
+
+void TheorySep::finishInit()
+{
+  Assert(d_equalityEngine != nullptr);
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine->addFunctionKind(kind::SEP_PTO);
+  // we could but don't do congruence on SEP_STAR here.
 }
 
 Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
@@ -126,9 +134,10 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
     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, NULL );
+      d_equalityEngine->explainEquality(
+          atom[0], atom[1], polarity, assumptions, NULL);
     } else {
-      d_equalityEngine.explainPredicate( atom, polarity, assumptions );
+      d_equalityEngine->explainPredicate(atom, polarity, assumptions);
     }
   }
 }
@@ -155,17 +164,19 @@ TrustNode TheorySep::explain(TNode literal)
 
 void TheorySep::addSharedTerm(TNode t) {
   Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_SEP);
+  d_equalityEngine->addTriggerTerm(t, THEORY_SEP);
 }
 
 
 EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) {
-  Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
-  if (d_equalityEngine.areEqual(a, b)) {
+  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+  if (d_equalityEngine->areEqual(a, b))
+  {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
-  else if (d_equalityEngine.areDisequal(a, b, false)) {
+  else if (d_equalityEngine->areDisequal(a, b, false))
+  {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
@@ -211,7 +222,7 @@ bool TheorySep::collectModelInfo(TheoryModel* m)
   computeRelevantTerms(termSet);
 
   // Send the equality engine information to the model
-  return m->assertEqualityEngine(&d_equalityEngine, &termSet);
+  return m->assertEqualityEngine(d_equalityEngine, &termSet);
 }
 
 void TheorySep::postProcessModel( TheoryModel* m ){
@@ -490,16 +501,16 @@ void TheorySep::check(Effort e) {
       if( !is_spatial ){
         Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl;
         if( s_atom.getKind()==kind::EQUAL ){
-          d_equalityEngine.assertEquality(atom, polarity, fact);
+          d_equalityEngine->assertEquality(atom, polarity, fact);
         }else{
-          d_equalityEngine.assertPredicate(atom, polarity, fact);
+          d_equalityEngine->assertPredicate(atom, polarity, fact);
         }
         Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl;
       }else if( s_atom.getKind()==kind::SEP_PTO ){
         Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
         Assert(s_lbl == pto_lbl);
         Trace("sep-assert") << "Asserting " << s_atom << std::endl;
-        d_equalityEngine.assertPredicate(s_atom, polarity, fact);
+        d_equalityEngine->assertPredicate(s_atom, polarity, fact);
         //associate the equivalence class of the lhs with this pto
         Node r = getRepresentative( s_lbl );
         HeapAssertInfo * ei = getOrMakeEqcInfo( r, true );
@@ -619,11 +630,11 @@ void TheorySep::check(Effort e) {
       Trace("sep-process") << "---" << std::endl;
     }
     if(Trace.isOn("sep-eqc")) {
-      eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
+      eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
       Trace("sep-eqc") << "EQC:" << std::endl;
       while( !eqcs2_i.isFinished() ){
         Node eqc = (*eqcs2_i);
-        eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+        eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
         Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
         while( !eqc2_i.isFinished() ) {
           if( (*eqc2_i)!=eqc ){
@@ -1552,22 +1563,21 @@ void TheorySep::computeLabelModel( Node lbl ) {
 }
 
 Node TheorySep::getRepresentative( Node t ) {
-  if( d_equalityEngine.hasTerm( t ) ){
-    return d_equalityEngine.getRepresentative( t );
+  if (d_equalityEngine->hasTerm(t))
+  {
+    return d_equalityEngine->getRepresentative(t);
   }else{
     return t;
   }
 }
 
-bool TheorySep::hasTerm( Node a ){
-  return d_equalityEngine.hasTerm( a );
-}
+bool TheorySep::hasTerm(Node a) { return d_equalityEngine->hasTerm(a); }
 
 bool TheorySep::areEqual( Node a, Node b ){
   if( a==b ){
     return true;
   }else if( hasTerm( a ) && hasTerm( b ) ){
-    return d_equalityEngine.areEqual( a, b );
+    return d_equalityEngine->areEqual(a, b);
   }else{
     return false;
   }
@@ -1577,7 +1587,8 @@ bool TheorySep::areDisequal( Node a, Node b ){
   if( a==b ){
     return false;
   }else if( hasTerm( a ) && hasTerm( b ) ){
-    if( d_equalityEngine.areDisequal( a, b, false ) ){
+    if (d_equalityEngine->areDisequal(a, b, false))
+    {
       return true;
     }
   }
@@ -1743,9 +1754,9 @@ void TheorySep::doPendingFacts() {
       bool pol = d_pending[i].getKind()!=kind::NOT;
       Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
       if( atom.getKind()==kind::EQUAL ){
-        d_equalityEngine.assertEquality(atom, pol, d_pending_exp[i]);
+        d_equalityEngine->assertEquality(atom, pol, d_pending_exp[i]);
       }else{
-        d_equalityEngine.assertPredicate(atom, pol, d_pending_exp[i]);
+        d_equalityEngine->assertPredicate(atom, pol, d_pending_exp[i]);
       }
     }
   }else{
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 7c6ce38c4..84a7025f0 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -74,9 +74,18 @@ class TheorySep : public Theory {
             ProofNodeManager* pnm = nullptr);
   ~TheorySep();
 
-  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
 
   std::string identify() const override { return std::string("TheorySep"); }
 
@@ -202,9 +211,6 @@ class TheorySep : public Theory {
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
-
   /** Are we in conflict? */
   context::CDO<bool> d_conflict;
   std::vector< Node > d_pending_exp;
@@ -326,7 +332,6 @@ class TheorySep : public Theory {
   void doPendingFacts();
 
  public:
-  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
   void initializeBounds();
 };/* class TheorySep */