merge from arrays-clark branch

7 files changed, 1049 insertions, 1154 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 50ded8758..cd6c38a7f 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -139,6 +139,20 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){
 };
 
 
+void ArrayInfo::setNonLinear(const TNode a) {
+  Assert(a.getType().isArray());
+  Info* temp_info;
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_info = new Info(ct, bck);
+    temp_info->isNonLinear = true;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->isNonLinear = true;
+  }
+  
+}
+
 
 /**
  * Returns the information associated with TNode a
@@ -152,6 +166,15 @@ const Info* ArrayInfo::getInfo(const TNode a) const{
   return emptyInfo;
 }
 
+const bool ArrayInfo::isNonLinear(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end())
+      return (*it).second->isNonLinear;
+  return false;
+}
+
 List<TNode>* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index d1c435b48..3eae369ca 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -55,9 +55,10 @@ namespace theory {
 namespace arrays {
 
 typedef context::CDList<TNode> CTNodeList;
+typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
-struct TNodeQuadHashFunction {
-  size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const {
+struct RowLemmaTypeHashFunction {
+  size_t operator()(const RowLemmaType& q ) const {
     TNode n1 = q.first;
     TNode n2 = q.second;
     TNode n3 = q.third;
@@ -66,7 +67,7 @@ struct TNodeQuadHashFunction {
         n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
 
   }
-};/* struct TNodeQuadHashFunction */
+};/* struct RowLemmaTypeHashFunction */
 
 void printList (CTNodeList* list);
 void printList( List<TNode>* list);
@@ -81,11 +82,12 @@ bool inList(const CTNodeList* l, const TNode el);
 
 class Info {
 public:
+  context::CDO<bool> isNonLinear;
   List<TNode>* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false) {
     indices = new List<TNode>(bck);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -228,6 +230,7 @@ public:
   void addStore(const Node a, const TNode st);
   void addInStore(const TNode a, const TNode st);
 
+  void setNonLinear(const TNode a);
 
   /**
    * Returns the information associated with TNode a
@@ -235,6 +238,8 @@ public:
 
   const Info* getInfo(const TNode a) const;
 
+  const bool isNonLinear(const TNode a) const;
+
   List<TNode>* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 2f4bc7313..06240a315 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -7,7 +7,7 @@
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
 
-properties polite stable-infinite
+properties polite stable-infinite parametric
 properties check propagate presolve
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
@@ -24,7 +24,11 @@ operator SELECT 2 "array select"
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store"
 
+# used internally by array theory
+operator ARR_TABLE_FUN 4 "array table function"
+
 typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
 typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 
 endtheory
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 03a9d7a4c..718483143 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,45 +23,87 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
+#include "theory/uf/equality_engine_impl.h"
+
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
 
 
-TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+
+// These are the options that produce the best empirical results on QF_AX benchmarks.
+// Use static configuration of options for now
+const bool d_ccStore = false;
+const bool d_useArrTable = false;
+const bool d_eagerLemmas = true;
+const bool d_propagateLemmas = false;
+const bool d_preprocess = true;
+const bool d_solveWrite = true;
+const bool d_useNonLinearOpt = true;
+
+
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_ARRAY, c, u, out, valuation),
-  d_ccChannel(this),
-  d_cc(c, &d_ccChannel),
-  d_unionFind(c),
-  d_backtracker(c),
-  d_infoMap(c,&d_backtracker),
-  d_disequalities(c),
-  d_equalities(c),
-  d_prop_queue(c),
-  d_atoms(),
-  d_explanations(c),
-  d_conflict(),
   d_numRow("theory::arrays::number of Row lemmas", 0),
   d_numExt("theory::arrays::number of Ext lemmas", 0),
   d_numProp("theory::arrays::number of propagations", 0),
   d_numExplain("theory::arrays::number of explanations", 0),
+  d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
+  d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
   d_checkTimer("theory::arrays::checkTime"),
-  d_donePreregister(false)
+  d_ppNotify(),
+  d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"),
+  d_ppFacts(u),
+  //  d_ppCache(u),  
+  d_literalsToPropagate(c),
+  d_literalsToPropagateIndex(c, 0),
+  d_mayEqualNotify(),
+  d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"),
+  d_notify(*this),
+  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
+  d_conflict(c, false),
+  d_backtracker(c),
+  d_infoMap(c, &d_backtracker),
+  d_mergeQueue(c),
+  d_mergeInProgress(false),
+  d_RowQueue(u),
+  d_RowAlreadyAdded(u),
+  d_sharedArrays(c),
+  d_sharedTerms(c, false),
+  d_reads(c),
+  d_permRef(c)
 {
-  //d_backtracker = new Backtracker<TNode>(c);
-  //d_infoMap = ArrayInfo(c, d_backtracker);
-
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
   StatisticsRegistry::registerStat(&d_numProp);
   StatisticsRegistry::registerStat(&d_numExplain);
+  StatisticsRegistry::registerStat(&d_numNonLinear);
+  StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
   StatisticsRegistry::registerStat(&d_checkTimer);
 
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
+  d_ppEqualityEngine.addTerm(d_true);
+  d_ppEqualityEngine.addTerm(d_false);
+  d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+  d_equalityEngine.addTerm(d_true);
+  d_equalityEngine.addTerm(d_false);
+  d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
 
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::SELECT);
+  if (d_ccStore) {
+    d_equalityEngine.addFunctionKind(kind::STORE);
+  }
+  d_equalityEngine.addFunctionKind(kind::EQUAL);
+  if (d_useArrTable) {
+    d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
+  }
 }
 
 
@@ -71,159 +113,27 @@ TheoryArrays::~TheoryArrays() {
   StatisticsRegistry::unregisterStat(&d_numExt);
   StatisticsRegistry::unregisterStat(&d_numProp);
   StatisticsRegistry::unregisterStat(&d_numExplain);
+  StatisticsRegistry::unregisterStat(&d_numNonLinear);
+  StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
   StatisticsRegistry::unregisterStat(&d_checkTimer);
 
 }
 
 
-void TheoryArrays::addSharedTerm(TNode t) {
-  Trace("arrays") << "Arrays::addSharedTerm(): "
-                  << t << endl;
-}
-
-
-void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
-}
-
-void TheoryArrays::notifyCongruent(TNode a, TNode b) {
-  Trace("arrays") << "Arrays::notifyCongruent(): "
-       << a << " = " << b << endl;
-  if(!d_conflict.isNull()) {
-    return;
-  }
-  merge(a,b);
-}
-
-
-void TheoryArrays::check(Effort e) {
-  TimerStat::CodeTimer codeTimer(d_checkTimer);
-
-  if(!d_donePreregister ) {
-    // only start looking for lemmas after preregister on all input terms
-    // has been called
-   return;
-  }
-
-  Trace("arrays") <<"Arrays::start check ";
-  while(!done()) {
-    Node assertion = get();
-    Trace("arrays") << "Arrays::check(): " << assertion << endl;
-
-    switch(assertion.getKind()) {
-    case kind::EQUAL:
-    case kind::IFF:
-      d_cc.addEquality(assertion);
-      if(!d_conflict.isNull()) {
-        // addEquality can cause a notify congruent which calls merge
-        // which can lead to a conflict
-        Node conflict = constructConflict(d_conflict);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-      }
-      merge(assertion[0], assertion[1]);
-      break;
-    case kind::NOT:
-    {
-      Assert(assertion[0].getKind() == kind::EQUAL ||
-         assertion[0].getKind() == kind::IFF );
-      Node a = assertion[0][0];
-      Node b = assertion[0][1];
-      addDiseq(assertion[0]);
-
-      d_cc.addTerm(a);
-      d_cc.addTerm(b);
-
-      if(!d_conflict.isNull()) {
-        // we got notified through notifyCongruent which called merge
-        // after addTerm since we weren't watching a or b before
-        Node conflict = constructConflict(d_conflict);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-      }
-      else if(find(a) == find(b)) {
-        Node conflict = constructConflict(assertion[0]);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-        }
-      Assert(!d_cc.areCongruent(a,b));
-      if(a.getType().isArray()) {
-        queueExtLemma(a, b);
-      }
-      break;
-    }
-    default:
-      Unhandled(assertion.getKind());
-    }
-
-  }
-
-  if(fullEffort(e)) {
-    // generate the lemmas on the worklist
-    //while(!d_RowQueue.empty() || ! d_extQueue.empty()) {
-    dischargeLemmas();
-    Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
-    //}
-  }
-  Trace("arrays") << "Arrays::check(): done" << endl;
-}
-
-Node TheoryArrays::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
+/////////////////////////////////////////////////////////////////////////////
+// PREPROCESSING
+/////////////////////////////////////////////////////////////////////////////
 
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  default:
-    Unhandled(n.getKind());
-  }
-}
-
-Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  switch(in.getKind()) {
-    case kind::EQUAL:
-    {
-      d_staticFactManager.addEq(in);
-      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
-        outSubstitutions.addSubstitution(in[0], in[1]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
-        outSubstitutions.addSubstitution(in[1], in[0]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      break;
-    }
-    case kind::NOT:
-    {
-      Assert(in[0].getKind() == kind::EQUAL ||
-             in[0].getKind() == kind::IFF );
-      Node a = in[0][0];
-      Node b = in[0][1];
-      d_staticFactManager.addDiseq(in[0]);
-      break;
-    }
-    default:
-      break;
-  }
-  return PP_ASSERT_STATUS_UNSOLVED;
-}
 
-Node TheoryArrays::preprocessTerm(TNode term) {
+Node TheoryArrays::ppRewrite(TNode term) {
+  if (!d_preprocess) return term;
   switch (term.getKind()) {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
       if (term[0].getKind() == kind::STORE &&
-          d_staticFactManager.areDiseq(term[0][1], term[1])) {
+          (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) ||
+           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
       }
       break;
@@ -233,7 +143,8 @@ Node TheoryArrays::preprocessTerm(TNode term) {
       //    IF i != j and j comes before i in the ordering
       if (term[0].getKind() == kind::STORE &&
           (term[1] < term[0][1]) &&
-          d_staticFactManager.areDiseq(term[1], term[0][1])) {
+          (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) ||
+           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
         Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
         return outer;
@@ -241,6 +152,7 @@ Node TheoryArrays::preprocessTerm(TNode term) {
       break;
     }
     case kind::EQUAL: {
+      if (!d_solveWrite) break;
       if (term[0].getKind() == kind::STORE ||
           term[1].getKind() == kind::STORE) {
         TNode left = term[0];
@@ -295,7 +207,8 @@ Node TheoryArrays::preprocessTerm(TNode term) {
                 NodeBuilder<> hyp(kind::AND);
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
-                  if (d_staticFactManager.areDiseq(index_i, index_j)) {
+                  if (d_ppEqualityEngine.areDisequal(index_i, index_j) ||
+                      (index_i.isConst() && index_j.isConst() && index_i != index_j)) {
                     continue;
                   }
                   Node hyp2(index_i.getType() == nm->booleanType()? 
@@ -338,7 +251,7 @@ Node TheoryArrays::preprocessTerm(TNode term) {
           Node l = left;
           Node tmp;
           NodeBuilder<> nb(kind::AND);
-          while (right.getKind() == STORE) {
+          while (right.getKind() == kind::STORE) {
             tmp = nm->mkNode(kind::SELECT, l, right[1]);
             nb << tmp.eqNode(right[2]);
             tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
@@ -357,699 +270,683 @@ Node TheoryArrays::preprocessTerm(TNode term) {
   return term;
 }
 
-Node TheoryArrays::recursivePreprocessTerm(TNode term) {
-  unsigned nc = term.getNumChildren();
-  if (nc == 0 ||
-      (theoryOf(term) != theory::THEORY_ARRAY &&
-       term.getType() != NodeManager::currentNM()->booleanType())) {
-    return term;
-  }
-  NodeMap::iterator find = d_ppCache.find(term);
-  if (find != d_ppCache.end()) {
-    return (*find).second;
-  }
-  NodeBuilder<> newNode(term.getKind());
-  unsigned i;
-  for (i = 0; i < nc; ++i) {
-    newNode << recursivePreprocessTerm(term[i]);
-  }
-  Node newTerm = Rewriter::rewrite(newNode);
-  Node newTerm2 = preprocessTerm(newTerm);
-  if (newTerm != newTerm2) {
-    newTerm = recursivePreprocessTerm(Rewriter::rewrite(newTerm2));
-  }
-  d_ppCache[term] = newTerm;
-  return newTerm;
-}
 
-Node TheoryArrays::ppRewrite(TNode atom) {
-  if (d_donePreregister) return atom;
-  Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str());
-  return recursivePreprocessTerm(atom);
+Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+  switch(in.getKind()) {
+    case kind::EQUAL:
+    {
+      d_ppFacts.push_back(in);
+      d_ppEqualityEngine.addEquality(in[0], in[1], in);
+      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      break;
+    }
+    case kind::NOT:
+    {
+      d_ppFacts.push_back(in);
+      Assert(in[0].getKind() == kind::EQUAL ||
+             in[0].getKind() == kind::IFF );
+      Node a = in[0][0];
+      Node b = in[0][1];
+      d_ppEqualityEngine.addDisequality(a, b, in);
+      break;
+    }
+    default:
+      break;
+  }
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
 
 
-void TheoryArrays::merge(TNode a, TNode b) {
-  Assert(d_conflict.isNull());
+/////////////////////////////////////////////////////////////////////////////
+// T-PROPAGATION / REGISTRATION
+/////////////////////////////////////////////////////////////////////////////
 
-  Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
 
-  /*
-   * take care of the congruence closure part
-   */
+bool TheoryArrays::propagate(TNode literal)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal  << ")" << std::endl;
 
-  // make "a" the one with shorter diseqList
-  CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
-  CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
 
-  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;
+  // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
+  bool satValue = false;
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+  // If asserted, we're done or in conflict
+  if (isAsserted) {
+    if (!satValue) {
+      Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+      std::vector<TNode> assumptions;
+      Node negatedLiteral;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return false;
     }
+    // Propagate even if already known in SAT - could be a new equation between shared terms
+    // (terms that weren't shared when the literal was asserted!)
   }
-  a = find(a);
-  b = find(b);
 
-  if( a == b) {
-    return;
-  }
+  // Nothing, just enqueue it for propagation and mark it as asserted already
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+  d_literalsToPropagate.push_back(literal);
 
+  return true;
+}/* TheoryArrays::propagate(TNode) */
 
