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. 

6 files changed, 127 insertions, 100 deletions

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index a554ac595..8634478fd 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -27,11 +27,10 @@ namespace strings {
 
 SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
-                         eq::EqualityEngine& ee,
                          Valuation& v)
     : d_context(c),
       d_ucontext(u),
-      d_ee(ee),
+      d_ee(nullptr),
       d_eeDisequalities(c),
       d_valuation(v),
       d_conflict(c, false),
@@ -48,19 +47,25 @@ SolverState::~SolverState()
   }
 }
 
+void SolverState::finishInit(eq::EqualityEngine* ee)
+{
+  Assert(ee != nullptr);
+  d_ee = ee;
+}
+
 context::Context* SolverState::getSatContext() const { return d_context; }
 context::UserContext* SolverState::getUserContext() const { return d_ucontext; }
 
 Node SolverState::getRepresentative(Node t) const
 {
-  if (d_ee.hasTerm(t))
+  if (d_ee->hasTerm(t))
   {
-    return d_ee.getRepresentative(t);
+    return d_ee->getRepresentative(t);
   }
   return t;
 }
 
-bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); }
+bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); }
 
 bool SolverState::areEqual(Node a, Node b) const
 {
@@ -70,7 +75,7 @@ bool SolverState::areEqual(Node a, Node b) const
   }
   else if (hasTerm(a) && hasTerm(b))
   {
-    return d_ee.areEqual(a, b);
+    return d_ee->areEqual(a, b);
   }
   return false;
 }
@@ -83,17 +88,17 @@ bool SolverState::areDisequal(Node a, Node b) const
   }
   else if (hasTerm(a) && hasTerm(b))
   {
-    Node ar = d_ee.getRepresentative(a);
-    Node br = d_ee.getRepresentative(b);
+    Node ar = d_ee->getRepresentative(a);
+    Node br = d_ee->getRepresentative(b);
     return (ar != br && ar.isConst() && br.isConst())
-           || d_ee.areDisequal(ar, br, false);
+           || d_ee->areDisequal(ar, br, false);
   }
   Node ar = getRepresentative(a);
   Node br = getRepresentative(b);
   return ar != br && ar.isConst() && br.isConst();
 }
 
