(new theory) Update TheoryArrays to the new standard (#5000)

This includes using the standard d_conflict flag in TheoryState and splitting its check into 3 callbacks.

It also deletes some unused code and eliminates an assertion (line 791 of theory_arrays.cpp) which doesn't hold in a central architecture.

Further work on standardization for arrays will add an InferenceManager to guard its uses of asserting facts to equality engine (both for proofs and configurable theory combination).

FYI @barrettcw

5 files changed, 121 insertions, 452 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2da04ce66..0ad9526a5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -354,8 +354,6 @@ libcvc4_add_sources(
   theory/arith/type_enumerator.h
   theory/arrays/array_info.cpp
   theory/arrays/array_info.h
-  theory/arrays/static_fact_manager.cpp
-  theory/arrays/static_fact_manager.h
   theory/arrays/theory_arrays.cpp
   theory/arrays/theory_arrays.h
   theory/arrays/theory_arrays_rewriter.cpp
diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
deleted file mode 100644
index d2f4b75c9..000000000
--- a/src/theory/arrays/static_fact_manager.cpp
+++ /dev/null
@@ -1,170 +0,0 @@
-/*********************                                                        */
-/*! \file static_fact_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Clark Barrett, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include <iostream>
-
-#include "base/check.h"
-#include "expr/node.h"
-#include "theory/arrays/static_fact_manager.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-bool StaticFactManager::areEq(TNode a, TNode b) {
-  return (find(a) == find(b));
-}
-
-bool StaticFactManager::areDiseq(TNode a, TNode b) {
-  Node af = find(a);
-  Node bf = find(b);
-  Node left, right;
-  unsigned i;
-  for (i = 0; i < d_diseq.size(); ++i) {
-    left = find(d_diseq[i][0]);
-    right = find(d_diseq[i][1]);
-    if ((left == af && right == bf) ||
-        (left == bf && right == af)) {
-      return true;
-    }
-  }
-  return false;
-}
-
-void StaticFactManager::addDiseq(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL);
-  d_diseq.push_back(eq);
-}
-
-void StaticFactManager::addEq(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL);
-  Node a = find(eq[0]);
-  Node b = find(eq[1]);
-
-  if( a == b) {
-    return;
-  }
-
-  /*
-   * take care of the congruence closure part
-   */
-
-  // make "a" the one with shorter diseqList
-  // CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
-  // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
-
-  // if(deq_ia != d_disequalities.end()) {
-  //   if(deq_ib == d_disequalities.end() ||
-  //      (*deq_ia).second->size() > (*deq_ib).second->size()) {
-  //     TNode tmp = a;
-  //     a = b;
-  //     b = tmp;
-  //   }
-  // }
-  // a = find(a);
-  // b = find(b);
-
-
-  // b becomes the canon of a
-  setCanon(a, b);
-
-  // deq_ia = d_disequalities.find(a);
-  // map<TNode, TNode> alreadyDiseqs;
-  // if(deq_ia != d_disequalities.end()) {
-  //   /*
-  //    * Collecting the disequalities of b, no need to check for conflicts
-  //    * since the representative of b does not change and we check all the things
-  //    * in a's class when we look at the diseq list of find(a)
-  //    */
-
-  //   CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
-  //   if(deq_ib != d_disequalities.end()) {
-  //     CTNodeListAlloc* deq = (*deq_ib).second;
-  //     for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end();
-  //     j++) {
-  //       TNode deqn = *j;
-  //       TNode s = deqn[0];
-  //       TNode t = deqn[1];
-  //       TNode sp = find(s);
-  //       TNode tp = find(t);
-  //       Assert(sp == b || tp == b);
-  //       if(sp == b) {
-  //         alreadyDiseqs[tp] = deqn;
-  //       } else {
-  //         alreadyDiseqs[sp] = deqn;
-  //       }
-  //     }
-  //   }
-
-  //   /*
-  //    * Looking for conflicts in the a disequality list. Note
-  //    * that at this point a and b are already merged. Also has
-  //    * the side effect that it adds them to the list of b (which
-  //    * became the canonical representative)
-  //    */
-
-  //   CTNodeListAlloc* deqa = (*deq_ia).second;
-  //   for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end();
-  //   i++) {
-  //     TNode deqn = (*i);
-  //     Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() ==
-  //     kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; TNode sp = find(s);
-  //     TNode tp = find(t);
-
-  //     if(find(s) == find(t)) {
-  //       d_conflict = deqn;
-  //       return;
-  //     }
-  //     Assert( sp == b || tp == b);
-
-  //     // make sure not to add duplicates
-
-  //     if(sp == b) {
-  //       if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
-  //         appendToDiseqList(b, deqn);
-  //         alreadyDiseqs[tp] = deqn;
-  //       }
-  //     } else {
-  //       if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
-  //         appendToDiseqList(b, deqn);
-  //         alreadyDiseqs[sp] = deqn;
-  //       }
-  //     }
-
-  //   }
-  // }
-
-  // // TODO: check for equality propagations
-  // // a and b are find(a) and find(b) here
-  // checkPropagations(a,b);
-
-  // if(a.getType().isArray()) {
-  //   checkRowLemmas(a,b);
-  //   checkRowLemmas(b,a);
-  //   // note the change in order, merge info adds the list of
-  //   // the 2nd argument to the first
-  //   d_infoMap.mergeInfo(b, a);
-  // }
-}
-
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
deleted file mode 100644
index 2df4b0fda..000000000
--- a/src/theory/arrays/static_fact_manager.h
+++ /dev/null
@@ -1,116 +0,0 @@
-/*********************                                                        */
-/*! \file static_fact_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Clark Barrett, Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-#define CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-
-#include <utility>
-#include <vector>
-#include <unordered_map>
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-  class StaticFactManager {
-  /** Our underlying map type. */
-  typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
-
-  /**
-   * Our map of Nodes to their canonical representatives.
-   * If a Node is not present in the map, it is its own
-   * representative.
-   */
-  MapType d_map;
-  std::vector<Node> d_diseq;
-
-public:
-  StaticFactManager() {}
-
-  /**
-   * Return a Node's union-find representative, doing path compression.
-   */
-  inline TNode find(TNode n);
-
-  /**
-   * Return a Node's union-find representative, NOT doing path compression.
-   * This is useful for Assert() statements, debug checking, and similar
-   * things that you do NOT want to mutate the structure.
-   */
-  inline TNode debugFind(TNode n) const;
-
-  /**
-   * Set the canonical representative of n to newParent.  They should BOTH
-   * be their own canonical representatives on entry to this funciton.
-   */
-  inline void setCanon(TNode n, TNode newParent);
-
-  bool areEq(TNode a, TNode b);
-  bool areDiseq(TNode a, TNode b);
-  void addDiseq(TNode eq);
-  void addEq(TNode eq);
-
-};/* class StaticFactManager<> */
-
-inline TNode StaticFactManager::debugFind(TNode n) const {
-  MapType::const_iterator i = d_map.find(n);
-  if(i == d_map.end()) {
-    return n;
-  } else {
-    return debugFind((*i).second);
-  }
-}
-
-inline TNode StaticFactManager::find(TNode n) {
-  Trace("arraysuf") << "arraysUF find of " << n << std::endl;
-  MapType::iterator i = d_map.find(n);
-  if(i == d_map.end()) {
-    Trace("arraysuf") << "arraysUF   it is rep" << std::endl;
-    return n;
-  } else {
-    Trace("arraysuf") << "arraysUF   not rep: par is " << (*i).second << std::endl;
-    std::pair<TNode, TNode> pr = *i;
-    // our iterator is invalidated by the recursive call to find(),
-    // since it mutates the map
-    TNode p = find(pr.second);
-    if(p == pr.second) {
-      return p;
-    }
-    pr.second = p;
-    d_map.insert(pr);
-    return p;
-  }
-}
-
-inline void StaticFactManager::setCanon(TNode n, TNode newParent) {
-  Assert(d_map.find(n) == d_map.end());
-  Assert(d_map.find(newParent) == d_map.end());
-  if(n != newParent) {
-    d_map[n] = newParent;
-  }
-}
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 603dc9639..408f4c682 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -43,7 +43,6 @@ namespace arrays {
 
 // Use static configuration of options for now
 const bool d_ccStore = false;
-const bool d_useArrTable = false;
   //const bool d_eagerLemmas = false;
 const bool d_preprocess = true;
 const bool d_solveWrite = true;
@@ -85,7 +84,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_isPreRegistered(c),
       d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
       d_notify(*this),
-      d_conflict(c, false),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker, name),
       d_mergeQueue(c),