-  // 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;
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::SELECT:
+      lhs = literal;
+      rhs = d_true;
+      break;
+    case kind::NOT:
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
         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;
-        }
+        // Predicates
+        lhs = literal[0];
+        rhs = d_false;
+        break;
       }
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
 
+
+  /**
+   * Stores in d_infoMap the following information for each term a of type array:
+   *
+   *    - all i, such that there exists a term a[i] or a = store(b i v)
+   *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
+   *      position i due to the implicit axiom store(b i v)[i] = v )
+   *
+   *    - all the stores a is congruent to (this information is context dependent)
+   *
+   *    - all store terms of the form store (a i v) (i.e. in which a appears
+   *      directly; this is invariant because no new store terms are created)
+   *
+   * Note: completeness depends on having pre-register called on all the input
+   *       terms before starting to instantiate lemmas.
+   */
+void TheoryArrays::preRegisterTerm(TNode node)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
+
+  switch (node.getKind()) {
+  case kind::EQUAL:
+    // Add the terms
+    //    d_equalityEngine.addTerm(node[0]);
+    //    d_equalityEngine.addTerm(node[1]);
+    d_equalityEngine.addTerm(node);
+    // Add the trigger for equality
+    d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+    d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+    break;
+  case kind::SELECT:
+    // Reads
+    d_equalityEngine.addTerm(node);
+    // Maybe it's a predicate
+    // TODO: remove this or keep it if we allow Boolean elements in arrays.
+    if (node.getType().isBoolean()) {
+      // Get triggered for both equal and dis-equal
+      d_equalityEngine.addTriggerEquality(node, d_true, node);
+      d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
     }
-  }
 
-  // TODO: check for equality propagations
-  // a and b are find(a) and find(b) here
-  checkPropagations(a,b);
+    d_infoMap.addIndex(node[0], node[1]);
+    checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0]));
+    d_reads.push_back(node);
+    break;
 
-  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);
-  }
+  case kind::STORE: {
+    d_equalityEngine.addTriggerTerm(node);
 
+    TNode a = node[0];
+    TNode i = node[1];
+    TNode v = node[2];
 
-}
+    d_mayEqualEqualityEngine.addEquality(node, node[0], d_true);
 
+    NodeManager* nm = NodeManager::currentNM();
+    Node ni = nm->mkNode(kind::SELECT, node, i);
+    if (!d_equalityEngine.hasTerm(ni)) {
+      preRegisterTerm(ni);
+    }
 
-void TheoryArrays::checkPropagations(TNode a, TNode b) {
-  EqLists::const_iterator ita = d_equalities.find(a);
-  EqLists::const_iterator itb = d_equalities.find(b);
+    // Apply RIntro1 Rule
+    d_equalityEngine.addEquality(ni, v, d_true);
 
-  if(ita != d_equalities.end()) {
-    if(itb!= d_equalities.end()) {
-      // because b is the canonical representative
-      List<TNode>* eqsa = (*ita).second;
-      List<TNode>* eqsb = (*itb).second;
+    d_infoMap.addStore(node, node);
+    d_infoMap.addInStore(a, node);
 
-      for(List<TNode>::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) {
-        Node eq = *it;
-        Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF);
-        if(find(eq[0])== find(eq[1])) {
-          d_prop_queue.push_back(eq);
-        }
-      }
-     eqsb->concat(eqsa);
+    checkStore(node);
+    break;
+  }
+  default:
+    // Variables etc
+    if (node.getType().isArray()) {
+      d_equalityEngine.addTriggerTerm(node);
     }
     else {
-      List<TNode>* eqsb = new List<TNode>(&d_backtracker);
-      List<TNode>* eqsa = (*ita).second;
-      d_equalities.insert(b, eqsb);
-      eqsb->concat(eqsa);
+      d_equalityEngine.addTerm(node);
     }
-  } else {
-    List<TNode>* eqsb = new List<TNode>(&d_backtracker);
-    d_equalities.insert(b, eqsb);
-    List<TNode>* eqsa = new List<TNode>(&d_backtracker);
-    d_equalities.insert(a, eqsa);
-    eqsb->concat(eqsa);
+    break;
   }
 }
 
 
