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, 246 insertions, 168 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 245da617b..85759b75f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -88,7 +88,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_isPreRegistered(c),
       d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, name + "theory::arrays", true),
       d_conflict(c, false),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker, name),
@@ -112,7 +111,7 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_readTableContext(new context::Context()),
       d_arrayMerges(c),
       d_inCheckModel(false),
-      d_proofReconstruction(&d_equalityEngine),
+      d_proofReconstruction(nullptr),
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
 {
@@ -133,27 +132,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
   // The preprocessing congruence kinds
   d_ppEqualityEngine.addFunctionKind(kind::SELECT);
   d_ppEqualityEngine.addFunctionKind(kind::STORE);
-
-  // The kinds we are treating as function application in congruence
-  d_equalityEngine.addFunctionKind(kind::SELECT);
-  if (d_ccStore) {
-    d_equalityEngine.addFunctionKind(kind::STORE);
-  }
-  if (d_useArrTable) {
-    d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
-  }
-
-  d_reasonRow = d_equalityEngine.getFreshMergeReasonType();
-  d_reasonRow1 = d_equalityEngine.getFreshMergeReasonType();
-  d_reasonExt = d_equalityEngine.getFreshMergeReasonType();
-
-  d_proofReconstruction.setRowMergeTag(d_reasonRow);
-  d_proofReconstruction.setRow1MergeTag(d_reasonRow1);
-  d_proofReconstruction.setExtMergeTag(d_reasonExt);
-
-  d_equalityEngine.addPathReconstructionTrigger(d_reasonRow, &d_proofReconstruction);
-  d_equalityEngine.addPathReconstructionTrigger(d_reasonRow1, &d_proofReconstruction);
-  d_equalityEngine.addPathReconstructionTrigger(d_reasonExt, &d_proofReconstruction);
 }
 
 TheoryArrays::~TheoryArrays() {
@@ -179,8 +157,45 @@ TheoryArrays::~TheoryArrays() {
   smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
 }
 
-void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_equalityEngine.setMasterEqualityEngine(eq);
+TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = d_instanceName + "theory::arrays::ee";
+  return true;
+}
+
+void TheoryArrays::finishInit()
+{
+  Assert(d_equalityEngine != nullptr);
+
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine->addFunctionKind(kind::SELECT);
+  if (d_ccStore)
+  {
+    d_equalityEngine->addFunctionKind(kind::STORE);
+  }
+  if (d_useArrTable)
+  {
+    d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
+  }
+
+  d_proofReconstruction.reset(new ArrayProofReconstruction(d_equalityEngine));
+  d_reasonRow = d_equalityEngine->getFreshMergeReasonType();
+  d_reasonRow1 = d_equalityEngine->getFreshMergeReasonType();
+  d_reasonExt = d_equalityEngine->getFreshMergeReasonType();
+
+  d_proofReconstruction->setRowMergeTag(d_reasonRow);
+  d_proofReconstruction->setRow1MergeTag(d_reasonRow1);
+  d_proofReconstruction->setExtMergeTag(d_reasonExt);
+
+  d_equalityEngine->addPathReconstructionTrigger(d_reasonRow,
+                                                 d_proofReconstruction.get());
+  d_equalityEngine->addPathReconstructionTrigger(d_reasonRow1,
+                                                 d_proofReconstruction.get());
+  d_equalityEngine->addPathReconstructionTrigger(d_reasonExt,
+                                                 d_proofReconstruction.get());
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -427,9 +442,10 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
   //eq::EqProof * eqp = new eq::EqProof;
   // eq::EqProof * eqp = NULL;
   if (atom.getKind() == kind::EQUAL) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
+    d_equalityEngine->explainEquality(
+        atom[0], atom[1], polarity, assumptions, proof);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
+    d_equalityEngine->explainPredicate(atom, polarity, assumptions, proof);
   }
   if (Debug.isOn("pf::array"))
   {
@@ -469,7 +485,8 @@ TNode TheoryArrays::weakEquivGetRepIndex(TNode node, TNode index) {
       return node;
     }
     index2 = d_infoMap.getWeakEquivIndex(node);
-    if (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) {
+    if (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
+    {
       node = pointer;
     }
     else {
@@ -493,7 +510,8 @@ void TheoryArrays::visitAllLeaves(TNode reason, vector<TNode>& conjunctions) {
       conjunctions.push_back(reason);
       break;
     case kind::EQUAL:
-      d_equalityEngine.explainEquality(reason[0], reason[1], true, conjunctions);
+      d_equalityEngine->explainEquality(
+          reason[0], reason[1], true, conjunctions);
       break;
     default:
       Unreachable();
@@ -511,10 +529,11 @@ void TheoryArrays::weakEquivBuildCond(TNode node, TNode index, vector<TNode>& co
     index2 = d_infoMap.getWeakEquivIndex(node);
     if (index2.isNull()) {
       // Null index means these two nodes became equal: explain the equality.
-      d_equalityEngine.explainEquality(node, pointer, true, conjunctions);
+      d_equalityEngine->explainEquality(node, pointer, true, conjunctions);
       node = pointer;
     }
-    else if (!d_equalityEngine.areEqual(index, index2)) {
+    else if (!d_equalityEngine->areEqual(index, index2))
+    {
       // If indices are not equal in current context, need to add that to the lemma.
       Node reason = index.eqNode(index2).notNode();
       d_permRef.push_back(reason);
@@ -556,7 +575,8 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) {
   TNode index2 = d_infoMap.getWeakEquivIndex(secondary);
   Node reason;
   TNode next;
-  while (index2.isNull() || !d_equalityEngine.areEqual(index, index2)) {
+  while (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
+  {
     next = d_infoMap.getWeakEquivPointer(secondary);
     d_infoMap.setWeakEquivSecondary(node, next);
     reason = d_infoMap.getWeakEquivSecondaryReason(node);
@@ -590,13 +610,13 @@ void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arr
   TNode pointer, indexRep;
   if (!index.isNull()) {
     index_trail.push_back(index);
-    marked.insert(d_equalityEngine.getRepresentative(index));
+    marked.insert(d_equalityEngine->getRepresentative(index));
   }
   while (arrayFrom != arrayTo) {
     index = d_infoMap.getWeakEquivIndex(arrayFrom);
     pointer = d_infoMap.getWeakEquivPointer(arrayFrom);
     if (!index.isNull()) {
-      indexRep = d_equalityEngine.getRepresentative(index);
+      indexRep = d_equalityEngine->getRepresentative(index);
       if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) {
         weakEquivMakeRepIndex(arrayFrom);
         d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo);
@@ -639,7 +659,7 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
              || !secondary.isNull());
       if (!pointer.isNull()) {
         if (index.isNull()) {
-          Assert(d_equalityEngine.areEqual(n, pointer));
+          Assert(d_equalityEngine->areEqual(n, pointer));
         }
         else {
           Assert(
@@ -677,16 +697,17 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   case kind::EQUAL:
     // Add the trigger for equality
     // NOTE: note that if the equality is true or false already, it might not be added
-    d_equalityEngine.addTriggerEquality(node);
+    d_equalityEngine->addTriggerEquality(node);
     break;
   case kind::SELECT: {
     // Invariant: array terms should be preregistered before being added to the equality engine
-    if (d_equalityEngine.hasTerm(node)) {
+    if (d_equalityEngine->hasTerm(node))
+    {
       Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end());
       return;
     }
     // Reads
-    TNode store = d_equalityEngine.getRepresentative(node[0]);
+    TNode store = d_equalityEngine->getRepresentative(node[0]);
 
     // The may equal needs the store
     d_mayEqualEqualityEngine.addTerm(store);
@@ -694,15 +715,15 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray())
     {
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+      d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
     }
     else
     {
-      d_equalityEngine.addTerm(node);
+      d_equalityEngine->addTerm(node);
     }
     Assert((d_isPreRegistered.insert(node), true));
 
-    Assert(d_equalityEngine.getRepresentative(store) == store);
+    Assert(d_equalityEngine->getRepresentative(store) == store);
     d_infoMap.addIndex(store, node[1]);
 
     // Synchronize d_constReadsContext with SAT context
@@ -712,7 +733,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     }
 
     // Record read in sharing data structure
-    TNode index = d_equalityEngine.getRepresentative(node[1]);
+    TNode index = d_equalityEngine->getRepresentative(node[1]);
     if (!options::arraysWeakEquivalence() && index.isConst()) {
       CTNodeList* temp;
       CNodeNListMap::iterator it = d_constReads.find(index);
@@ -734,12 +755,13 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     break;
   }
   case kind::STORE: {
-    if (d_equalityEngine.hasTerm(node)) {
+    if (d_equalityEngine->hasTerm(node))
+    {
       break;
     }
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+    d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
 
-    TNode a = d_equalityEngine.getRepresentative(node[0]);
+    TNode a = d_equalityEngine->getRepresentative(node[0]);
 
     if (node.isConst()) {
       // Can't use d_mayEqualEqualityEngine to merge node with a because they are both constants,
@@ -761,12 +783,13 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     TNode v = node[2];
     NodeManager* nm = NodeManager::currentNM();
     Node ni = nm->mkNode(kind::SELECT, node, i);
-    if (!d_equalityEngine.hasTerm(ni)) {
+    if (!d_equalityEngine->hasTerm(ni))
+    {
       preRegisterTermInternal(ni);
     }
 
     // Apply RIntro1 Rule
-    d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+    d_equalityEngine->assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
 
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
@@ -787,7 +810,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     break;
   }
   case kind::STORE_ALL: {
-    if (d_equalityEngine.hasTerm(node)) {
+    if (d_equalityEngine->hasTerm(node))
+    {
       break;
     }
     ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
@@ -798,7 +822,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_infoMap.setConstArr(node, node);
     d_mayEqualEqualityEngine.addTerm(node);
     Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
+    d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
     d_defValues[node] = defaultValue;
     break;
   }
@@ -807,19 +831,19 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray()) {
       // The may equal needs the node
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
-      Assert(d_equalityEngine.getSize(node) == 1);
+      d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+      Assert(d_equalityEngine->getSize(node) == 1);
     }
     else {
-      d_equalityEngine.addTerm(node);
+      d_equalityEngine->addTerm(node);
     }
 
     break;
   }
   // Invariant: preregistered terms are exactly the terms in the equality engine
   // Disabled, see comment above for kind::EQUAL
-  // Assert(d_equalityEngine.hasTerm(node) ||
-  // !d_equalityEngine.consistent());
+  // Assert(d_equalityEngine->hasTerm(node) ||
+  // !d_equalityEngine->consistent());
 }
 
 
@@ -830,7 +854,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
   // Note: do this here instead of in preRegisterTermInternal to prevent internal select
   // terms from being propagated out (as this results in an assertion failure).
   if (node.getKind() == kind::SELECT && node.getType().isBoolean()) {
-    d_equalityEngine.addTriggerPredicate(node);
+    d_equalityEngine->addTriggerPredicate(node);
   }
 }
 
@@ -862,7 +886,7 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
 
 void TheoryArrays::addSharedTerm(TNode t) {
   Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAYS);
+  d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS);
   if (t.getType().isArray()) {
     d_sharedArrays.insert(t);
   }
@@ -876,12 +900,14 @@ void TheoryArrays::addSharedTerm(TNode t) {
 
 
 EqualityStatus TheoryArrays::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;
   }
@@ -895,16 +921,19 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
 
   TNode x = r1[1];
   TNode y = r2[1];
-  Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS));
+  Assert(d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS));
 
-  if (d_equalityEngine.hasTerm(x) && d_equalityEngine.hasTerm(y) &&
-      (d_equalityEngine.areEqual(x,y) || d_equalityEngine.areDisequal(x,y,false))) {
+  if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
+      && (d_equalityEngine->areEqual(x, y)
+          || d_equalityEngine->areDisequal(x, y, false)))
+  {
     Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl;
     return;
   }
 
   // If the terms are already known to be equal, we are also in good shape
-  if (d_equalityEngine.areEqual(r1, r2)) {
+  if (d_equalityEngine->areEqual(r1, r2))
+  {
     Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
     return;
   }
@@ -913,8 +942,9 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
     // If arrays are known to be disequal, or cannot become equal, we can continue
     Assert(d_mayEqualEqualityEngine.hasTerm(r1[0])
            && d_mayEqualEqualityEngine.hasTerm(r2[0]));
-    if (r1[0].getType() != r2[0].getType() ||
-        d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
+    if (r1[0].getType() != r2[0].getType()
+        || d_equalityEngine->areDisequal(r1[0], r2[0], false))
+    {
       Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
       return;
     }
@@ -923,14 +953,17 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
     }
   }
 
-  if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAYS)) {
+  if (!d_equalityEngine->isTriggerTerm(y, THEORY_ARRAYS))
+  {
     Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
     return;
   }
 
   // Get representative trigger terms
-  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
-  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAYS);
+  TNode x_shared =
+      d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
+  TNode y_shared =
+      d_equalityEngine->getTriggerTermRepresentative(y, THEORY_ARRAYS);
   EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
   switch (eqStatusDomain) {
     case EQUALITY_TRUE_AND_PROPAGATED:
@@ -999,14 +1032,16 @@ void TheoryArrays::computeCareGraph()
       TNode r1 = d_reads[i];
 
       Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1 << std::endl;
-      Assert(d_equalityEngine.hasTerm(r1));
+      Assert(d_equalityEngine->hasTerm(r1));
       TNode x = r1[1];
 
-      if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS)) {
+      if (!d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS))
+      {
         Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
         continue;
       }
-      Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
+      Node x_shared =
+          d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
 
       // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
       // Also, insert this read in the list at the proper index
@@ -1034,12 +1069,12 @@ void TheoryArrays::computeCareGraph()
         // We don't know the model value for x.  Just do brute force examination of all pairs of reads
         for (unsigned j = 0; j < size; ++j) {
           TNode r2 = d_reads[j];
-          Assert(d_equalityEngine.hasTerm(r2));
+          Assert(d_equalityEngine->hasTerm(r2));
           checkPair(r1,r2);
         }
         for (unsigned j = 0; j < d_constReadsList.size(); ++j) {
           TNode r2 = d_constReadsList[j];
-          Assert(d_equalityEngine.hasTerm(r2));
+          Assert(d_equalityEngine->hasTerm(r2));
           checkPair(r1,r2);
         }
       }
@@ -1064,7 +1099,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> arrays;
   bool computeRep, isArray;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
   for (; !eqcs_i.isFinished(); ++eqcs_i) {
     Node eqc = (*eqcs_i);
     isArray = eqc.getType().isArray();
@@ -1072,7 +1107,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
       continue;
     }
     computeRep = false;
-    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
     for (; !eqc_i.isFinished(); ++eqc_i) {
       Node n = *eqc_i;
       // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
@@ -1095,30 +1130,36 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
   bool changed;
   do {
     changed = false;
-    eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+    eqcs_i = eq::EqClassesIterator(d_equalityEngine);
     for (; !eqcs_i.isFinished(); ++eqcs_i) {
       Node eqc = (*eqcs_i);
-      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
       for (; !eqc_i.isFinished(); ++eqc_i) {
         Node n = *eqc_i;
         if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) {
 
           // Find all terms equivalent to n[0] and get corresponding read terms
-          Node array_eqc = d_equalityEngine.getRepresentative(n[0]);
-          eq::EqClassIterator array_eqc_i = eq::EqClassIterator(array_eqc, &d_equalityEngine);
+          Node array_eqc = d_equalityEngine->getRepresentative(n[0]);
+          eq::EqClassIterator array_eqc_i =
+              eq::EqClassIterator(array_eqc, d_equalityEngine);
           for (; !array_eqc_i.isFinished(); ++array_eqc_i) {
             Node arr = *array_eqc_i;
-            if (arr.getKind() == kind::STORE &&
-                termSet.find(arr) != termSet.end() &&
-                !d_equalityEngine.areEqual(arr[1],n[1])) {
+            if (arr.getKind() == kind::STORE
+                && termSet.find(arr) != termSet.end()
+                && !d_equalityEngine->areEqual(arr[1], n[1]))
+            {
               Node r = nm->mkNode(kind::SELECT, arr, n[1]);
-              if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+              if (termSet.find(r) == termSet.end()
+                  && d_equalityEngine->hasTerm(r))
+              {
                 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(a) read: " << r << endl;
                 termSet.insert(r);
                 changed = true;
               }
               r = nm->mkNode(kind::SELECT, arr[0], n[1]);
-              if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+              if (termSet.find(r) == termSet.end()
+                  && d_equalityEngine->hasTerm(r))
+              {
                 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(b) read: " << r << endl;
                 termSet.insert(r);
                 changed = true;
@@ -1132,16 +1173,21 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
           for(; it < instores->size(); ++it) {
             TNode instore = (*instores)[it];
             Assert(instore.getKind() == kind::STORE);
-            if (termSet.find(instore) != termSet.end() &&
-                !d_equalityEngine.areEqual(instore[1],n[1])) {
+            if (termSet.find(instore) != termSet.end()
+                && !d_equalityEngine->areEqual(instore[1], n[1]))
+            {
               Node r = nm->mkNode(kind::SELECT, instore, n[1]);
-              if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+              if (termSet.find(r) == termSet.end()
+                  && d_equalityEngine->hasTerm(r))
+              {
                 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(c) read: " << r << endl;
                 termSet.insert(r);
                 changed = true;
               }
               r = nm->mkNode(kind::SELECT, instore[0], n[1]);
-              if (termSet.find(r) == termSet.end() && d_equalityEngine.hasTerm(r)) {
+              if (termSet.find(r) == termSet.end()
+                  && d_equalityEngine->hasTerm(r))
+              {
                 Trace("arrays::collectModelInfo") << "TheoryArrays::collectModelInfo, adding RIntro2(d) read: " << r << endl;
                 termSet.insert(r);
                 changed = true;
@@ -1154,7 +1200,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
   } while (changed);
 
   // Send the equality engine information to the model
-  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
   {
     return false;
   }
@@ -1166,7 +1212,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
     Node n = *set_it;
     // If this term is a select, record that the EC rep of its store parameter is being read from using this term
     if (n.getKind() == kind::SELECT) {
-      selects[d_equalityEngine.getRepresentative(n[0])].push_back(n);
+      selects[d_equalityEngine->getRepresentative(n[0])].push_back(n);
     }
   }
 
@@ -1177,7 +1223,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
   // Compute all default values already in use
   //if (fullModel) {
     for (size_t i=0; i<arrays.size(); ++i) {
-      TNode nrep = d_equalityEngine.getRepresentative(arrays[i]);
+      TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
       d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
       TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
       it = d_defValues.find(mayRep);
@@ -1190,7 +1236,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
   // Loop through all array equivalence classes that need a representative computed
   for (size_t i=0; i<arrays.size(); ++i) {
     TNode n = arrays[i];
-    TNode nrep = d_equalityEngine.getRepresentative(n);
+    TNode nrep = d_equalityEngine->getRepresentative(n);
 
     //if (fullModel) {
       // Compute default value for this array - there is one default value for every mayEqual equivalence class
@@ -1280,9 +1326,9 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
   }
   else {
     skolem = (*it).second;
-    if (d_equalityEngine.hasTerm(ref) &&
-        d_equalityEngine.hasTerm(skolem) &&
-        d_equalityEngine.areEqual(ref, skolem)) {
+    if (d_equalityEngine->hasTerm(ref) && d_equalityEngine->hasTerm(skolem)
+        && d_equalityEngine->areEqual(ref, skolem))
+    {
       makeEqual = false;
     }
   }
@@ -1294,7 +1340,7 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
   if (makeEqual) {
     Node d = skolem.eqNode(ref);
     Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
-    d_equalityEngine.assertEquality(d, true, d_true);
+    d_equalityEngine->assertEquality(d, true, d_true);
     Assert(!d_conflict);
     d_skolemAssertions.push_back(d);
     d_skolemIndex = d_skolemIndex + 1;
@@ -1328,13 +1374,15 @@ void TheoryArrays::check(Effort e) {
     if (!assertion.d_isPreregistered)
     {
       if (atom.getKind() == kind::EQUAL) {
-        if (!d_equalityEngine.hasTerm(atom[0])) {
+        if (!d_equalityEngine->hasTerm(atom[0]))
+        {
           Assert(atom[0].isConst());
-          d_equalityEngine.addTerm(atom[0]);
+          d_equalityEngine->addTerm(atom[0]);
         }
-        if (!d_equalityEngine.hasTerm(atom[1])) {
+        if (!d_equalityEngine->hasTerm(atom[1]))
+        {
           Assert(atom[1].isConst());
-          d_equalityEngine.addTerm(atom[1]);
+          d_equalityEngine->addTerm(atom[1]);
         }
       }
     }
@@ -1342,17 +1390,19 @@ void TheoryArrays::check(Effort e) {
     // Do the work
     switch (fact.getKind()) {
       case kind::EQUAL:
-        d_equalityEngine.assertEquality(fact, true, fact);
+        d_equalityEngine->assertEquality(fact, true, fact);
         break;
       case kind::SELECT:
-        d_equalityEngine.assertPredicate(fact, true, fact);
+        d_equalityEngine->assertPredicate(fact, true, fact);
         break;
       case kind::NOT:
         if (fact[0].getKind() == kind::SELECT) {
-          d_equalityEngine.assertPredicate(fact[0], false, fact);
-        } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) {
+          d_equalityEngine->assertPredicate(fact[0], false, fact);
+        }
+        else if (!d_equalityEngine->areDisequal(fact[0][0], fact[0][1], false))
+        {
           // Assert the dis-equality
-          d_equalityEngine.assertEquality(fact[0], false, fact);
+          d_equalityEngine->assertEquality(fact[0], false, fact);
 
           // Apply ArrDiseq Rule if diseq is between arrays
           if(fact[0][0].getType().isArray() && !d_conflict) {
@@ -1396,18 +1446,26 @@ void TheoryArrays::check(Effort e) {
             // when we output the lemma. However, in replay need the lemma to be propagated, and so we
             // preregister manually.
             if (d_proofsEnabled) {
-              if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); }
-              if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); }
+              if (!d_equalityEngine->hasTerm(ak))
+              {
+                preRegisterTermInternal(ak);
+              }
+              if (!d_equalityEngine->hasTerm(bk))
+              {
+                preRegisterTermInternal(bk);
+              }
             }
 
-            if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) {
+            if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
+                && d_equalityEngine->hasTerm(bk))
+            {
               // Propagate witness disequality - might produce a conflict
               d_permRef.push_back(lemma);
               Debug("pf::array") << "Asserting to the equality engine:" << std::endl
                                  << "\teq = " << eq << std::endl
                                  << "\treason = " << fact << std::endl;
 
-              d_equalityEngine.assertEquality(eq, false, fact, d_reasonExt);
+              d_equalityEngine->assertEquality(eq, false, fact, d_reasonExt);
               ++d_numProp;
             }
 
@@ -1465,7 +1523,7 @@ void TheoryArrays::check(Effort e) {
 
       // Find the bucket for this read.
       mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]);
-      iRep = d_equalityEngine.getRepresentative(r[1]);
+      iRep = d_equalityEngine->getRepresentative(r[1]);
       std::pair<TNode, TNode> key(mayRep, iRep);
       ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key);
       if (rbm_it == d_readBucketTable.end())
@@ -1484,20 +1542,21 @@ void TheoryArrays::check(Effort e) {
         const TNode& r2 = *ctnl_it;
         Assert(r2.getKind() == kind::SELECT);
         Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0]));
-        Assert(iRep == d_equalityEngine.getRepresentative(r2[1]));
-        if (d_equalityEngine.areEqual(r, r2)) {
+        Assert(iRep == d_equalityEngine->getRepresentative(r2[1]));
+        if (d_equalityEngine->areEqual(r, r2))
+        {
           continue;
         }
         if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) {
           // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
           vector<TNode> conjunctions;
-          Assert(d_equalityEngine.areEqual(r, Rewriter::rewrite(r)));
-          Assert(d_equalityEngine.areEqual(r2, Rewriter::rewrite(r2)));
+          Assert(d_equalityEngine->areEqual(r, Rewriter::rewrite(r)));
+          Assert(d_equalityEngine->areEqual(r2, Rewriter::rewrite(r2)));
           Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate();
           d_permRef.push_back(lemma);
           conjunctions.push_back(lemma);
           if (r[1] != r2[1]) {
-            d_equalityEngine.explainEquality(r[1], r2[1], true, conjunctions);
+            d_equalityEngine->explainEquality(r[1], r2[1], true, conjunctions);
           }
           // TODO: get smaller lemmas by eliminating shared parts of path
           weakEquivBuildCond(r[0], r[1], conjunctions);
@@ -1648,8 +1707,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     // Normally, a is its own representative, but it's possible for a to have
     // been merged with another array after it got queued up by the equality engine,
     // so we take its representative to be safe.
-    a = d_equalityEngine.getRepresentative(a);
-    Assert(d_equalityEngine.getRepresentative(b) == a);
+    a = d_equalityEngine->getRepresentative(a);
+    Assert(d_equalityEngine->getRepresentative(b) == a);
     Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n";
 
     if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
@@ -1759,7 +1818,7 @@ void TheoryArrays::checkStore(TNode a) {
   TNode b = a[0];
   TNode i = a[1];
 
-  TNode brep = d_equalityEngine.getRepresentative(b);
+  TNode brep = d_equalityEngine->getRepresentative(b);
 
   if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) {
     const CTNodeList* js = d_infoMap.getIndices(brep);
@@ -1786,17 +1845,18 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
-  Assert(d_equalityEngine.getRepresentative(a) == a);
+  Assert(d_equalityEngine->getRepresentative(a) == a);
 
   TNode constArr = d_infoMap.getConstArr(a);
   if (!constArr.isNull()) {
     ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
     Node defValue = storeAll.getValue();
     Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
-    if (!d_equalityEngine.hasTerm(selConst)) {
+    if (!d_equalityEngine->hasTerm(selConst))
+    {
       preRegisterTermInternal(selConst);
     }
-    d_equalityEngine.assertEquality(selConst.eqNode(defValue), true, d_true);
+    d_equalityEngine->assertEquality(selConst.eqNode(defValue), true, d_true);
   }
 
   const CTNodeList* stores = d_infoMap.getStores(a);
@@ -1848,7 +1908,8 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
     for( ; it < i_a->size(); ++it) {
       TNode i = (*i_a)[it];
       Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
-      if (!d_equalityEngine.hasTerm(selConst)) {
+      if (!d_equalityEngine->hasTerm(selConst))
+      {
         preRegisterTermInternal(selConst);
       }
     }
@@ -1901,8 +1962,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
   std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
-  if (d_equalityEngine.areEqual(a,b) ||
-      d_equalityEngine.areEqual(i,j)) {
+  if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
+  {
     return;
   }
 
@@ -1911,14 +1972,15 @@ void TheoryArrays::propagate(RowLemmaType lem)
   Node bj = nm->mkNode(kind::SELECT, b, j);
 
   // Try to avoid introducing new read terms: track whether these already exist
-  bool ajExists = d_equalityEngine.hasTerm(aj);
-  bool bjExists = d_equalityEngine.hasTerm(bj);
+  bool ajExists = d_equalityEngine->hasTerm(aj);
+  bool bjExists = d_equalityEngine->hasTerm(bj);
   bool bothExist = ajExists && bjExists;
 
   // If propagating, check propagations
   int prop = options::arraysPropagate();
   if (prop > 0) {
-    if (d_equalityEngine.areDisequal(i,j,true) && (bothExist || prop > 1)) {
+    if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1))
+    {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
       Node aj_eq_bj = aj.eqNode(bj);
       Node reason =
@@ -1930,17 +1992,18 @@ void TheoryArrays::propagate(RowLemmaType lem)
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
-      d_equalityEngine.assertEquality(aj_eq_bj, true, reason, d_reasonRow);
+      d_equalityEngine->assertEquality(aj_eq_bj, true, reason, d_reasonRow);
       ++d_numProp;
       return;
     }
-    if (bothExist && d_equalityEngine.areDisequal(aj,bj,true)) {
+    if (bothExist && d_equalityEngine->areDisequal(aj, bj, true))
+    {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
       Node reason =
           (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
       Node i_eq_j = i.eqNode(j);
       d_permRef.push_back(reason);
-      d_equalityEngine.assertEquality(i_eq_j, true, reason, d_reasonRow);
+      d_equalityEngine->assertEquality(i_eq_j, true, reason, d_reasonRow);
       ++d_numProp;
       return;
     }
@@ -1958,8 +2021,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   std::tie(a, b, i, j) = lem;
 
   Assert(a.getType().isArray() && b.getType().isArray());
-  if (d_equalityEngine.areEqual(a,b) ||
-      d_equalityEngine.areEqual(i,j)) {
+  if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
+  {
     return;
   }
 
@@ -1968,8 +2031,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   Node bj = nm->mkNode(kind::SELECT, b, j);
 
   // Try to avoid introducing new read terms: track whether these already exist
-  bool ajExists = d_equalityEngine.hasTerm(aj);
-  bool bjExists = d_equalityEngine.hasTerm(bj);
+  bool ajExists = d_equalityEngine->hasTerm(aj);
+  bool bjExists = d_equalityEngine->hasTerm(bj);
   bool bothExist = ajExists && bjExists;
 
   // If propagating, check propagations
@@ -1981,13 +2044,16 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   // If equivalent lemma already exists, don't enqueue this one
   if (d_useArrTable) {
     Node tableEntry = NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
-    if (d_equalityEngine.getSize(tableEntry) != 1) {
+    if (d_equalityEngine->getSize(tableEntry) != 1)
+    {
       return;
     }
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
-  if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
+  if (options::arraysEagerIndexSplitting() && !bothExist
+      && !d_equalityEngine->areDisequal(i, j, false))
+  {
     Node i_eq_j;
     if (!d_proofsEnabled) {
       i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
@@ -2008,20 +2074,22 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       if (!ajExists) {
         preRegisterTermInternal(aj);
       }
-      if (!d_equalityEngine.hasTerm(aj2)) {
+      if (!d_equalityEngine->hasTerm(aj2))
+      {
         preRegisterTermInternal(aj2);
       }
-      d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+      d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
-      if (!d_equalityEngine.hasTerm(bj2)) {
+      if (!d_equalityEngine->hasTerm(bj2))
+      {
         preRegisterTermInternal(bj2);
       }
-      d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
+      d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true);
     }
     if (aj2 == bj2) {
       return;
@@ -2031,20 +2099,22 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
-      if (!d_equalityEngine.hasTerm(aj2)) {
+      if (!d_equalityEngine->hasTerm(aj2))
+      {
         preRegisterTermInternal(aj2);
       }
-      if (!d_equalityEngine.hasTerm(bj2)) {
+      if (!d_equalityEngine->hasTerm(bj2))
+      {
         preRegisterTermInternal(bj2);
       }
-      d_equalityEngine.assertEquality(eq1, true, d_true);
+      d_equalityEngine->assertEquality(eq1, true, d_true);
       return;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_equalityEngine.assertEquality(eq2, true, d_true);
+      d_equalityEngine->assertEquality(eq2, true, d_true);
       return;
     }
 
@@ -2089,14 +2159,16 @@ bool TheoryArrays::dischargeLemmas()
     NodeManager* nm = NodeManager::currentNM();
     Node aj = nm->mkNode(kind::SELECT, a, j);
     Node bj = nm->mkNode(kind::SELECT, b, j);
-    bool ajExists = d_equalityEngine.hasTerm(aj);
-    bool bjExists = d_equalityEngine.hasTerm(bj);
+    bool ajExists = d_equalityEngine->hasTerm(aj);
+    bool bjExists = d_equalityEngine->hasTerm(bj);
 
     // Check for redundant lemma
     // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
-    if (!d_equalityEngine.hasTerm(i) || !d_equalityEngine.hasTerm(j) || d_equalityEngine.areEqual(i,j) ||
-        !d_equalityEngine.hasTerm(a) || !d_equalityEngine.hasTerm(b) || d_equalityEngine.areEqual(a,b) ||
-        (ajExists && bjExists && d_equalityEngine.areEqual(aj,bj))) {
+    if (!d_equalityEngine->hasTerm(i) || !d_equalityEngine->hasTerm(j)
+        || d_equalityEngine->areEqual(i, j) || !d_equalityEngine->hasTerm(a)
+        || !d_equalityEngine->hasTerm(b) || d_equalityEngine->areEqual(a, b)
+        || (ajExists && bjExists && d_equalityEngine->areEqual(aj, bj)))
+    {
       continue;
     }
 
@@ -2114,21 +2186,22 @@ bool TheoryArrays::dischargeLemmas()
       if (!ajExists) {
         preRegisterTermInternal(aj);
       }
-      if (!d_equalityEngine.hasTerm(aj2)) {
+      if (!d_equalityEngine->hasTerm(aj2))
+      {
         preRegisterTermInternal(aj2);
       }
-      d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+      d_equalityEngine->assertEquality(aj.eqNode(aj2), true, d_true);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
-      if (!d_equalityEngine.hasTerm(bj2)) {
+      if (!d_equalityEngine->hasTerm(bj2))
+      {
         preRegisterTermInternal(bj2);
       }
-      d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
-
+      d_equalityEngine->assertEquality(bj.eqNode(bj2), true, d_true);
     }
     if (aj2 == bj2) {
       continue;
@@ -2138,20 +2211,22 @@ bool TheoryArrays::dischargeLemmas()
     Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
-      if (!d_equalityEngine.hasTerm(aj2)) {
+      if (!d_equalityEngine->hasTerm(aj2))
+      {
         preRegisterTermInternal(aj2);
       }
-      if (!d_equalityEngine.hasTerm(bj2)) {
+      if (!d_equalityEngine->hasTerm(bj2))
+      {
         preRegisterTermInternal(bj2);
       }
-      d_equalityEngine.assertEquality(eq1, true, d_true);
+      d_equalityEngine->assertEquality(eq1, true, d_true);
       continue;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_equalityEngine.assertEquality(eq2, true, d_true);
+      d_equalityEngine->assertEquality(eq2, true, d_true);
       continue;
     }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 116b0f43b..f1cd2ea14 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -148,9 +148,18 @@ class TheoryArrays : public Theory {
                std::string name = "");
   ~TheoryArrays();
 
-  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("TheoryArrays"); }
 
@@ -353,9 +362,6 @@ class TheoryArrays : 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;
 
@@ -460,7 +466,7 @@ class TheoryArrays : public Theory {
   int d_topLevel;
 
   /** An equality-engine callback for proof reconstruction */
-  ArrayProofReconstruction d_proofReconstruction;
+  std::unique_ptr<ArrayProofReconstruction> d_proofReconstruction;
 
   /**
    * The decision strategy for the theory of arrays, which calls the
@@ -493,9 +499,6 @@ class TheoryArrays : public Theory {
    */
   Node getNextDecisionRequest();
 
- public:
-  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
-
 };/* class TheoryArrays */
 
 }/* CVC4::theory::arrays namespace */