@@ -175,10 +173,6 @@ void TheoryArrays::finishInit()
   {
     d_equalityEngine->addFunctionKind(kind::STORE);
   }
-  if (d_useArrTable)
-  {
-    d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
-  }
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -401,7 +395,8 @@ bool TheoryArrays::propagateLit(TNode literal)
                   << std::endl;
 
   // If already in conflict, no more propagation
-  if (d_conflict) {
+  if (d_state.isInConflict())
+  {
     Debug("arrays") << spaces(getSatContext()->getLevel())
                     << "TheoryArrays::propagateLit(" << literal
                     << "): already in conflict" << std::endl;
@@ -414,7 +409,7 @@ bool TheoryArrays::propagateLit(TNode literal)
   }
   bool ok = d_out->propagate(literal);
   if (!ok) {
-    d_conflict = true;
+    d_state.notifyInConflict();
   }
   return ok;
 }/* TheoryArrays::propagate(TNode) */
@@ -644,7 +639,8 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
  */
 void TheoryArrays::preRegisterTermInternal(TNode node)
 {
-  if (d_conflict) {
+  if (d_state.isInConflict())
+  {
     return;
   }
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
@@ -788,7 +784,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       // The may equal needs the node
       d_mayEqualEqualityEngine.addTerm(node);
       d_equalityEngine->addTerm(node);
-      Assert(d_equalityEngine->getSize(node) == 1);
     }
     else {
       d_equalityEngine->addTerm(node);
@@ -802,7 +797,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   // !d_equalityEngine->consistent());
 }
 
-
 void TheoryArrays::preRegisterTerm(TNode node)
 {
   preRegisterTermInternal(node);
@@ -863,23 +857,6 @@ void TheoryArrays::notifySharedTerm(TNode t)
   }
 }
 