-bool TheoryArrays::isNonLinear(TNode a) {
-  Assert(a.getType().isArray());
-  const CTNodeList* inst = d_infoMap.getInStores(find(a));
-  if(inst->size()<=1) {
-    return false;
-  }
-  return true;
-}
-
-bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
-  Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n";
-  if(t1.getKind() == kind::SELECT) {
-    TNode a = t1[0];
-    TNode i = t1[1];
-
-    if(a.getKind() == kind::STORE) {
-      TNode b = a[0];
-      TNode j = a[1];
-      TNode v = a[2];
-      if(i == j && v == t2) {
-        Trace("arrays-axiom")<<"Arrays::isAxiom true\n";
-        return true;
+void TheoryArrays::propagate(Effort e)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
+  if (!d_conflict) {
+    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+      Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
+      bool satValue;
+      Node normalized = Rewriter::rewrite(literal);
+      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+        d_out->propagate(literal);
+      } else {
+        Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
+        Node negatedLiteral;
+        std::vector<TNode> assumptions;
+        if (normalized != d_false) {
+          negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+          assumptions.push_back(negatedLiteral);
+        }
+        explain(literal, assumptions);
+        d_conflictNode = mkAnd(assumptions);
+        d_conflict = true;
+        break;
       }
     }
   }
-  return false;
+
 }
 
 
-Node TheoryArrays::constructConflict(TNode diseq) {
-  Trace("arrays") << "arrays: begin constructConflict()" << endl;
-  Trace("arrays") << "arrays:   using diseq == " << diseq << endl;
+Node TheoryArrays::explain(TNode literal)
+{
+  ++d_numExplain;
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(literal, assumptions);
+  return mkAnd(assumptions);
+}
+
 
-  // returns the reason the two terms are equal
-  Node explanation = d_cc.explain(diseq[0], diseq[1]);
+/////////////////////////////////////////////////////////////////////////////
+// SHARING
+/////////////////////////////////////////////////////////////////////////////
 
-  NodeBuilder<> nb(kind::AND);
 
-  if(explanation.getKind() == kind::EQUAL ||
-     explanation.getKind() == kind::IFF) {
-    // if the explanation is only one literal
-    if(!isAxiom(explanation[0], explanation[1]) &&
-       !isAxiom(explanation[1], explanation[0])) {
-      nb<<explanation;
-    }
+void TheoryArrays::addSharedTerm(TNode t) {
+  Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(t);
+  if (t.getType().isArray()) {
+    d_sharedArrays.insert(t,true);
   }
   else {
-    Assert(explanation.getKind() == kind::AND);
-    for(TNode::iterator i  = TNode(explanation).begin();
-        i != TNode(explanation).end(); i++) {
-      if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
-        nb<<*i;
-      }
-    }
+    d_sharedTerms = true;
   }
-
-  nb<<diseq.notNode();
-  Node conflict = nb;
-  Trace("arrays") << "conflict constructed : " << conflict << endl;
-  return conflict;
 }
 
-/*
-void TheoryArrays::addAtom(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL);
-
-  TNode lhs = eq[0];
-  TNode rhs = eq[1];
-
-  appendToAtomList(find(lhs), rhs);
-  appendToAtomList(find(rhs), lhs);
-}
 
-void TheoryArrays::appendToAtomList(TNode a, TNode b) {
-  Assert(find(a) == a);
-
-  NodeTNodesMap::const_iterator it = d_atoms.find(a);
-  if(it != d_atoms.end()) {
-    (*it).second->push_back(b);
+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 {
-   CTNodeList* list = new (true)CTNodeList(getContext());
-   list->push_back(b);
-   d_atoms[a] = list;
+  if (d_equalityEngine.areDisequal(a, b)) {
+    // The terms are implied to be dis-equal
+    return EQUALITY_FALSE;
   }
-
+  //TODO: can we be more precise sometimes?
+  return EQUALITY_UNKNOWN;
 }
-*/
 
-void TheoryArrays::addEq(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-  TNode a = eq[0];
-  TNode b = eq[1];
-
-  // don't need to say find(a) because due to the structure of the lists it gets
-  // automatically added
-  appendToEqList(a, eq);
-  appendToEqList(b, eq);
-
-}
 
-void TheoryArrays::appendToEqList(TNode n, TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-
-  EqLists::const_iterator it = d_equalities.find(n);
-  if(it == d_equalities.end()) {
-    List<TNode>* eqs = new List<TNode>(&d_backtracker);
-    eqs->append(eq);
-    d_equalities.insert(n, eqs);
-  } else {
-    List<TNode>* eqs = (*it).second;
-    eqs->append(eq);
+void TheoryArrays::computeCareGraph()
+{
+  if (d_sharedArrays.size() > 0) {
+    context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+    for (; it1 != iend; ++it1) {
+      for (it2 = it1, ++it2; it2 != iend; ++it2) {
+        EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first);
+        if (eqStatusArr != EQUALITY_UNKNOWN) {
+          continue;
+        }
+        Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN);
+        addCarePair((*it1).first, (*it2).first);
+        ++d_numSharedArrayVarSplits;
+        return;
+      }
+    }
   }
-}
+  if (d_sharedTerms) {
 
-void TheoryArrays::addDiseq(TNode diseq) {
-  Assert(diseq.getKind() == kind::EQUAL ||
-         diseq.getKind() == kind::IFF);
-  TNode a = diseq[0];
-  TNode b = diseq[1];
+    vector< pair<TNode, TNode> > currentPairs;
 
-  appendToDiseqList(find(a), diseq);
-  appendToDiseqList(find(b), diseq);
+    // Go through the read terms and see if there are any to split on
+    unsigned size = d_reads.size();
+    for (unsigned i = 0; i < size; ++ i) {
+      TNode r1 = d_reads[i];
 
-}
+      for (unsigned j = i + 1; j < size; ++ j) {
+        TNode r2 = d_reads[j];
 
-void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
-  Trace("arrays") << "appending " << eq << endl
-              << "  to diseq list of " << of << endl;
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-
-  CNodeTNodesMap::iterator deq_i = d_disequalities.find(of);
-  CTNodeListAlloc* deq;
-  if(deq_i == d_disequalities.end()) {
-    deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false,
-                                             ContextMemoryAllocator<TNode>(getContext()->getCMM()));
-    d_disequalities.insertDataFromContextMemory(of, deq);
-  } else {
-    deq = (*deq_i).second;
-  }
+        Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
 
-  deq->push_back(eq);
-}
+        // If the terms are already known to be equal, we are also in good shape
+        if (d_equalityEngine.areEqual(r1, r2)) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
+          continue;
+        }
 
+        if (r1[0] != r2[0]) {
+          // If arrays are known to be disequal, or cannot become equal, we can continue
+          if (d_equalityEngine.areDisequal(r1[0], r2[0]) ||
+              (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) {
+            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
+            continue;
+          }
+        }
 
-/**
- * Iterates through the indices of a and stores of b and checks if any new
- * Row lemmas need to be instantiated.
- */
-bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) {
-  Assert(a.getType().isArray());
-  Assert(b.getType().isArray());
+        TNode x = r1[1];
+        TNode y = r2[1];
 
-  if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 ||
-     d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) {
-    return true;
-  }
+        EqualityStatus eqStatus = getEqualityStatus(x, y);
 
-  return false;
-}
+        if (eqStatus != EQUALITY_UNKNOWN) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl;
+          continue;
+        }
 
-bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) {
-  NodeManager* nm = NodeManager::currentNM();
-  Node aj = nm->mkNode(kind::SELECT, a, j);
-  Node bj = nm->mkNode(kind::SELECT, b, j);
+        if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
+          continue;
+        }
 