-eq::EqualityEngine* SolverState::getEqualityEngine() const { return &d_ee; }
+eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; }
 
 const context::CDList<Node>& SolverState::getDisequalityList() const
 {
@@ -105,7 +110,7 @@ void SolverState::eqNotifyNewClass(TNode t)
   Kind k = t.getKind();
   if (k == STRING_LENGTH || k == STRING_TO_CODE)
   {
-    Node r = d_ee.getRepresentative(t[0]);
+    Node r = d_ee->getRepresentative(t[0]);
     EqcInfo* ei = getOrMakeEqcInfo(r);
     if (k == STRING_LENGTH)
     {
@@ -317,14 +322,14 @@ void SolverState::separateByLength(
   NodeManager* nm = NodeManager::currentNM();
   for (const Node& eqc : n)
   {
-    Assert(d_ee.getRepresentative(eqc) == eqc);
+    Assert(d_ee->getRepresentative(eqc) == eqc);
     TypeNode tnEqc = eqc.getType();
     EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
     Node lt = ei ? ei->d_lengthTerm : Node::null();
     if (!lt.isNull())
     {
       lt = nm->mkNode(STRING_LENGTH, lt);
-      Node r = d_ee.getRepresentative(lt);
+      Node r = d_ee->getRepresentative(lt);
       std::pair<Node, TypeNode> lkey(r, tnEqc);
       if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
       {
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 8d3162b38..0322abdb7 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -46,9 +46,13 @@ class SolverState
  public:
   SolverState(context::Context* c,
               context::UserContext* u,
-              eq::EqualityEngine& ee,
               Valuation& v);
   ~SolverState();
+  /**
+   * Finish initialize, ee is a pointer to the official equality engine
+   * of theory of strings.
+   */
+  void finishInit(eq::EqualityEngine* ee);
   /** Get the SAT context */
   context::Context* getSatContext() const;
   /** Get the user context */
@@ -186,8 +190,8 @@ class SolverState
   context::Context* d_context;
   /** Pointer to the user context object used by the theory of strings. */
   context::UserContext* d_ucontext;
-  /** Reference to equality engine of the theory of strings. */
-  eq::EqualityEngine& d_ee;
+  /** Pointer to equality engine of the theory of strings. */
+  eq::EqualityEngine* d_ee;
   /**
    * The (SAT-context-dependent) list of disequalities that have been asserted
    * to the equality engine above.
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index f28db4c35..71b45915f 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -37,12 +37,10 @@ typedef expr::Attribute<StringsProxyVarAttributeId, bool>
     StringsProxyVarAttribute;
 
 TermRegistry::TermRegistry(SolverState& s,
-                           eq::EqualityEngine& ee,
                            OutputChannel& out,
                            SequencesStatistics& statistics,
                            ProofNodeManager* pnm)
     : d_state(s),
-      d_ee(ee),
       d_out(out),
       d_statistics(statistics),
       d_hasStrCode(false),
@@ -129,6 +127,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   {
     return;
   }
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
   d_preregisteredTerms.insert(n);
   Trace("strings-preregister")
       << "TheoryString::preregister : " << n << std::endl;
@@ -156,15 +155,15 @@ void TermRegistry::preRegisterTerm(TNode n)
       ss << "Equality between regular expressions is not supported";
       throw LogicException(ss.str());
     }
-    d_ee.addTriggerEquality(n);
+    ee->addTriggerEquality(n);
     return;
   }
   else if (k == STRING_IN_REGEXP)
   {
     d_out.requirePhase(n, true);
-    d_ee.addTriggerPredicate(n);
-    d_ee.addTerm(n[0]);
-    d_ee.addTerm(n[1]);
+    ee->addTriggerPredicate(n);
+    ee->addTerm(n[0]);
+    ee->addTerm(n[1]);
     return;
   }
   else if (k == STRING_TO_CODE)
@@ -196,17 +195,17 @@ void TermRegistry::preRegisterTerm(TNode n)
         }
       }
     }
-    d_ee.addTerm(n);
+    ee->addTerm(n);
   }
   else if (tn.isBoolean())
   {
     // Get triggered for both equal and dis-equal
-    d_ee.addTriggerPredicate(n);
+    ee->addTriggerPredicate(n);
   }
   else
   {
     // Function applications/predicates
-    d_ee.addTerm(n);
+    ee->addTerm(n);
   }
   // Set d_functionsTerms stores all function applications that are
   // relevant to theory combination. Notice that this is a subset of
@@ -216,7 +215,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   // Concatenation terms do not need to be considered here because
   // their arguments have string type and do not introduce any shared
   // terms.
-  if (n.hasOperator() && d_ee.isFunctionKind(k) && k != STRING_CONCAT)
+  if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
   {
     d_functionsTerms.push_back(n);
   }
@@ -313,7 +312,7 @@ void TermRegistry::registerType(TypeNode tn)
   {
     // preregister the empty word for the type
     Node emp = Word::mkEmptyWord(tn);
-    if (!d_ee.hasTerm(emp))
+    if (!d_state.hasTerm(emp))
     {
       preRegisterTerm(emp);
     }
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 2048abec1..45fb40073 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -50,7 +50,6 @@ class TermRegistry
 
  public:
   TermRegistry(SolverState& s,
-               eq::EqualityEngine& ee,
                OutputChannel& out,
                SequencesStatistics& statistics,
                ProofNodeManager* pnm);
@@ -220,8 +219,6 @@ class TermRegistry
   uint32_t d_cardSize;
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
-  /** Reference to equality engine of the theory of strings. */
-  eq::EqualityEngine& d_ee;
   /** Reference to the output channel of the theory of strings. */
   OutputChannel& d_out;
   /** Reference to the statistics for the theory of strings/sequences. */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0ad887d2f..b23765313 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -43,9 +43,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
       d_notify(*this),
       d_statistics(),
-      d_equalityEngine(d_notify, c, "theory::strings::ee", true),
-      d_state(c, u, d_equalityEngine, d_valuation),
-      d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
+      d_state(c, u, d_valuation),
+      d_termReg(d_state, out, d_statistics, nullptr),
       d_extTheory(this),
       d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
       d_rewriter(&d_statistics.d_rewrites),
@@ -67,30 +66,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
                 d_statistics),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
-  bool eagerEval = options::stringEagerEval();
-  // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::STRING_LENGTH, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_CONCAT, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::SEQ_UNIT, eagerEval);
-
-  // extended functions
-  d_equalityEngine.addFunctionKind(kind::STRING_STRCTN, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_LEQ, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_UPDATE, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_ITOS, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_STOI, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPL, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER, eagerEval);
-  d_equalityEngine.addFunctionKind(kind::STRING_REV, eagerEval);
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -113,26 +88,63 @@ TheoryStrings::~TheoryStrings() {
 }
 
 TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
-std::string TheoryStrings::identify() const
-{
-  return std::string("TheoryStrings");
-}
-eq::EqualityEngine* TheoryStrings::getEqualityEngine()
+
+bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
 {
-  return &d_equalityEngine;
+  esi.d_notify = &d_notify;
+  esi.d_name = "theory::strings::ee";
+  return true;
 }
+
 void TheoryStrings::finishInit()
 {
+  Assert(d_equalityEngine != nullptr);
+
   // witness is used to eliminate str.from_code
   d_valuation.setUnevaluatedKind(WITNESS);
+
+  bool eagerEval = options::stringEagerEval();
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval);
+  // extended functions
+  d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_SUBSTR, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_UPDATE, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_ITOS, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_STOI, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_STRIDOF, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_STRREPL, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval);
+  d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval);
+
+  d_state.finishInit(d_equalityEngine);
+}
+
+std::string TheoryStrings::identify() const
+{
+  return std::string("TheoryStrings");
 }
 
 bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
-  Assert(d_equalityEngine.hasTerm(x));
-  Assert(d_equalityEngine.hasTerm(y));
-  if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
-    TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
-    TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
+  Assert(d_equalityEngine->hasTerm(x));
+  Assert(d_equalityEngine->hasTerm(y));
+  if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
+      && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
+  {
+    TNode x_shared =
+        d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS);
+    TNode y_shared =
+        d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS);
     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;
@@ -141,14 +153,10 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   return false;
 }
 
-void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
-}
-
 void TheoryStrings::addSharedTerm(TNode t) {
   Debug("strings") << "TheoryStrings::addSharedTerm(): "
                      << t << " " << t.getType().isBoolean() << endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
+  d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS);
   if (options::stringExp())
   {
     d_esolver.addSharedTerm(t);
@@ -157,12 +165,15 @@ void TheoryStrings::addSharedTerm(TNode t) {
 }
 
 EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
-  if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
-    if (d_equalityEngine.areEqual(a, b)) {
+  if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
+  {
+    if (d_equalityEngine->areEqual(a, b))
+    {
       // The terms are implied to be equal
       return EQUALITY_TRUE;
     }
-    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;
     }
@@ -251,7 +262,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
   // assert the (relevant) portion of the equality engine to the model
-  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
     Unreachable()
         << "TheoryStrings::collectModelInfo: failed to assert equality engine"
@@ -670,14 +681,15 @@ void TheoryStrings::check(Effort e) {
         << "Theory of strings " << e << " effort check " << std::endl;
     if(Trace.isOn("strings-eqc")) {
       for( unsigned t=0; t<2; t++ ) {
-        eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
+        eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
         Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
         while( !eqcs2_i.isFinished() ){
           Node eqc = (*eqcs2_i);
           bool print = (t == 0 && eqc.getType().isStringLike())
                        || (t == 1 && !eqc.getType().isStringLike());
           if (print) {
-            eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+            eq::EqClassIterator eqc2_i =
+                eq::EqClassIterator(eqc, d_equalityEngine);
             Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
             while( !eqc2_i.isFinished() ) {
               if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){
@@ -779,20 +791,26 @@ void TheoryStrings::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))
+      {
         Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
         for (unsigned k = 0; 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_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
-              TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
-              TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
+          if (!d_equalityEngine->areEqual(x, y))
+          {
+            if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
+                && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
+            {
+              TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
+                  x, THEORY_STRINGS);
+              TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
+                  y, THEORY_STRINGS);
               currentPairs.push_back(make_pair(x_shared, y_shared));
             }
           }
@@ -820,7 +838,8 @@ void TheoryStrings::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 );
             }
@@ -833,7 +852,7 @@ void TheoryStrings::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))
             {
@@ -862,8 +881,9 @@ void TheoryStrings::computeCareGraph(){
     std::vector< TNode > reps;
     bool has_trigger_arg = false;
     for( unsigned j=0; j<f1.getNumChildren(); j++ ){
-      reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
-      if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_STRINGS ) ){
+      reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
+      if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_STRINGS))
+      {
         has_trigger_arg = true;
       }
     }
@@ -889,7 +909,7 @@ void TheoryStrings::checkRegisterTermsPreNormalForm()
   const std::vector<Node>& seqc = d_bsolver.getStringEqc();
   for (const Node& eqc : seqc)
   {
-    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
     while (!eqc_i.isFinished())
     {
       Node n = (*eqc_i);
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 2fb827429..500daac1f 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -70,20 +70,24 @@ class TheoryStrings : public Theory {
                 const LogicInfo& logicInfo,
                 ProofNodeManager* pnm);
   ~TheoryStrings();
+  //--------------------------------- 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;
-  /** Get the theory rewriter of this class */
-  TheoryRewriter* getTheoryRewriter() override;
-  /** Set the master equality engine */
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  //--------------------------------- end initialization
   /** Identify this theory */
   std::string identify() const override;
   /** Propagate */
   void propagate(Effort e) override;
   /** Explain */
   TrustNode explain(TNode literal) override;
-  /** Get the equality engine */
-  eq::EqualityEngine* getEqualityEngine() override;
   /** Get current substitution */
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
@@ -268,8 +272,6 @@ class TheoryStrings : public Theory {
    * theories is collected in this object.
    */
   SequencesStatistics d_statistics;
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
   /** The solver state object */
   SolverState d_state;
   /** The term registry for this theory */