-
-EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode 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))
-  {
-    // The terms are implied to be dis-equal
-    return EQUALITY_FALSE;
-  }
-  return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
-}
-
-
 void TheoryArrays::checkPair(TNode r1, TNode r2)
 {
   Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
@@ -1061,6 +1038,7 @@ bool TheoryArrays::collectModelValues(TheoryModel* m,
   NodeManager* nm = NodeManager::currentNM();
   // Compute arrays that we need to produce representatives for
   std::vector<Node> arrays;
+
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
   for (; !eqcs_i.isFinished(); ++eqcs_i) {
     Node eqc = (*eqcs_i);
@@ -1113,12 +1091,14 @@ bool TheoryArrays::collectModelValues(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);
+    for (size_t i = 0; i < arrays.size(); ++i)
+    {
+      TNode n = arrays[i];
+      TNode nrep = d_equalityEngine->getRepresentative(n);
 
-    //if (fullModel) {
-      // Compute default value for this array - there is one default value for every mayEqual equivalence class
+      // if (fullModel) {
+      // Compute default value for this array - there is one default value for
+      // every mayEqual equivalence class
       TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
       it = d_defValues.find(mayRep);
       // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
@@ -1220,7 +1200,7 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
     Node d = skolem.eqNode(ref);
     Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
     d_equalityEngine->assertEquality(d, true, d_true);
-    Assert(!d_conflict);
+    Assert(!d_state.isInConflict());
     d_skolemAssertions.push_back(d);
     d_skolemIndex = d_skolemIndex + 1;
   }
@@ -1229,115 +1209,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
   return skolem;
 }
 
-
-void TheoryArrays::check(Effort e) {
-  if (done() && !fullEffort(e)) {
-    return;
-  }
-
-  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  while (!done() && !d_conflict)
+void TheoryArrays::postCheck(Effort level)
+{
+  if ((options::arraysEagerLemmas() || fullEffort(level))
+      && !d_state.isInConflict() && options::arraysWeakEquivalence())
   {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.d_assertion;
-
-    Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
-
-    bool polarity = fact.getKind() != kind::NOT;
-    TNode atom = polarity ? fact : fact[0];
-
-    if (!assertion.d_isPreregistered)
-    {
-      if (atom.getKind() == kind::EQUAL) {
-        if (!d_equalityEngine->hasTerm(atom[0]))
-        {
-          Assert(atom[0].isConst());
-          d_equalityEngine->addTerm(atom[0]);
-        }
-        if (!d_equalityEngine->hasTerm(atom[1]))
-        {
-          Assert(atom[1].isConst());
-          d_equalityEngine->addTerm(atom[1]);
-        }
-      }
-    }
-
-    // Do the work
-    switch (fact.getKind()) {
-      case kind::EQUAL:
-        d_equalityEngine->assertEquality(fact, true, fact);
-        break;
-      case kind::SELECT:
-        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))
-        {
-          // Assert the dis-equality
-          d_equalityEngine->assertEquality(fact[0], false, fact);
-
-          // Apply ArrDiseq Rule if diseq is between arrays
-          if(fact[0][0].getType().isArray() && !d_conflict) {
-            if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; }
-
-            NodeManager* nm = NodeManager::currentNM();
-            TypeNode indexType = fact[0][0].getType()[0];
-
-            TNode k;
-            // k is the skolem for this disequality.
-            Debug("pf::array")
-                << "Check: kind::NOT: array theory making a skolem"
-                << std::endl;
-            k = getSkolem(
-                fact,
-                "array_ext_index",
-                indexType,
-                "an extensional lemma index variable from the theory of arrays",
-                false);
-            Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
-            Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
-            Node eq = ak.eqNode(bk);
-            Node lemma = fact[0].orNode(eq.notNode());
-
-            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, theory::eq::MERGED_THROUGH_EXT);
-              ++d_numProp;
-            }
-
-            // If this is the solution pass, generate the lemma. Otherwise,
-            // don't generate it - as this is the lemma that we're reproving...
-            Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
-            d_out->lemma(lemma);
-            ++d_numExt;
-          } else {
-            Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
-            d_modelConstraints.push_back(fact);
-          }
-        }
-        break;
-    default:
-      Unreachable();
-      break;
-    }
-  }
-
-  if ((options::arraysEagerLemmas() || fullEffort(e)) && !d_conflict && options::arraysWeakEquivalence()) {
     // Replay all array merges to update weak equivalence data structures
     context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
     TNode a, b, eq;
@@ -1424,10 +1300,13 @@ void TheoryArrays::check(Effort e) {
     d_readTableContext->pop();
   }
 
-  if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
+  if (!options::arraysEagerLemmas() && fullEffort(level)
+      && !d_state.isInConflict() && !options::arraysWeakEquivalence())
+  {
     // generate the lemmas on the worklist
     Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
-    while (d_RowQueue.size() > 0 && !d_conflict) {
+    while (d_RowQueue.size() > 0 && !d_state.isInConflict())
+    {
       if (dischargeLemmas()) {
         break;
       }
@@ -1437,6 +1316,84 @@ void TheoryArrays::check(Effort e) {
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
 }
 
+bool TheoryArrays::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  if (!isPrereg)
+  {
+    if (atom.getKind() == kind::EQUAL)
+    {
+      if (!d_equalityEngine->hasTerm(atom[0]))
+      {
+        Assert(atom[0].isConst());
+        d_equalityEngine->addTerm(atom[0]);
+      }
+      if (!d_equalityEngine->hasTerm(atom[1]))
+      {
+        Assert(atom[1].isConst());
+        d_equalityEngine->addTerm(atom[1]);
+      }
+    }
+  }
+  return false;
+}
+
+void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+  // if a disequality
+  if (atom.getKind() == kind::EQUAL && !pol)
+  {
+    // Apply ArrDiseq Rule if diseq is between arrays
+    if (fact[0][0].getType().isArray() && !d_state.isInConflict())
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      TypeNode indexType = fact[0][0].getType()[0];
+
+      TNode k;
+      // k is the skolem for this disequality.
+      Debug("pf::array") << "Check: kind::NOT: array theory making a skolem"
+                          << std::endl;
+
+      // If not in replay mode, generate a fresh skolem variable
+      k = getSkolem(
+          fact,
+          "array_ext_index",
+          indexType,
+          "an extensional lemma index variable from the theory of arrays",
+          false);
+
+      Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
+      Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
+      Node eq = ak.eqNode(bk);
+      Node lemma = fact[0].orNode(eq.notNode());
+
+      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_numProp;
+      }
+
+      // If this is the solution pass, generate the lemma. Otherwise, don't
+      // generate it - as this is the lemma that we're reproving...
+      Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
+      d_out->lemma(lemma);
+      ++d_numExt;
+    }
+    else
+    {
+      Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem"
+                         << std::endl;
+      d_modelConstraints.push_back(fact);
+    }
+  }
+}
 
 Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
 {
@@ -1641,7 +1598,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     }
 
     // If no more to do, break