-  if(find(i) == find(j) || find(aj) == find(bj)) {
-    Trace("arrays") << "isRedundantInContext valid "
-                    << a << " " << b << " " << i << " " << j << endl;
-    checkRowForIndex(j, b); // why am i doing this?
-    checkRowForIndex(i, a);
-    return true;
-  }
-  Trace("arrays") << "isRedundantInContext " << a << endl
-                  << "isRedundantInContext " << b << endl
-                  << "isRedundantInContext " << i << endl
-                  << "isRedundantInContext " << j << endl;
-  Node ieqj = i.eqNode(j);
-  Node literal1 = Rewriter::rewrite(ieqj);
-  bool hasValue1, satValue1;
-  Node ff = nm->mkConst<bool>(false);
-  Node tt = nm->mkConst<bool>(true);
-  if (literal1 == ff) {
-    hasValue1 = true;
-    satValue1 = false;
-  } else if (literal1 == tt) {
-    hasValue1 = true;
-    satValue1 = true;
-  } else {
-    hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1));
-  }
-  if (hasValue1) {
-    if (satValue1) {
-      Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl;
-      return true;
-    }
-    Node ajeqbj = aj.eqNode(bj);
-    Node literal2 = Rewriter::rewrite(ajeqbj);
-    bool hasValue2, satValue2;
-    if (literal2 == ff) {
-      hasValue2 = true;
-      satValue2 = false;
-    } else if (literal2 == tt) {
-      hasValue2 = true;
-      satValue2 = true;
-    } else {
-      hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2));
-    }
-    if (hasValue2) {
-      if (satValue2) {
-        Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl;
-        return true;
+        // Get representative trigger terms
+        TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
+        TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
+
+        EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
+        switch (eqStatusDomain) {
+          case EQUALITY_FALSE_AND_PROPAGATED:
+          case EQUALITY_FALSE:
+            continue;
+            break;
+          case EQUALITY_TRUE_AND_PROPAGATED:
+          case EQUALITY_TRUE:
+            // Should have been propagated to us
+            Assert(false);
+            continue;
+            break;
+          case EQUALITY_FALSE_IN_MODEL:
+            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl;
+            continue;
+            break;
+          default:
+            break;
+        }
+
+        // Otherwise, add this pair
+        Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
+        addCarePair(x_shared, y_shared);
       }
-      // conflict
-      Assert(!satValue1 && !satValue2);
-      Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL);
-      NodeBuilder<2> nb(kind::AND);
-      //literal1 = areDisequal(literal1[0], literal1[1]);
-      //literal2 = areDisequal(literal2[0], literal2[1]);
-      Assert(!literal1.isNull() && !literal2.isNull());
-      nb << literal1.notNode() << literal2.notNode();
-      literal1 = nb;
-      d_conflict = Node::null();
-      d_out->conflict(literal1);
-      Trace("arrays") << "TheoryArrays::isRedundantInContext() "
-                      << "conflict via lemma: " << literal1 << endl;
-      return true;
     }
   }
-  if(alreadyAddedRow(a, b, i, j)) {
-    Trace("arrays") << "isRedundantInContext already added "
-                    << a << " " << b << " " << i << " " << j << endl;
-    return true;
-  }
-  return false;
 }
 
-TNode TheoryArrays::areDisequal(TNode a, TNode b) {
-  Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n";
-
-  a = find(a);
-  b = find(b);
-
-  CNodeTNodesMap::const_iterator it = d_disequalities.find(a);
-  if(it!= d_disequalities.end()) {
-    CTNodeListAlloc::const_iterator i = (*it).second->begin();
-    for( ; i!= (*it).second->end(); i++) {
-      Trace("arrays-prop") << "   " << *i << "\n";
-      TNode s = (*i)[0];
-      TNode t = (*i)[1];
-
-      Assert(find(s) == a || find(t) == a);
-      TNode sp, tp;
-      if(find(t) == a) {
-        sp = find(t);
-        tp = find(s);
-      }
-      else {
-        sp = find(s);
-        tp = find(t);
-      }
 
-      if(tp == b) {
-        return *i;
-      }
+/////////////////////////////////////////////////////////////////////////////
+// MODEL GENERATION
+/////////////////////////////////////////////////////////////////////////////
 
-    }
-  }
-  Trace("arrays-prop") << "    not disequal \n";
-  return TNode::null();
-}
 
-bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
-  Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+Node TheoryArrays::getValue(TNode n)
+{
+  // TODO: Implement this
+  NodeManager* nodeManager = NodeManager::currentNM();
 
-  NodeManager* nm = NodeManager::currentNM();
-  Node aj = nm->mkNode(kind::SELECT, a, j);
-  Node bj = nm->mkNode(kind::SELECT, b, j);
+  switch(n.getKind()) {
 
-  Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj);
-  Node eq_ij = nm->mkNode(kind::EQUAL, i, j);
-
-  // first check if the current context implies NOT (i = j)
-  // in which case we can propagate a[j] = b[j]
-  // FIXME: does i = j need to be a SAT literal or can we propagate anyway?
-
-  // if it does not have an atom we must add the lemma (do we?!)
-  if(d_atoms.count(eq_aj_bj) != 0 ||
-     d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) {
-    Node diseq = areDisequal(i, j);
-    // check if the current context implies that (NOT i = j)
-    if(diseq != TNode::null()) {
-      // if it's unassigned
-      Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull();
-      if(d_valuation.getSatValue(eq_aj_bj).isNull()) {
-        d_out->propagate(eq_aj_bj);
-        ++d_numProp;
-        // save explanation
-        d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq));
-        return true;
-      }
+  case kind::VARIABLE:
+    Unhandled(kind::VARIABLE);
 
-    }
-  }
+  case kind::EQUAL: // 2 args
+    return nodeManager->
+      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
 
-  // now check if the current context implies NOT a[j] = b[j]
-  // in which case we propagate i = j
+  default:
+    Unhandled(n.getKind());
+  }
+}
 
-  // we can't propagate if it does not have an atom
-  if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) {
 
-    Node diseq = areDisequal(aj, bj);
-    Assert(TNode::null() == Node::null());
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
 
-    if(diseq != TNode::null()) {
-      if(d_valuation.getSatValue(eq_ij) == Node::null()) {
-        d_out->propagate(eq_ij);
-        ++d_numProp;
-        // save explanation
-        d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq));
-        return true;
-      }
-    }
-  }
 
-  Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
-  return false;
+void TheoryArrays::presolve()
+{
+  Trace("arrays")<<"Presolving \n";
 }
 