-    if (d_conflict || d_mergeQueue.empty()) {
+    if (d_state.isInConflict() || d_mergeQueue.empty())
+    {
       break;
     }
 
@@ -1865,7 +1823,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
   Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
 
-  if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
+  if (d_state.isInConflict() || d_RowAlreadyAdded.contains(lem))
+  {
     return;
   }
   TNode a, b, i, j;
@@ -1892,15 +1851,6 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     propagate(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)
-    {
-      return;
-    }
-  }
-
   // Prefer equality between indexes so as not to introduce new read terms
   if (options::arraysEagerIndexSplitting() && !bothExist
       && !d_equalityEngine->areDisequal(i, j, false))
@@ -2025,7 +1975,8 @@ bool TheoryArrays::dischargeLemmas()
     int prop = options::arraysPropagate();
     if (prop > 0) {
       propagate(l);
-      if (d_conflict) {
+      if (d_state.isInConflict())
+      {
         return true;
       }
     }
@@ -2103,7 +2054,7 @@ void TheoryArrays::conflict(TNode a, TNode b) {
     d_out->conflict(d_conflictNode);
   }
 
-  d_conflict = true;
+  d_state.notifyInConflict();
 }
 
 TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8fdbde0ab..dea3d4136 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -240,7 +240,6 @@ class TheoryArrays : public Theory {
 
  public:
   void notifySharedTerm(TNode t) override;
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   void computeCareGraph() override;
   bool isShared(TNode t)
   {
@@ -252,6 +251,7 @@ class TheoryArrays : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
  public:
+  /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
@@ -267,8 +267,18 @@ class TheoryArrays : public Theory {
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
 
- public:
-  void check(Effort e) override;
+  //--------------------------------- standard check
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  /** Pre-notify fact, return true if processed. */
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+  /** Notify fact */
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  //--------------------------------- end standard check
 
  private:
   TNode weakEquivGetRep(TNode node);
@@ -331,9 +341,6 @@ class TheoryArrays : public Theory {
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
-  /** Are we in conflict? */
-  context::CDO<bool> d_conflict;
-
   /** Conflict when merging constants */
   void conflict(TNode a, TNode b);
 
@@ -464,7 +471,6 @@ class TheoryArrays : public Theory {
    * for the comparison between the indexes that appears in the lemma.
    */
   Node getNextDecisionRequest();
-
   /**
    * Compute relevant terms. This includes select nodes for the
    * RIntro1 and RIntro2 rules.