-Node TheoryArrays::explain(TNode n) {
 
+/////////////////////////////////////////////////////////////////////////////
+// MAIN SOLVER
+/////////////////////////////////////////////////////////////////////////////
 
-  Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
-  ++d_numExplain;
-
-  Assert(n.getKind()==kind::EQUAL);
 
-  Node explanation = d_cc.explain(n[0], n[1]);
+void TheoryArrays::check(Effort e) {
+  TimerStat::CodeTimer codeTimer(d_checkTimer);
 
-  NodeBuilder<> nb(kind::AND);
+  while (!done() && !d_conflict) 
+  {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
+
+    // If the assertion doesn't have a literal, it's a shared equality
+    Assert(assertion.isPreregistered ||
+           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+    // Do the work
+    switch (fact.getKind()) {
+      case kind::EQUAL:
+        d_equalityEngine.addEquality(fact[0], fact[1], fact);
+        break;
+      case kind::SELECT:
+        d_equalityEngine.addPredicate(fact, true, fact);
+        break;
+      case kind::NOT:
+        if (fact[0].getKind() == kind::SELECT) {
+          d_equalityEngine.addPredicate(fact[0], false, fact);
+        } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
+          // Assert the dis-equality
+          d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+
+          // Apply ArrDiseq Rule if diseq is between arrays
+          if(fact[0][0].getType().isArray()) {
+            NodeManager* nm = NodeManager::currentNM();
+            TypeNode indexType = fact[0][0].getType()[0];
+            TNode k;
+            std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
+            if (it == d_diseqCache.end()) {
+              Node newk = nm->mkVar(indexType);
+	      Dump.declareVar(newk.toExpr(),
+                              "an extensional lemma index variable from the theory of arrays");
+              d_diseqCache[fact] = newk;
+              k = newk;
+            }
+            else {
+              k = (*it).second;
+            }
 
-  if(explanation.getKind() == kind::EQUAL ||
-     explanation.getKind() == kind::IFF) {
-    // if the explanation is only one literal
-    if(!isAxiom(explanation[0], explanation[1]) &&
-       !isAxiom(explanation[1], explanation[0])) {
-      nb<<explanation;
+            Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
+            Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
+            if (!d_equalityEngine.hasTerm(ak)) {
+              preRegisterTerm(ak);
+            }
+            if (!d_equalityEngine.hasTerm(bk)) {
+              preRegisterTerm(bk);
+            }
+            d_equalityEngine.addDisequality(ak, bk, fact);
+            Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
+            ++d_numExt;
+          }
+        }
+        break;
+      default:
+        Unreachable();
     }
   }
+
+  // If in conflict, output the conflict
+  if (d_conflict) {
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
+    d_out->conflict(d_conflictNode);
+  }
   else {
-    Assert(explanation.getKind() == kind::AND);
-    for(TNode::iterator i  = TNode(explanation).begin();
-        i != TNode(explanation).end(); i++) {
-      if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
-        nb<<*i;
-      }
+    // Otherwise we propagate
+    propagate(e);
+
+    if(!d_eagerLemmas && fullEffort(e)) {
+      // generate the lemmas on the worklist
+      Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+      dischargeLemmas();
     }
   }
-  Node reason = nb;
-
-  return reason;
-
-  /*
-  context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator
-                                                    it = d_explanations.find(n);
-  Assert(it!= d_explanations.end());
-  TNode diseq = (*it).second.second;
-  TNode s = diseq[0];
-  TNode t = diseq[1];
 
-  TNode eq = (*it).second.first;
-  TNode a = eq[0];
-  TNode b = eq[1];
+  Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl;
+}
 
-  Assert ((find(a) == find(s) && find(b) == find(t)) ||
-          (find(a) == find(t) && find(b) == find(s)));
 
+Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
+{
+  Assert(conjunctions.size() > 0);
 
-  if(find(a) == find(t)) {
-    TNode temp = t;
-    t = s;
-    s = temp;
-  }
+  std::set<TNode> all;
+  std::set<TNode> explained;
 
-  // construct the explanation
+  unsigned i = 0;
+  TNode t;
+  for (; i < conjunctions.size(); ++i) {
+    t = conjunctions[i];
 
-  NodeBuilder<> nb(kind::AND);
-  Node explanation1 = d_cc.explain(a, s);
-  Node explanation2 = d_cc.explain(b, t);
+    // Remove true node - represents axiomatically true assertion
+    if (t == d_true) continue;
 
-  if(explanation1.getKind() == kind::AND) {
-    for(TNode::iterator i= TNode(explanation1).begin();
-        i!=TNode(explanation1).end(); ++i) {
-      nb << *i;
+    // Expand explanation resulting from propagating a ROW lemma
+    if (t.getKind() == kind::OR) {
+      if ((explained.find(t) == explained.end())) {
+        Assert(t[1].getKind() == kind::EQUAL);
+        d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions);
+        explained.insert(t);
+      }
+      continue;
     }
-  } else {
-    Assert(explanation1.getKind() == kind::EQUAL ||
-           explanation1.getKind() == kind::IFF);
-    nb << explanation1;
+    all.insert(t);
   }
 
-  if(explanation2.getKind() == kind::AND) {
-    for(TNode::iterator i= TNode(explanation2).begin();
-        i!=TNode(explanation2).end(); ++i) {
-      nb << *i;
-    }
-  } else {
-    Assert(explanation2.getKind() == kind::EQUAL ||
-           explanation2.getKind() == kind::IFF);
-    nb << explanation2;
+  Assert(all.size() > 0);
+  if (all.size() == 1) {
+    // All the same, or just one
+    return *(all.begin());
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
   }
 
-  nb << diseq;
-  Node reason = nb;
-  d_out->explanation(reason);
-  Trace("arrays")<<"explanation "<< reason<<" done \n";
-  */
+  return conjunction;
 }
 
-void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
 
-  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
-  if(Trace.isOn("arrays-crl"))
-    d_infoMap.getInfo(a)->print();
-  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
-  if(Trace.isOn("arrays-crl"))
-    d_infoMap.getInfo(b)->print();
+void TheoryArrays::setNonLinear(TNode a)
+{
+  if (d_infoMap.isNonLinear(a)) return;
+
+  Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
+  d_infoMap.setNonLinear(a);
+  ++d_numNonLinear;
 
   List<TNode>* i_a = d_infoMap.getIndices(a);
-  const CTNodeList* st_b = d_infoMap.getStores(b);
-  const CTNodeList* inst_b = d_infoMap.getInStores(b);
+  const CTNodeList* st_a = d_infoMap.getStores(a);
+  const CTNodeList* inst_a = d_infoMap.getInStores(a);
 
-  List<TNode>::const_iterator it = i_a->begin();
-  CTNodeList::const_iterator its;
+  CTNodeList::const_iterator it = st_a->begin();
 
-  for( ; it != i_a->end(); it++ ) {
-    TNode i = *it;
-    its = st_b->begin();
-    for ( ; its != st_b->end(); its++) {
-      TNode store = *its;
+  // Propagate non-linearity down chain of stores
+  for(; it!= st_a->end(); ++it) {
+    TNode store = *it;
+    Assert(store.getKind()==kind::STORE);
+    setNonLinear(store[0]);
+  }
+
+  // Instantiate ROW lemmas that were ignored before
+  List<TNode>::const_iterator itl = i_a->begin();
+  RowLemmaType lem;
+  for(; itl != i_a->end(); ++itl ) {
+    TNode i = *itl;
+    it = inst_a->begin();
+    for ( ; it !=inst_a->end(); ++it) {
+      TNode store = *it;
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-
-      if(  !isRedundantRowLemma(store, c, j, i)){
-         //&&!propagateFromRow(store, c, j, i)) {
-        queueRowLemma(store, c, j, i);
-      }
+      lem = make_quad(store, c, j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
-
   }
 
-  it = i_a->begin();
+}
 
-  for( ; it != i_a->end(); it++ ) {
-    TNode i = *it;
-    its = inst_b->begin();
-    for ( ; its !=inst_b->end(); its++) {
-      TNode store = *its;
-      Assert(store.getKind() == kind::STORE);
-      TNode j = store[1];
-      TNode c = store[0];
 
-      if (   isNonLinear(c)
-          &&!isRedundantRowLemma(store, c, j, i)){
-          //&&!propagateFromRow(store, c, j, i)) {
-        queueRowLemma(store, c, j, i);
+void TheoryArrays::mergeArrays(TNode a, TNode b)
+{
+  // Note: a is the new representative
+  Assert(a.getType().isArray() && b.getType().isArray());
+
+  if (d_mergeInProgress) {
+    // Nested call to mergeArrays, just push on the queue and return
+    d_mergeQueue.push(a.eqNode(b));
+    return;
+  }
+
+  d_mergeInProgress = true;
+
+  Node n;
+  while (true) {
+    if (d_useNonLinearOpt) {
+      bool aNL = d_infoMap.isNonLinear(a);
+      bool bNL = d_infoMap.isNonLinear(b);
+      if (aNL) {
+        if (bNL) {
+          // already both marked as non-linear - no need to do anything
+        }
+        else {
+          // Set b to be non-linear
+          setNonLinear(b);
+        }
       }
+      else {
+        if (bNL) {
+          // Set a to be non-linear
+          setNonLinear(a);
+        }
+        else {
+          // Check for new non-linear arrays
+          const CTNodeList* astores = d_infoMap.getStores(a);
+          const CTNodeList* bstores = d_infoMap.getStores(a);
+          Assert(astores->size() <= 1 && bstores->size() <= 1);
+          if (astores->size() > 0 && bstores->size() > 0) {
+            setNonLinear(a);
+            setNonLinear(b);
+          }
+        }
+      }
+    }
+
+    d_mayEqualEqualityEngine.addEquality(a, b, d_true);
 
+    checkRowLemmas(a,b);
+    checkRowLemmas(b,a);
+
+    // merge info adds the list of the 2nd argument to the first
+    d_infoMap.mergeInfo(a, b);
+
+    // If no more to do, break
+    if (d_conflict || d_mergeQueue.empty()) {
+      break;
     }
-  }
 
-  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
+    // Otherwise, prepare for next iteration
+    n = d_mergeQueue.front();
+    a = n[0];
+    b = n[1];
+    d_mergeQueue.pop();
+  }
+  d_mergeInProgress = false;
 }
 
-/**
- * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the
- * same and a and b are also not identical.
- *
- */
-
-inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
 
- // construct lemma
- NodeManager* nm = NodeManager::currentNM();
- Node aj = nm->mkNode(kind::SELECT, a, j);
- Node bj = nm->mkNode(kind::SELECT, b, j);
- Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
- Node eq2 = nm->mkNode(kind::EQUAL, i, j);
- Node lem = nm->mkNode(kind::OR, eq2, eq1);
+void TheoryArrays::checkStore(TNode a) {
+  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
+  if(Trace.isOn("arrays-cri")) {
+    d_infoMap.getInfo(a)->print();
+  }
+  Assert(a.getType().isArray());
+  Assert(a.getKind()==kind::STORE);
+  TNode b = a[0];
+  TNode i = a[1];
 
+  TNode brep = d_equalityEngine.getRepresentative(b);
 
- Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
- d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
- d_out->lemma(lem);
- ++d_numRow;
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) {
+    List<TNode>* js = d_infoMap.getIndices(brep);
+    List<TNode>::const_iterator it = js->begin();
 
+    RowLemmaType lem;
+    for(; it!= js->end(); ++it) {
+      TNode j = *it;
+      if (i == j) continue;
+      lem = make_quad(a,b,i,j);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+      queueRowLemma(lem);
+    }
+  }
 }
 
 
-/**
- * Because a is now being read at position i check if new lemmas can be
- * instantiated for all store terms equal to a and all store terms of the form
- * store(a _ _ )
- */
-void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
+void TheoryArrays::checkRowForIndex(TNode i, TNode a)
+{
   Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
   Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
@@ -1057,107 +954,207 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
+  Assert(d_equalityEngine.getRepresentative(a) == a);
 
   const CTNodeList* stores = d_infoMap.getStores(a);
   const CTNodeList* instores = d_infoMap.getInStores(a);
   CTNodeList::const_iterator it = stores->begin();
+  RowLemmaType lem;
 
-  for(; it!= stores->end(); it++) {
+  for(; it!= stores->end(); ++it) {
     TNode store = *it;
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
-    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundantRowLemma(store, store[0], j, i)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
-      queueRowLemma(store, store[0], j, i);
-    }
+    if (i == j) continue;
+    lem = make_quad(store, store[0], j, i);
+    Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+    queueRowLemma(lem);
   }
 
-  it = instores->begin();
-  for(; it!= instores->end(); it++) {
-    TNode instore = *it;
-    Assert(instore.getKind()==kind::STORE);
-    TNode j = instore[1];
-    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundantRowLemma(instore, instore[0], j, i)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
-      queueRowLemma(instore, instore[0], j, i);
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(a)) {
+    it = instores->begin();
+    for(; it!= instores->end(); ++it) {
+      TNode instore = *it;
+      Assert(instore.getKind()==kind::STORE);
+      TNode j = instore[1];
+      if (i == j) continue;
+      lem = make_quad(instore, instore[0], j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
   }
-
 }
 
 
-void TheoryArrays::checkStore(TNode a) {
-  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
-
-  if(Trace.isOn("arrays-cri")) {
+// a just became equal to b
+// look for new ROW lemmas
+void TheoryArrays::checkRowLemmas(TNode a, TNode b)
+{
+  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
+  if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
-  }
-  Assert(a.getType().isArray());
-  Assert(a.getKind()==kind::STORE);
-  TNode b = a[0];
-  TNode i = a[1];
+  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
+  if(Trace.isOn("arrays-crl"))
+    d_infoMap.getInfo(b)->print();
 
-  List<TNode>* js = d_infoMap.getIndices(b);
-  List<TNode>::const_iterator it = js->begin();
+  List<TNode>* i_a = d_infoMap.getIndices(a);
+  const CTNodeList* st_b = d_infoMap.getStores(b);
+  const CTNodeList* inst_b = d_infoMap.getInStores(b);
+
+  List<TNode>::const_iterator it = i_a->begin();
+  CTNodeList::const_iterator its;
 
-  for(; it!= js->end(); it++) {
-    TNode j = *it;
+  RowLemmaType lem;
 
-    if(!isRedundantRowLemma(a, b, i, j)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
-      queueRowLemma(a,b,i,j);
+  for( ; it != i_a->end(); ++it ) {
+    TNode i = *it;
+    its = st_b->begin();
+    for ( ; its != st_b->end(); ++its) {
+      TNode store = *its;
+      Assert(store.getKind() == kind::STORE);
+      TNode j = store[1];
+      TNode c = store[0];
+      lem = make_quad(store, c, j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
   }
 
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(b)) {
+    for(it = i_a->begin() ; it != i_a->end(); ++it ) {
+      TNode i = *it;
+      its = inst_b->begin();
+      for ( ; its !=inst_b->end(); ++its) {
+        TNode store = *its;
+        Assert(store.getKind() == kind::STORE);
+        TNode j = store[1];
+        TNode c = store[0];
+        lem = make_quad(store, c, j, i);
+        Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+        queueRowLemma(lem);
+      }
+    }
+  }
+  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-inline void TheoryArrays::queueExtLemma(TNode a, TNode b) {
+
+void TheoryArrays::queueRowLemma(RowLemmaType lem)
+{
+  if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+    return;
+  }
+  TNode a = lem.first;
+  TNode b = lem.second;
+  TNode i = lem.third;
+  TNode j = lem.fourth;
   Assert(a.getType().isArray() && b.getType().isArray());
+  if (d_equalityEngine.areEqual(a,b) ||
+      d_equalityEngine.areEqual(i,j)) {
+    return;
+  }
 
-  d_extQueue.insert(make_pair(a,b));
-}
+  NodeManager* nm = NodeManager::currentNM();
 
-void TheoryArrays::queueRowLemma(TNode a, TNode b, TNode i, TNode j) {
-  Assert(a.getType().isArray() && b.getType().isArray());
-//if(!isRedundantInContext(a,b,i,j)) {
-  d_RowQueue.insert(make_quad(a, b, i, j));
-}
+  Node aj = nm->mkNode(kind::SELECT, a, j);
+  Node bj = nm->mkNode(kind::SELECT, b, j);
+  if (!d_equalityEngine.hasTerm(aj)) {
+    preRegisterTerm(aj);
+  }
+  if (!d_equalityEngine.hasTerm(bj)) {
+    preRegisterTerm(bj);
+  }
+
+  if (d_equalityEngine.areEqual(aj,bj)) {
+    return;
+  }
+
+  if (d_useArrTable) {
+    Node tableEntry = nm->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
+    if (d_equalityEngine.getSize(tableEntry) != 1) {
+      return;
+    }
+  }
 
-/**
-* Adds a new Ext lemma of the form
-*    a = b OR a[k]!=b[k], for a new variable k
-*/
+  //Propagation
+  if (d_propagateLemmas) {
+    if (d_equalityEngine.areDisequal(i,j)) {
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
+      Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j));
+      d_permRef.push_back(reason);
+      d_equalityEngine.addEquality(aj, bj, reason);
+      ++d_numProp;
+      return;
+    }
+    if (d_equalityEngine.areDisequal(aj,bj)) {
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
+      Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
+      d_permRef.push_back(reason);
+      d_equalityEngine.addEquality(i, j, reason);
+      ++d_numProp;
+      return;
+    }
+  }
 
-inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
+  // TODO: maybe add triggers here
 
- Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
- Trace("arrays-cle")<<"                   and "<<b<<" \n";
+  if (d_eagerLemmas) {
+    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+    Node lemma = nm->mkNode(kind::OR, eq2, eq1);
+    Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n";
+    d_RowAlreadyAdded.insert(lem);
+    d_out->lemma(lemma);
+    ++d_numRow;
+  }
+  else {
+    d_RowQueue.push(lem);
+  }
+}
 
 
- if(   d_extAlreadyAdded.count(make_pair(a, b)) == 0
-    && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
+void TheoryArrays::dischargeLemmas()
+{
+  size_t sz = d_RowQueue.size();
+  for (unsigned count = 0; count < sz; ++count) {
+    RowLemmaType l = d_RowQueue.front();
+    d_RowQueue.pop();
+    if (d_RowAlreadyAdded.count(l) != 0) {
+      continue;
+    }
 
-   NodeManager* nm = NodeManager::currentNM();
-   TypeNode ixType = a.getType()[0];
-   Node k = nm->mkVar(ixType);
-   Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays");
-   Node eq = nm->mkNode(kind::EQUAL, a, b);
-   Node ak = nm->mkNode(kind::SELECT, a, k);
-   Node bk = nm->mkNode(kind::SELECT, b, k);
-   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk));
-   Node lem = nm->mkNode(kind::OR, eq, neq);
+    TNode a = l.first;
+    TNode b = l.second;
+    TNode i = l.third;
+    TNode j = l.fourth;
+    Assert(a.getType().isArray() && b.getType().isArray());
+
+    NodeManager* nm = NodeManager::currentNM();
+    Node aj = nm->mkNode(kind::SELECT, a, j);
+    Node bj = nm->mkNode(kind::SELECT, b, j);
+
+    // Check for redundant lemma
+    // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
+    if (d_equalityEngine.areEqual(i,j) ||
+        d_equalityEngine.areEqual(a,b) ||
+        d_equalityEngine.areEqual(aj,bj)) {
+      d_RowQueue.push(l);
+      continue;
+    }
 
-   Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
-   d_extAlreadyAdded.insert(make_pair(a,b));
-   d_out->lemma(lem);
-   ++d_numExt;
-   return;
- }
+    // construct lemma
+    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+    Node lem = nm->mkNode(kind::OR, eq2, eq1);
 
- Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+    Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
+    d_RowAlreadyAdded.insert(l);
+    d_out->lemma(lem);
+    ++d_numRow;
+  }
 }
 
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index dcae47dc7..12dbd771d 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -2,7 +2,7 @@
 /*! \file theory_arrays.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: lianah
  ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -22,17 +22,12 @@
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
 #include "theory/theory.h"
-#include "theory/arrays/union_find.h"
-#include "util/congruence_closure.h"
 #include "theory/arrays/array_info.h"
-#include "util/hash.h"
-#include "util/ntuple.h"
 #include "util/stats.h"
-#include "util/backtrackable.h"
-#include "theory/arrays/static_fact_manager.h"
-
-#include <iostream>
-#include <map>
+#include "theory/uf/equality_engine.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,417 +82,237 @@ namespace arrays {
  *  check. Ext lemmas are stored in a cache to prevent instantiating essentially
  *  the same lemma multiple times.
  */
-class TheoryArrays : public Theory {
 
-private:
+static inline std::string spaces(int level)
+{
+  std::string indentStr(level, ' ');
+  return indentStr;
+}
 
+class TheoryArrays : public Theory {
 
-  class CongruenceChannel {
-    TheoryArrays* d_arrays;
+  /////////////////////////////////////////////////////////////////////////////
+  // MISC
+  /////////////////////////////////////////////////////////////////////////////
 
-  public:
-    CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {}
-    void notifyCongruent(TNode a, TNode b) {
-      d_arrays->notifyCongruent(a, b);
-    }
-  }; /* class CongruenceChannel*/
-  friend class CongruenceChannel;
+  private:
 
-  /**
-   * Output channel connected to the congruence closure module.
-   */
-  CongruenceChannel d_ccChannel;
+  /** True node for predicates = true */
+  Node d_true;
 
-  /**
-   * Instance of the congruence closure module.
-   */
-  CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1
-                                 (kind::SELECT)> d_cc;
+  /** True node for predicates = false */
+  Node d_false;
 
-  /**
-   * (Temporary) fact manager for preprocessing - eventually handle this with
-   * something more standard (like congruence closure module)
-   */
-  StaticFactManager d_staticFactManager;
+  // Statistics
 
-  /**
-   * Cache for proprocessing of atoms.
-   */
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_ppCache;
+  /** number of Row lemmas */
+  IntStat d_numRow;
+  /** number of Ext lemmas */
+  IntStat d_numExt;
+  /** number of propagations */
+  IntStat d_numProp;
+  /** number of explanations */
+  IntStat d_numExplain;
+  /** calls to non-linear */
+  IntStat d_numNonLinear;
+  /** splits on array variables */
+  IntStat d_numSharedArrayVarSplits;
+  /** time spent in check() */
+  TimerStat d_checkTimer;
 
-  /**
-   * Union find for storing the equalities.
-   */
+  public:
 
-  UnionFind<Node, NodeHashFunction> d_unionFind;
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+  ~TheoryArrays();
 
-  Backtracker<TNode> d_backtracker;
+  std::string identify() const { return std::string("TheoryArrays"); }
 
+  /////////////////////////////////////////////////////////////////////////////
+  // PREPROCESSING
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Context dependent map from a congruence class canonical representative of
-   * type array to an Info pointer that keeps track of information useful to axiom
-   * instantiation
-   */
+  private:
 
-  ArrayInfo d_infoMap;
+  // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
+  class PPNotifyClass {
+  public:
+    bool notify(TNode propagation) { return true; }
+    void notify(TNode t1, TNode t2) { }
+  };
 
-  /**
-   * Received a notification from the congruence closure algorithm that the two
-   * nodes a and b have become congruent.
-   */
+  /** The notify class for d_ppEqualityEngine */
+  PPNotifyClass d_ppNotify;
 
-  void notifyCongruent(TNode a, TNode b);
+  /** Equaltity engine */
+  uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine;
 
+  // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
+  context::CDList<Node> d_ppFacts;
 
-  typedef context::CDChunkList<TNode> CTNodeListAlloc;
-  typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
-  typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+  Node preprocessTerm(TNode term);
+  Node recursivePreprocessTerm(TNode term);
 
+  public:
 
-  typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap;
-  /**
-   * List of all disequalities this theory has seen. Maintains the invariant that
-   * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map
-   * */
-  CNodeTNodesMap d_disequalities;
-  EqLists d_equalities;
-  context::CDList<TNode> d_prop_queue;
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  Node ppRewrite(TNode atom);
 
-  void checkPropagations(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // T-PROPAGATION / REGISTRATION
+  /////////////////////////////////////////////////////////////////////////////
 
-  /** List of all atoms the SAT solver knows about and are candidates for
-   *  propagation. */
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
+  private:
 
-  /** List of disequalities needed to construct explanations for propagated
-   * row lemmas */
+  /** Literals to propagate */
+  context::CDList<Node> d_literalsToPropagate;
 
-  context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  /**
-   * stores the conflicting disequality (still need to call construct
-   * conflict to get the actual explanation)
-   */
-  Node d_conflict;
+  /** Should be called to propagate the literal.  */
+  bool propagate(TNode literal);
 
-  typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList;
+  /** Explain why this literal is true by adding assumptions */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
 
+  public:
 
-  /**
-   * Ext lemma workslist that stores extensionality lemmas that still need to be added
-   */
-  std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue;
+  void preRegisterTerm(TNode n);
+  void propagate(Effort e);
+  Node explain(TNode n);
 
-  /**
-   * Row Lemma worklist, stores lemmas that can still be added to the SAT solver
-   * to be emptied during full effort check
-   */
-  std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowQueue;
+  /////////////////////////////////////////////////////////////////////////////
+  // SHARING
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Extensionality lemma cache which stores the array pair (a,b) for which
-   * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver.
-   */
-  std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extAlreadyAdded;
+  private:
 
-  /**
-   * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a
-   * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed
-   * to prevent infinite recursion in addRowLemma.
-   */
-  std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowAlreadyAdded;
+  class MayEqualNotifyClass {
+  public:
+    bool notify(TNode propagation) { return true; }
+    void notify(TNode t1, TNode t2) { }
+  };
 
-  /*
-   * Congruence helper methods
-   */
+  /** The notify class for d_mayEqualEqualityEngine */
+  MayEqualNotifyClass d_mayEqualNotify;
 
-  void addDiseq(TNode diseq);
-  void addEq(TNode eq);
+  /** Equaltity engine for determining if two arrays might be equal */
+  uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine;
 
-  void appendToDiseqList(TNode of, TNode eq);
-  void appendToEqList(TNode a, TNode b);
-  Node constructConflict(TNode diseq);
+  public:
 
-  /**
-   * Merges two congruence classes in the internal union-find and checks for a
-   * conflict.
-   */
+  void addSharedTerm(TNode t);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void computeCareGraph();
+  bool isShared(TNode t)
+    { return (d_sharedArrays.find(t) != d_sharedArrays.end()); }
 
-  void merge(TNode a, TNode b);
-  inline TNode find(TNode a);
-  inline TNode debugFind(TNode a) const;
 
-  inline void setCanon(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // MODEL GENERATION
+  /////////////////////////////////////////////////////////////////////////////
 
-  void queueRowLemma(TNode a, TNode b, TNode i, TNode j);
-  inline void queueExtLemma(TNode a, TNode b);
+  private:
+  public:
 
-  /**
-   * Adds a Row lemma of the form:
-   *    i = j OR a[j] = b[j]
-   */
-  void addRowLemma(TNode a, TNode b, TNode i, TNode j);
+  Node getValue(TNode n);
 
-  /**
-   * Adds a new Ext lemma of the form
-   *    a = b OR a[k]!=b[k], for a new variable k
-   */
-  void addExtLemma(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Because Row1 axioms of the form (store a i v) [i] = v are not added as
-   * explicitly but are kept track of internally, is axiom recognizez an axiom
-   * of the above form given the two terms in the equality.
-   */
-  bool isAxiom(TNode lhs, TNode rhs);
+  private:
+  public:
 
+  void presolve();
+  void shutdown() { }
 
-  bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j);
-  bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
+  /////////////////////////////////////////////////////////////////////////////
+  // MAIN SOLVER
+  /////////////////////////////////////////////////////////////////////////////
 
+  public:
 
+  void check(Effort e);
 
-  bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
-    //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin();
-    a = find(a);
-    b = find(b);
-    i = find(i);
-    j = find(j);
+  private:
 
-    for( ; it!= d_RowAlreadyAdded.end(); it++) {
+  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+  class NotifyClass {
+    TheoryArrays& d_arrays;
+  public:
+    NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 
-      TNode a_ = find((*it).first);
-      TNode b_ = find((*it).second);
-      TNode i_ = find((*it).third);
-      TNode j_ = find((*it).fourth);
-      if( a == a_ && b == b_ && i==i_ && j==j_) {
-        //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
-        return true;
-      }
+    bool notify(TNode propagation) {
+      Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+      // Just forward to arrays
+      return d_arrays.propagate(propagation);
     }
-    return false;
-  }
-
-
-  bool isNonLinear(TNode n);
-
-  /**
-   * Checks if any new Row lemmas need to be generated after merging arrays a
-   * and b; called after setCanon.
-   */
-  void checkRowLemmas(TNode a, TNode b);
-
-  /**
-   * Called after a new select term a[i] is created to check whether new Row
-   * lemmas need to be instantiated.
-   */
-  void checkRowForIndex(TNode i, TNode a);
-
-  void checkStore(TNode a);
-  /**
-   * Lemma helper functions to prevent changing the list we are iterating through.
-   */
 
-  void insertInQuadQueue(std::set<quad<TNode, TNode, TNode, TNode> >& queue, TNode a, TNode b, TNode i, TNode j){
-    if(i != j) {
-      queue.insert(make_quad(a,b,i,j));
-    }
-  }
-
-  void dischargeLemmas() {
-    // we need to swap the temporary lists because adding a lemma calls preregister
-    // which might modify the d_RowQueue we would be iterating through
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > temp_Row;
-    temp_Row.swap(d_RowQueue);
-
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin();
-    for( ; it1!= temp_Row.end(); it1++) {
-      if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) {
-        addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
-      }
-      else {
-        // add it to queue may be needed later
-        queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
+    void notify(TNode t1, TNode t2) {
+      Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      if (t1.getType().isArray()) {
+        d_arrays.mergeArrays(t1, t2);
+        if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
+          return;
+        }
       }
+      // Propagate equality between shared terms
+      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+      d_arrays.propagate(equality);
     }
+  };
 
-    std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction>  temp_ext;
-    temp_ext.swap(d_extQueue);
 
-    std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin();
-    for(; it2 != temp_ext.end(); it2++) {
-      addExtLemma((*it2).first, (*it2).second);
-    }
-  }
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
 
-  /** Checks if instead of adding a lemma of the form i = j OR  a[j] = b[j]
-   * we can propagate either i = j or NOT a[j] = b[j] and does the propagation.
-   * Returns whether it did propagate.
-   */
-  bool propagateFromRow(TNode a, TNode b, TNode i, TNode j);
+  /** Equaltity engine */
+  uf::EqualityEngine<NotifyClass> d_equalityEngine;
 
-  TNode areDisequal(TNode a, TNode b);
-
-
-
-  /*
-   * === STATISTICS ===
-   */
+  // Are we in conflict?
+  context::CDO<bool> d_conflict;
 
-  /** number of Row lemmas */
-  IntStat d_numRow;
-  /** number of Ext lemmas */
-  IntStat d_numExt;
-
-  /** number of propagations */
-  IntStat d_numProp;
-  IntStat d_numExplain;
-  /** time spent in check() */
-  TimerStat d_checkTimer;
-
-  bool d_donePreregister;
-
-  Node preprocessTerm(TNode term);
-  Node recursivePreprocessTerm(TNode term);
-
-public:
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
-  ~TheoryArrays();
+  /** The conflict node */
+  Node d_conflictNode;
 
   /**
-   * Stores in d_infoMap the following information for each term a of type array:
-   *
-   *    - all i, such that there exists a term a[i] or a = store(b i v)
-   *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
-   *      position i due to the implicit axiom store(b i v)[i] = v )
-   *
-   *    - all the stores a is congruent to (this information is context dependent)
-   *
-   *    - all store terms of the form store (a i v) (i.e. in which a appears
-   *      directly; this is invariant because no new store terms are created)
-   *
-   * Note: completeness depends on having pre-register called on all the input
-   *       terms before starting to instantiate lemmas.
+   * Context dependent map from a congruence class canonical representative of
+   * type array to an Info pointer that keeps track of information useful to axiom
+   * instantiation
    */
-  void preRegisterTerm(TNode n) {
-    //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
-    Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
-    //TODO: check non-linear arrays with an AlwaysAssert!!!
-    //if(n.getType().isArray())
-
-    switch(n.getKind()) {
-    case kind::EQUAL:
-      // stores the seen atoms for propagation
-      Trace("arrays-preregister")<<"atom "<<n<<"\n";
-      d_atoms.insert(n);
-      // add to proper equality lists
-      addEq(n);
-      break;
-    case kind::SELECT:
-      //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
-      d_infoMap.addIndex(n[0], n[1]);
-      checkRowForIndex(n[1], find(n[0]));
-      //Trace("arrays-preregister")<<"n[0] \n";
-      //d_infoMap.getInfo(n[0])->print();
-      //Trace("arrays-preregister")<<"find(n[0]) \n";
-      //d_infoMap.getInfo(find(n[0]))->print();
-      break;
-
-    case kind::STORE:
-    {
-      // this should always be called at level0 since we do not create new store terms
-      TNode a = n[0];
-      TNode i = n[1];
-      TNode v = n[2];
-
-      NodeManager* nm = NodeManager::currentNM();
-      Node ni = nm->mkNode(kind::SELECT, n, i);
-      Node eq = nm->mkNode(kind::EQUAL, ni, v);
-
-      d_cc.addEquality(eq);
-
-      d_infoMap.addIndex(n, i);
-      d_infoMap.addStore(n, n);
-      d_infoMap.addInStore(a, n);
-
-      checkStore(n);
-
-      break;
-    }
-    default:
-      Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
-    }
-  }
 
-  //void registerTerm(TNode n) {
-  //  Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
-  //}
+  Backtracker<TNode> d_backtracker;
+  ArrayInfo d_infoMap;
 
-  void presolve() {
-    Trace("arrays")<<"Presolving \n";
-    d_donePreregister = true;
-  }
+  context::CDQueue<Node> d_mergeQueue;
 
-  void addSharedTerm(TNode t);
-  void notifyEq(TNode lhs, TNode rhs);
-  void check(Effort e);
+  bool d_mergeInProgress;
 
-  void propagate(Effort e) {
+  typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
-    // Trace("arrays-prop")<<"Propagating \n";
+  context::CDQueue<RowLemmaType> d_RowQueue;
+  context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
 
-    // context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
-    /*
-    for(; it!= d_prop_queue.end(); it++) {
-      TNode eq = *it;
-      if(d_valuation.getSatValue(eq).isNull()) {
-        //FIXME remove already propagated literals?
-        d_out->propagate(eq);
-        ++d_numProp;
-      }
-    }*/
-    //d_prop_queue.deleteSelf();
-    /*
-    __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator it = d_atoms.begin();
-
-    for(; it!= d_atoms.end(); it++) {
-      TNode eq = *it;
-      Assert(eq.getKind()==kind::EQUAL);
-      Trace("arrays-prop")<<"value of "<<eq<<" ";
-      Trace("arrays-prop")<<d_valuation.getSatValue(eq);
-      if(find(eq[0]) == find(eq[1])) {
-        Trace("arrays-prop")<<" eq \n";
-        ++d_numProp;
-      }
-    }
-    */
+  context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays;
+  context::CDO<bool> d_sharedTerms;
+  context::CDList<TNode> d_reads;
+  std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
 
-  }
-  Node explain(TNode n);
+  // List of nodes that need permanent references in this context
+  context::CDList<Node> d_permRef;
 
-  Node getValue(TNode n);
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
-  void shutdown() { }
-  std::string identify() const { return std::string("TheoryArrays"); }
+  Node mkAnd(std::vector<TNode>& conjunctions);
+  void setNonLinear(TNode a);
+  void mergeArrays(TNode a, TNode b);
+  void checkStore(TNode a);
+  void checkRowForIndex(TNode i, TNode a);
+  void checkRowLemmas(TNode a, TNode b);
+  void queueRowLemma(RowLemmaType lem);
+  void dischargeLemmas();
 
 };/* class TheoryArrays */
 
-inline void TheoryArrays::setCanon(TNode a, TNode b) {
-  d_unionFind.setCanon(a, b);
-}
-
-inline TNode TheoryArrays::find(TNode a) {
-  return d_unionFind.find(a);
-}
-
-inline TNode TheoryArrays::debugFind(TNode a) const {
-  return d_unionFind.debugFind(a);
-}
-
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index f3a19ff02..627f34a30 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -36,11 +36,22 @@ public:
     Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
     switch (node.getKind()) {
       case kind::SELECT: {
-        // select(store(a,i,v),i) = v
         TNode store = node[0];
-        if (store.getKind() == kind::STORE &&
-            store[1] == node[1]) {
-          return RewriteResponse(REWRITE_DONE, store[2]);
+        if (store.getKind() == kind::STORE) {
+          // select(store(a,i,v),j)
+          Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+          if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+            bool value = eqRewritten.getConst<bool>();
+            if (value) {
+              // select(store(a,i,v),i) = v
+              return RewriteResponse(REWRITE_DONE, store[2]);
+            }
+            else {
+              // select(store(a,i,v),j) = select(a,j) if i /= j
+              Node newNode = NodeManager::currentNM()->mkNode(kind::SELECT, store[0], node[1]);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+          }
         }
         break;
       }
@@ -53,11 +64,25 @@ public:
             value[1] == node[1]) {
           return RewriteResponse(REWRITE_DONE, store);
         }
-        // store(store(a,i,v),i,w) = store(a,i,w)
-        if (store.getKind() == kind::STORE &&
-            store[1] == node[1]) {
-          Node newNode = NodeManager::currentNM()->mkNode(kind::STORE, store[0], store[1], value);
-          return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+        if (store.getKind() == kind::STORE) {
+          // store(store(a,i,v),j,w)
+          Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+          if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+            bool val = eqRewritten.getConst<bool>();
+            NodeManager* nm = NodeManager::currentNM();
+            if (val) {
+              // store(store(a,i,v),i,w) = store(a,i,w)
+              Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+            else if (node[1] < store[1]) {
+              // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
+              //    IF i != j and j comes before i in the ordering
+              Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value);
+              newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+          }
         }
         break;
       }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index fd9e7cb2f..fabff0aab 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -65,6 +65,32 @@ struct ArrayStoreTypeRule {
   }
 };/* struct ArrayStoreTypeRule */
 
+struct ArrayTableFunTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::ARR_TABLE_FUN);
+    TypeNode arrayType = n[0].getType(check);
+    if( check ) {
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array");
+      }
+      TypeNode arrType2 = n[1].getType(check);
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
+      }
+      TypeNode indexType = n[2].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
+      }
+      indexType = n[3].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
+      }
+    }
+    return arrayType.getArrayIndexType();
+  }
+};/* struct ArrayStoreTypeRule */
+
 struct CardinalityComputer {
   inline static Cardinality computeCardinality(TypeNode type) {
     Assert(type.getKind() == kind::ARRAY_TYPE);