Merge from arrays2 branch.

9 files changed, 2039 insertions, 16 deletions

diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 578915d69..1e070cdaf 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -9,6 +9,10 @@ libarrays_la_SOURCES = \
 	theory_arrays_type_rules.h \
 	theory_arrays_rewriter.h \
 	theory_arrays.h \
-	theory_arrays.cpp
+	theory_arrays.cpp \
+	union_find.h \
+	union_find.cpp \
+	array_info.h \
+	array_info.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
new file mode 100644
index 000000000..c795de0b9
--- /dev/null
+++ b/src/theory/arrays/array_info.cpp
@@ -0,0 +1,272 @@
+/*********************                                                        */
+/*! \file array_info.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Contains additional classes to store context dependent information
+ ** for each term of type array
+ **
+ **
+ **/
+
+#include "array_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+bool inList(const CTNodeList* l, const TNode el) {
+  CTNodeList::const_iterator it = l->begin();
+  for ( ; it!= l->end(); it ++) {
+    if(*it == el)
+      return true;
+  }
+  return false;
+}
+
+void printList (CTNodeList* list) {
+  CTNodeList::const_iterator it = list->begin();
+  Debug("arrays-info")<<"   [ ";
+  for(; it != list->end(); it++ ) {
+    Debug("arrays-info")<<(*it)<<" ";
+  }
+  Debug("arrays-info")<<"] \n";
+}
+
+void printList (List<TNode>* list) {
+  List<TNode>::const_iterator it = list->begin();
+  Debug("arrays-info")<<"   [ ";
+  for(; it != list->end(); it++ ) {
+    Debug("arrays-info")<<(*it)<<" ";
+  }
+  Debug("arrays-info")<<"] \n";
+}
+
+void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
+  std::set<TNode> temp;
+  CTNodeList::const_iterator it;
+  for(it = la->begin() ; it != la->end(); it++ ) {
+    temp.insert((*it));
+  }
+
+  for(it = lb->begin() ; it!= lb->end(); it++ ) {
+    if(temp.count(*it) == 0) {
+      la->push_back(*it);
+    }
+  }
+}
+
+void ArrayInfo::addIndex(const Node a, const TNode i) {
+  Assert(a.getType().isArray());
+  Assert(!i.getType().isArray()); // temporary for flat arrays
+  Debug("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
+  List<TNode>* temp_indices;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_indices = new List<TNode>(bck);
+    temp_indices->append(i);
+
+    temp_info = new Info(ct, bck);
+    temp_info->indices = temp_indices;
+
+    info_map[a] = temp_info;
+  } else {
+    temp_indices = (*it).second->indices;
+    temp_indices->append(i);
+  }
+  if(Debug.isOn("arrays-ind")) {
+    printList((*(info_map.find(a))).second->indices);
+  }
+
+}
+
+void ArrayInfo::addStore(const Node a, const TNode st){
+  Assert(a.getType().isArray());
+  Assert(st.getKind()== kind::STORE); // temporary for flat arrays
+
+  CTNodeList* temp_store;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_store = new(true) CTNodeList(ct);
+    temp_store->push_back(st);
+
+    temp_info = new Info(ct, bck);
+    temp_info->stores = temp_store;
+    info_map[a]=temp_info;
+  } else {
+    temp_store = (*it).second->stores;
+    if(! inList(temp_store, st)) {
+      temp_store->push_back(st);
+    }
+  }
+};
+
+
+void ArrayInfo::addInStore(const TNode a, const TNode b){
+  Debug("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
+  Assert(a.getType().isArray());
+  Assert(b.getType().isArray());
+
+  CTNodeList* temp_inst;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_inst = new(true) CTNodeList(ct);
+    temp_inst->push_back(b);
+
+    temp_info = new Info(ct, bck);
+    temp_info->in_stores = temp_inst;
+    info_map[a] = temp_info;
+  } else {
+    temp_inst = (*it).second->in_stores;
+    if(! inList(temp_inst, b)) {
+      temp_inst->push_back(b);
+    }
+  }
+};
+
+
+
+/**
+ * Returns the information associated with TNode a
+ */
+
+const Info* ArrayInfo::getInfo(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end())
+      return (*it).second;
+  return emptyInfo;
+}
+
+List<TNode>* ArrayInfo::getIndices(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->indices;
+  }
+  return emptyListI;
+}
+
+const CTNodeList* ArrayInfo::getStores(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->stores;
+  }
+  return emptyList;
+}
+
+const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->in_stores;
+  }
+  return emptyList;
+}
+
+
+void ArrayInfo::mergeInfo(const TNode a, const TNode b){
+  // can't have assertion that find(b) = a !
+  TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
+  ++d_callsMergeInfo;
+
+  Debug("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
+  Debug("arrays-mergei")<<"                      and "<<b<<"\n";
+
+  CNodeInfoMap::iterator ita = info_map.find(a);
+  CNodeInfoMap::iterator itb = info_map.find(b);
+
+  if(ita != info_map.end()) {
+    Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
+    if(Debug.isOn("arrays-mergei"))
+      (*ita).second->print();
+
+    if(itb != info_map.end()) {
+      Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
+      if(Debug.isOn("arrays-mergei"))
+        (*itb).second->print();
+
+      List<TNode>* lista_i = (*ita).second->indices;
+      CTNodeList* lista_st = (*ita).second->stores;
+      CTNodeList* lista_inst = (*ita).second->in_stores;
+
+
+      List<TNode>* listb_i = (*itb).second->indices;
+      CTNodeList* listb_st = (*itb).second->stores;
+      CTNodeList* listb_inst = (*itb).second->in_stores;
+
+      lista_i->concat(listb_i);
+      mergeLists(lista_st, listb_st);
+      mergeLists(lista_inst, listb_inst);
+
+      /* sketchy stats */
+
+      //FIXME
+      int s = 0;//lista_i->size();
+      d_maxList.maxAssign(s);
+
+
+      if(s!= 0) {
+        d_avgIndexListLength.addEntry(s);
+        ++d_listsCount;
+      }
+      s = lista_st->size();
+      d_maxList.maxAssign(s);
+      if(s!= 0) {
+        d_avgStoresListLength.addEntry(s);
+        ++d_listsCount;
+      }
+
+      s = lista_inst->size();
+      d_maxList.maxAssign(s);
+      if(s!=0) {
+        d_avgInStoresListLength.addEntry(s);
+        ++d_listsCount;
+      }
+
+      /* end sketchy stats */
+
+    }
+
+  } else {
+    Debug("arrays-mergei")<<" First element has no info \n";
+    if(itb != info_map.end()) {
+      Debug("arrays-mergei")<<" adding second element's info \n";
+      (*itb).second->print();
+
+      List<TNode>* listb_i = (*itb).second->indices;
+      CTNodeList* listb_st = (*itb).second->stores;
+      CTNodeList* listb_inst = (*itb).second->in_stores;
+
+      Info* temp_info = new Info(ct, bck);
+
+      (temp_info->indices)->concat(listb_i);
+      mergeLists(temp_info->stores, listb_st);
+      mergeLists(temp_info->in_stores, listb_inst);
+      info_map[a] = temp_info;
+
+    } else {
+    Debug("arrays-mergei")<<" Second element has no info \n";
+    }
+
+   }
+  Debug("arrays-mergei")<<"Arrays::mergeInfo done \n";
+
+}
+
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
new file mode 100644
index 000000000..6eb20e30a
--- /dev/null
+++ b/src/theory/arrays/array_info.h
@@ -0,0 +1,239 @@
+/*! \file array_info.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Contains additional classes to store context dependent information
+ ** for each term of type array
+ **
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#include "util/backtrackable.h"
+#include "context/cdlist.h"
+#include "context/cdmap.h"
+#include "expr/node.h"
+#include "util/stats.h"
+#include "util/ntuple.h"
+#include <ext/hash_set>
+#include <ext/hash_map>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+typedef context::CDList<TNode> CTNodeList;
+
+struct TNodeQuadHashFunction {
+  size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const {
+    TNode n1 = q.first;
+    TNode n2 = q.second;
+    TNode n3 = q.third;
+    TNode n4 = q.fourth;
+    return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 +
+        n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
+
+  }
+};/* struct TNodeQuadHashFunction */
+
+void printList (CTNodeList* list);
+void printList( List<TNode>* list);
+
+bool inList(const CTNodeList* l, const TNode el);
+
+/**
+ * Small class encapsulating the information
+ * in the map. It's a class and not a struct to
+ * call the destructor.
+ */
+
+class Info {
+public:
+  List<TNode>* indices;
+  CTNodeList* stores;
+  CTNodeList* in_stores;
+
+  Info(context::Context* c, Backtracker<TNode>* bck) {
+    indices = new List<TNode>(bck);
+    stores = new(true)CTNodeList(c);
+    in_stores = new(true)CTNodeList(c);
+
+  }
+
+  ~Info() {
+    //FIXME!
+    //indices->deleteSelf();
+    stores->deleteSelf();
+    in_stores->deleteSelf();
+  }
+
+  /**
+   * prints the information
+   */
+  void print() const {
+    Assert(indices != NULL && stores!= NULL); // && equals != NULL);
+    Debug("arrays-info")<<"  indices   ";
+    printList(indices);
+    Debug("arrays-info")<<"  stores ";
+    printList(stores);
+    Debug("arrays-info")<<"  in_stores ";
+    printList(in_stores);
+  }
+};
+
+
+typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
+
+/**
+ * Class keeping track of the following information for canonical
+ * representatives of type array [a] :
+ *    indices at which it is being read (all i for which there is a
+ *            term of the form SELECT a i)
+ *    all store terms in the congruence class
+ *    stores in which it appears (terms of the form STORE a _ _ )
+ *
+ */
+class ArrayInfo {
+private:
+  context::Context* ct;
+  Backtracker<TNode>* bck;
+  CNodeInfoMap info_map;
+
+  CTNodeList* emptyList;
+  List<TNode>* emptyListI;
+
+
+  /* == STATISTICS == */
+
+  /** time spent in preregisterTerm() */
+  TimerStat d_mergeInfoTimer;
+  AverageStat d_avgIndexListLength;
+  AverageStat d_avgStoresListLength;
+  AverageStat d_avgInStoresListLength;
+  IntStat d_listsCount;
+  IntStat d_callsMergeInfo;
+  IntStat d_maxList;
+  SizeStat<CNodeInfoMap > d_tableSize;
+
+  /**
+   * checks if a certain element is in the list l
+   * FIXME: better way to check for duplicates?
+   */
+
+  /**
+   * helper method that merges two lists into the first
+   * without adding duplicates
+   */
+  void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
+
+public:
+  const Info* emptyInfo;
+/*
+  ArrayInfo(): ct(NULl), info
+    d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
+    d_avgIndexListLength("theory::arrays::avgIndexListLength"),
+    d_avgStoresListLength("theory::arrays::avgStoresListLength"),
+    d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
+    d_listsCount("theory::arrays::listsCount",0),
+    d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
+    d_maxList("theory::arrays::maxList",0),
+    d_tableSize("theory::arrays::infoTableSize", info_map) {
+  StatisticsRegistry::registerStat(&d_mergeInfoTimer);
+  StatisticsRegistry::registerStat(&d_avgIndexListLength);
+  StatisticsRegistry::registerStat(&d_avgStoresListLength);
+  StatisticsRegistry::registerStat(&d_avgInStoresListLength);
+  StatisticsRegistry::registerStat(&d_listsCount);
+  StatisticsRegistry::registerStat(&d_callsMergeInfo);
+  StatisticsRegistry::registerStat(&d_maxList);
+  StatisticsRegistry::registerStat(&d_tableSize);
+  }*/
+  ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(),
+      d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
+      d_avgIndexListLength("theory::arrays::avgIndexListLength"),
+      d_avgStoresListLength("theory::arrays::avgStoresListLength"),
+      d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
+      d_listsCount("theory::arrays::listsCount",0),
+      d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
+      d_maxList("theory::arrays::maxList",0),
+      d_tableSize("theory::arrays::infoTableSize", info_map) {
+    emptyList = new(true) CTNodeList(ct);
+    emptyListI = new List<TNode>(bck);
+    emptyInfo = new Info(ct, bck);
+    StatisticsRegistry::registerStat(&d_mergeInfoTimer);
+    StatisticsRegistry::registerStat(&d_avgIndexListLength);
+    StatisticsRegistry::registerStat(&d_avgStoresListLength);
+    StatisticsRegistry::registerStat(&d_avgInStoresListLength);
+    StatisticsRegistry::registerStat(&d_listsCount);
+    StatisticsRegistry::registerStat(&d_callsMergeInfo);
+    StatisticsRegistry::registerStat(&d_maxList);
+    StatisticsRegistry::registerStat(&d_tableSize);
+  }
+
+  ~ArrayInfo(){
+    CNodeInfoMap::iterator it = info_map.begin();
+    for( ; it != info_map.end(); it++ ) {
+      if((*it).second!= emptyInfo) {
+        delete (*it).second;
+      }
+    }
+    emptyList->deleteSelf();
+    delete emptyInfo;
+    StatisticsRegistry::unregisterStat(&d_mergeInfoTimer);
+    StatisticsRegistry::unregisterStat(&d_avgIndexListLength);
+    StatisticsRegistry::unregisterStat(&d_avgStoresListLength);
+    StatisticsRegistry::unregisterStat(&d_avgInStoresListLength);
+    StatisticsRegistry::unregisterStat(&d_listsCount);
+    StatisticsRegistry::unregisterStat(&d_callsMergeInfo);
+    StatisticsRegistry::unregisterStat(&d_maxList);
+    StatisticsRegistry::unregisterStat(&d_tableSize);
+  };
+
+  /**
+   * adds the node a to the map if it does not exist
+   * and it initializes the info. checks for duplicate i's
+   */
+  void addIndex(const Node a, const TNode i);
+  void addStore(const Node a, const TNode st);
+  void addInStore(const TNode a, const TNode st);
+
+
+  /**
+   * Returns the information associated with TNode a
+   */
+
+  const Info* getInfo(const TNode a) const;
+
+  List<TNode>* getIndices(const TNode a) const;
+
+  const CTNodeList* getStores(const TNode a) const;
+
+  const CTNodeList* getInStores(const TNode a) const;
+
+  /**
+   * merges the information of  nodes a and b
+   * the nodes do not have to actually be in the map.
+   * pre-condition
+   *  a should be the canonical representative of b
+   */
+  void mergeInfo(const TNode a, const TNode b);
+};
+
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 4c68fb5cb..30242db30 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"
 
 properties polite stable-infinite
-properties check
+properties check propagate presolve
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8b625613a..37c49b341 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -20,7 +20,7 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/valuation.h"
 #include "expr/kind.h"
-
+#include <map>
 
 using namespace std;
 using namespace CVC4;
@@ -31,33 +31,140 @@ using namespace CVC4::theory::arrays;
 
 
 TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) :
-  Theory(THEORY_ARRAY, c, out, valuation)
+  Theory(THEORY_ARRAY, c, 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_checkTimer("theory::arrays::checkTime"),
+  d_donePreregister(false)
 {
+  //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_checkTimer);
+
+
 }
 
 
 TheoryArrays::~TheoryArrays() {
+
+  StatisticsRegistry::unregisterStat(&d_numRow);
+  StatisticsRegistry::unregisterStat(&d_numExt);
+  StatisticsRegistry::unregisterStat(&d_numProp);
+  StatisticsRegistry::unregisterStat(&d_numExplain);
+  StatisticsRegistry::unregisterStat(&d_checkTimer);
+
 }
 
 
 void TheoryArrays::addSharedTerm(TNode t) {
-  Debug("arrays") << "TheoryArrays::addSharedTerm(): "
+  Debug("arrays") << "Arrays::addSharedTerm(): "
                   << t << endl;
 }
 
 
 void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
-  Debug("arrays") << "TheoryArrays::notifyEq(): "
-                  << lhs << " = " << rhs << endl;
+}
+
+void TheoryArrays::notifyCongruent(TNode a, TNode b) {
+  Debug("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;
+  }
+
+  Debug("arrays") <<"Arrays::start check ";
   while(!done()) {
     Node assertion = get();
-    Debug("arrays") << "TheoryArrays::check(): " << assertion << endl;
+    Debug("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, false);
+        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, false);
+        return;
+      }
+      else if(find(a) == find(b)) {
+        Node conflict = constructConflict(assertion[0]);
+        d_out->conflict(conflict, false);
+        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();
+    Debug("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
+    //}
   }
-  Debug("arrays") << "TheoryArrays::check(): done" << endl;
+  Debug("arrays") << "Arrays::check(): done" << endl;
 }
 
 Node TheoryArrays::getValue(TNode n) {
@@ -76,3 +183,717 @@ Node TheoryArrays::getValue(TNode n) {
     Unhandled(n.getKind());
   }
 }
+
+void TheoryArrays::merge(TNode a, TNode b) {
+  Assert(d_conflict.isNull());
+
+  Debug("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
+
+  /*
+   * 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);
+
+  if( a == b) {
+    return;
+  }
+
+
+  // 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);
+  }
+
+
+}
+
+
+void TheoryArrays::checkPropagations(TNode a, TNode b) {
+  EqLists::const_iterator ita = d_equalities.find(a);
+  EqLists::const_iterator itb = d_equalities.find(b);
+
+  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;
+
+      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);
+    }
+    else {
+      List<TNode>* eqsb = new List<TNode>(&d_backtracker);
+      List<TNode>* eqsa = (*ita).second;
+      d_equalities.insert(b, eqsb);
+      eqsb->concat(eqsa);
+    }
+  } 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);
+  }
+}
+
+
+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) {
+  Debug("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) {
+        Debug("arrays-axiom")<<"Arrays::isAxiom true\n";
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+
+Node TheoryArrays::constructConflict(TNode diseq) {
+  Debug("arrays") << "arrays: begin constructConflict()" << endl;
+  Debug("arrays") << "arrays:   using diseq == " << diseq << endl;
+
+  // returns the reason the two terms are equal
+  Node explanation = d_cc.explain(diseq[0], diseq[1]);
+
+  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;
+    }
+  }
+  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;
+      }
+    }
+  }
+
+  nb<<diseq.notNode();
+  Node conflict = nb;
+  Debug("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);
+  }
+  else {
+   CTNodeList* list = new (true)CTNodeList(getContext());
+   list->push_back(b);
+   d_atoms[a] = list;
+  }
+
+}
+*/
+
+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::addDiseq(TNode diseq) {
+  Assert(diseq.getKind() == kind::EQUAL ||
+         diseq.getKind() == kind::IFF);
+  TNode a = diseq[0];
+  TNode b = diseq[1];
+
+  appendToDiseqList(find(a), diseq);
+  appendToDiseqList(find(b), diseq);
+
+}
+
+void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
+  Debug("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;
+  }
+
+  deq->push_back(eq);
+}
+
+
+/**
+ * Iterates through the indices of a and stores of b and checks if any new
+ * Row lemmas need to be instantiated.
+ */
+
+bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) {
+  Assert(a.getType().isArray());
+  Assert(b.getType().isArray());
+
+  if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 ||
+     d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) {
+    return true;
+  }
+
+  return false;
+}
+
+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(find(i) == find(j) || find(aj) == find(bj)) {
+    //Debug("arrays-lem")<<"isRedundantInContext valid "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+    checkRowForIndex(j,b); // why am i doing this?
+    checkRowForIndex(i,a);
+    return true;
+    }
+  if(alreadyAddedRow(a,b,i,j)) {
+   // Debug("arrays-lem")<<"isRedundantInContext already added "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+    return true;
+  }
+  return false;
+}
+
+TNode TheoryArrays::areDisequal(TNode a, TNode b) {
+  Debug("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++) {
+      Debug("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;
+      }
+
+    }
+  }
+  Debug("arrays-prop")<<"    not disequal \n";
+  return TNode::null();
+}
+
+bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
+  Debug("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node aj = nm->mkNode(kind::SELECT, a, j);
+  Node bj = nm->mkNode(kind::SELECT, b, j);
+
+  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
+      Debug("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;
+      }
+
+    }
+  }
+
+  // now check if the current context implies NOT a[j] = b[j]
+  // in which case we propagate i = j
+
+  // 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());
+
+    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;
+      }
+    }
+  }
+
+  Debug("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
+  return false;
+}
+
+void TheoryArrays::explain(TNode n) {
+
+
+  Debug("arrays")<<"Arrays::explain start for "<<n<<"\n";
+  ++d_numExplain;
+
+  Assert(n.getKind()==kind::EQUAL);
+
+  Node explanation = d_cc.explain(n[0], n[1]);
+
+  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;
+    }
+  }
+  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;
+      }
+    }
+  }
+  Node reason = nb;
+
+  d_out->explanation(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];
+
+  Assert ((find(a) == find(s) && find(b) == find(t)) ||
+          (find(a) == find(t) && find(b) == find(s)));
+
+
+  if(find(a) == find(t)) {
+    TNode temp = t;
+    t = s;
+    s = temp;
+  }
+
+  // construct the explanation
+
+  NodeBuilder<> nb(kind::AND);
+  Node explanation1 = d_cc.explain(a, s);
+  Node explanation2 = d_cc.explain(b, t);
+
+  if(explanation1.getKind() == kind::AND) {
+    for(TNode::iterator i= TNode(explanation1).begin();
+        i!=TNode(explanation1).end(); ++i) {
+      nb << *i;
+    }
+  } else {
+    Assert(explanation1.getKind() == kind::EQUAL ||
+           explanation1.getKind() == kind::IFF);
+    nb << explanation1;
+  }
+
+  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;
+  }
+
+  nb << diseq;
+  Node reason = nb;
+  d_out->explanation(reason);
+  Debug("arrays")<<"explanation "<< reason<<" done \n";
+  */
+}
+
+void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
+
+  Debug("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
+  if(Debug.isOn("arrays-crl"))
+    d_infoMap.getInfo(a)->print();
+  Debug("arrays-crl")<<"  ------------  and "<<b<<"\n";
+  if(Debug.isOn("arrays-crl"))
+    d_infoMap.getInfo(b)->print();
+
+  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 != 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];
+
+      if(  !isRedundandRowLemma(store, c, j, i)){
+         //&&!propagateFromRow(store, c, j, i)) {
+        queueRowLemma(store, c, j, i);
+      }
+    }
+
+  }
+
+  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)
+          &&!isRedundandRowLemma(store, c, j, i)){
+          //&&!propagateFromRow(store, c, j, i)) {
+        queueRowLemma(store, c, j, i);
+      }
+
+    }
+  }
+
+  Debug("arrays-crl")<<"Arrays::checkLemmas done.\n";
+}
+
+/**
+ * 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);
+
+
+
+ Debug("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
+ d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
+ d_out->lemma(lem);
+ ++d_numRow;
+
+}
+
+
+/**
+ * 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) {
+  Debug("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
+  Debug("arrays-cri")<<"                   index "<<i<<"\n";
+
+  if(Debug.isOn("arrays-cri")) {
+    d_infoMap.getInfo(a)->print();
+  }
+  Assert(a.getType().isArray());
+
+  const CTNodeList* stores = d_infoMap.getStores(a);
+  const CTNodeList* instores = d_infoMap.getInStores(a);
+  CTNodeList::const_iterator it = stores->begin();
+
+  for(; it!= stores->end(); it++) {
+    TNode store = *it;
+    Assert(store.getKind()==kind::STORE);
+    TNode j = store[1];
+    //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+    if(!isRedundandRowLemma(store, store[0], j, i)) {
+      //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(store, store[0], j, i);
+    }
+  }
+
+  it = instores->begin();
+  for(; it!= instores->end(); it++) {
+    TNode instore = *it;
+    Assert(instore.getKind()==kind::STORE);
+    TNode j = instore[1];
+    //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+    if(!isRedundandRowLemma(instore, instore[0], j, i)) {
+      //Debug("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(instore, instore[0], j, i);
+    }
+  }
+
+}
+
+
+void TheoryArrays::checkStore(TNode a) {
+  Debug("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
+
+  if(Debug.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];
+
+  List<TNode>* js = d_infoMap.getIndices(b);
+  List<TNode>::const_iterator it = js->begin();
+
+  for(; it!= js->end(); it++) {
+    TNode j = *it;
+
+    if(!isRedundandRowLemma(a, b, i, j)) {
+      //Debug("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+      queueRowLemma(a,b,i,j);
+    }
+  }
+
+}
+
+inline void TheoryArrays::queueExtLemma(TNode a, TNode b) {
+  Assert(a.getType().isArray() && b.getType().isArray());
+
+  d_extQueue.insert(make_pair(a,b));
+}
+
+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));
+}
+
+/**
+* Adds a new Ext lemma of the form
+*    a = b OR a[k]!=b[k], for a new variable k
+*/
+
+inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
+ Assert(a.getType().isArray());
+ Assert(b.getType().isArray());
+
+ Debug("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
+ Debug("arrays-cle")<<"                   and "<<b<<" \n";
+
+
+ if(   d_extAlreadyAdded.count(make_pair(a, b)) == 0
+    && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
+
+   NodeManager* nm = NodeManager::currentNM();
+   Node k = nm->mkVar(a.getType()[0]);
+   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);
+
+   Debug("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
+   d_extAlreadyAdded.insert(make_pair(a,b));
+   d_out->lemma(lem);
+   ++d_numExt;
+   return;
+ }
+ Debug("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+
+}
+
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index fbbda9e44..bc1f670ba 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Theory of arrays.
+ ** \brief Theory of arrays
  **
  ** Theory of arrays.
  **/
@@ -22,32 +22,465 @@
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
 #include "theory/theory.h"
+#include "theory/arrays/union_find.h"
+#include "util/congruence_closure.h"
+#include "array_info.h"
+#include "util/hash.h"
+#include "util/ntuple.h"
+#include "util/stats.h"
+#include "util/backtrackable.h"
 
 #include <iostream>
+#include <map>
 
 namespace CVC4 {
 namespace theory {
 namespace arrays {
 
+/**
+ * Decision procedure for arrays.
+ *
+ * Overview of decision procedure:
+ *
+ * Preliminary notation:
+ *   Stores(a)  = {t | a ~ t and t = store( _ _ _ )} 
+ *   InStores(a) = {t | t = store (b _ _) and a ~ b }
+ *   Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)}
+ *   ~ represents the equivalence relation based on the asserted equalities in the
+ *   current context.
+ * 
+ * The rules implemented are the following:
+ *             store(b i v)
+ *     Row1 -------------------
+ *          store(b i v)[i] = v
+ * 
+ *           store(b i v)  a'[j]
+ *     Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
+ *           i = j OR a[j] = b[j]
+ * 
+ *          a  b same kind arrays
+ *     Ext ------------------------ [ a!= b in current context, k new var]
+ *           a = b OR a[k] != b[k]p
+ * 
+ * 
+ *  The Row1 one rule is implemented implicitly as follows:
+ *     - for each store(b i v) term add the following equality to the congruence
+ *       closure store(b i v)[i] = v
+ *     - if one of the literals in a conflict is of the form store(b i v)[i] = v
+ *       remove it from the conflict
+ * 
+ *  Because new store terms are not created, we need to check if we need to
+ *  instantiate a new Row axiom in the following cases:
+ *     1. the congruence relation changes (i.e. two terms get merged)
+ *         - when a new equality between array terms a = b is asserted we check if
+ *           we can instantiate a Row lemma for all pairs of indices i where a is
+ *           being read and stores
+ *         - this is only done during full effort check
+ *     2. a new read term is created either as a consequences of an Ext lemma or a
+ *        Row lemma
+ *         - this is implemented in the checkRowForIndex method which is called
+ *           when preregistering a term of the form a[i].
+ *         - as a consequence lemmas are instantiated even before full effort check
+ * 
+ *  The Ext axiom is instantiated when a disequality is asserted during full effort
+ *  check. Ext lemmas are stored in a cache to prevent instantiating essentially
+ *  the same lemma multiple times.
+ */
 class TheoryArrays : public Theory {
+
+private:
+
+
+  class CongruenceChannel {
+    TheoryArrays* d_arrays;
+
+  public:
+    CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {}
+    void notifyCongruent(TNode a, TNode b) {
+      d_arrays->notifyCongruent(a, b);
+    }
+  }; /* class CongruenceChannel*/
+  friend class CongruenceChannel;
+
+  /**
+   * Output channel connected to the congruence closure module.
+   */
+  CongruenceChannel d_ccChannel;
+
+  /**
+   * Instance of the congruence closure module.
+   */
+  CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1
+                                 (kind::SELECT)> d_cc;
+
+  /**
+   * Union find for storing the equalities.
+   */
+
+  UnionFind<Node, NodeHashFunction> d_unionFind;
+
+  Backtracker<TNode> d_backtracker;
+
+
+  /**
+   * 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
+   */
+
+  ArrayInfo d_infoMap;
+
+  /**
+   * Received a notification from the congruence closure algorithm that the two
+   * nodes a and b have become congruent.
+   */
+
+  void notifyCongruent(TNode a, TNode b);
+
+
+  typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
+  typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
+  typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+
+
+  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;
+
+  void checkPropagations(TNode a, TNode b);
+
+  /** List of all atoms the SAT solver knows about and are candidates for
+   *  propagation. */
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
+
+  /** List of disequalities needed to construct explanations for propagated
+   * row lemmas */
+
+  context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
+
+  /**
+   * stores the conflicting disequality (still need to call construct
+   * conflict to get the actual explanation)
+   */
+  Node d_conflict;
+
+  typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList;
+
+
+  /**
+   * Ext lemma workslist that stores extensionality lemmas that still need to be added
+   */
+  std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue;
+
+  /**
+   * 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;
+
+  /**
+   * 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;
+
+  /**
+   * 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;
+
+  /*
+   * Congruence helper methods
+   */
+
+  void addDiseq(TNode diseq);
+  void addEq(TNode eq);
+
+  void appendToDiseqList(TNode of, TNode eq);
+  void appendToEqList(TNode a, TNode b);
+  Node constructConflict(TNode diseq);
+
+  /**
+   * Merges two congruence classes in the internal union-find and checks for a
+   * conflict.
+   */
+
+  void merge(TNode a, TNode b);
+  inline TNode find(TNode a);
+  inline TNode debugFind(TNode a) const;
+
+  inline void setCanon(TNode a, TNode b);
+
+  void queueRowLemma(TNode a, TNode b, TNode i, TNode j);
+  inline void queueExtLemma(TNode a, TNode b);
+
+  /**
+   * Adds a Row lemma of the form:
+   *    i = j OR a[j] = b[j]
+   */
+  void addRowLemma(TNode a, TNode b, TNode i, TNode j);
+
+  /**
+   * 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);
+
+  /**
+   * 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);
+
+
+  bool isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j);
+  bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
+
+
+
+  bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
+    //Debug("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);
+
+    for( ; it!= d_RowAlreadyAdded.end(); it++) {
+
+      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_) {
+        //Debug("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
+        return true;
+      }
+    }
+    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);
+      }
+    }
+
+    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);
+    }
+  }
+
+  /** 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);
+
+  TNode areDisequal(TNode a, TNode b);
+
+
+
+  /*
+   * === STATISTICS ===
+   */
+
+  /** 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;
+
+
 public:
   TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation);
   ~TheoryArrays();
-  void preRegisterTerm(TNode n) { }
-  //void registerTerm(TNode n) { }
 
-  //void presolve() { }
+  /**
+   * 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 preRegisterTerm(TNode n) {
+    //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
+    Debug("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
+      Debug("arrays-preregister")<<"atom "<<n<<"\n";
+      d_atoms.insert(n);
+      // add to proper equality lists
+      addEq(n);
+      break;
+    case kind::SELECT:
+      //Debug("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
+      d_infoMap.addIndex(n[0], n[1]);
+      checkRowForIndex(n[1], find(n[0]));
+      //Debug("arrays-preregister")<<"n[0] \n";
+      //d_infoMap.getInfo(n[0])->print();
+      //Debug("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:
+      Debug("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
+    }
+  }
+
+  //void registerTerm(TNode n) {
+  //  Debug("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
+  //}
+
+  void presolve() {
+    Debug("arrays")<<"Presolving \n";
+    d_donePreregister = true;
+  }
 
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void check(Effort e);
-  //void propagate(Effort e) { }
-  void explain(TNode n) { }
+
+  void propagate(Effort e) {
+
+    Debug("arrays-prop")<<"Propagating \n";
+
+    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);
+      Debug("arrays-prop")<<"value of "<<eq<<" ";
+      Debug("arrays-prop")<<d_valuation.getSatValue(eq);
+      if(find(eq[0]) == find(eq[1])) {
+        Debug("arrays-prop")<<" eq \n";
+        ++d_numProp;
+      }
+    }
+    */
+
+  }
+  void explain(TNode n);
+
   Node getValue(TNode n);
   void shutdown() { }
   std::string identify() const { return std::string("TheoryArrays"); }
+
 };/* 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 33a6233bc..c37cbe68c 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -32,11 +32,60 @@ class TheoryArraysRewriter {
 
 public:
 
-  static inline RewriteResponse postRewrite(TNode node) {
+  static RewriteResponse postRewrite(TNode node) {
+    Debug("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
+    if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+      if(node[0] == node[1]) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      }
+      // checks for RoW axiom: (select ( store a i v) i) = v and rewrites it
+      // to true
+      if(node[0].getKind()==kind::SELECT) {
+        TNode a = node[0][0];
+        TNode j = node[0][1];
+        if(a.getKind()==kind::STORE) {
+          TNode b = a[0];
+          TNode i = a[1];
+          TNode v = a[2];
+          if(v == node[1] && i == j) {
+            Debug("arrays-postrewrite") << "Arrays::postRewrite true" << std::endl;
+            return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+          }
+        }
+      }
+
+      if (node[0] > node[1]) {
+        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+        // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
+        if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
+          return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+        } else {
+          return RewriteResponse(REWRITE_DONE, newNode);
+        }
+      }
+    }
+    // FIXME: would it be better to move in preRewrite?
+    // if yes don't need the above case
+    if (node.getKind()==kind::SELECT) {
+      // we are rewriting (select (store a i v) i) to v
+      TNode a = node[0];
+      TNode i = node[1];
+      if(a.getKind() == kind::STORE) {
+        TNode b = a[0];
+        TNode j = a[1];
+        TNode v = a[2];
+        if(i==j) {
+          Debug("arrays-postrewrite") << "Arrays::postrewrite to " << v << std::endl;
+          return RewriteResponse(REWRITE_AGAIN_FULL, v);
+        }
+      }
+    }
+
     return RewriteResponse(REWRITE_DONE, node);
   }
 
   static inline RewriteResponse preRewrite(TNode node) {
+    Debug("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl;
     return RewriteResponse(REWRITE_DONE, node);
   }
 
diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp
new file mode 100644
index 000000000..b0f06b78e
--- /dev/null
+++ b/src/theory/arrays/union_find.cpp
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file union_find.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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 "theory/arrays/union_find.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+template <class NodeType, class NodeHash>
+void UnionFind<NodeType, NodeHash>::notify() {
+  Trace("arraysuf") << "arraysUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
+  while(d_offset < d_trace.size()) {
+    pair<TNode, TNode> p = d_trace.back();
+    if(p.second.isNull()) {
+      d_map.erase(p.first);
+      Trace("arraysuf") << "arraysUF   " << d_trace.size() << " erasing " << p.first << endl;
+    } else {
+      d_map[p.first] = p.second;
+      Trace("arraysuf") << "arraysUF   " << d_trace.size() << " replacing " << p << endl;
+    }
+    d_trace.pop_back();
+  }
+  Trace("arraysuf") << "arraysUF cancelling finished." << endl;
+}
+
+// The following declarations allow us to put functions in the .cpp file
+// instead of the header, since we know which instantiations are needed.
+
+template void UnionFind<Node, NodeHashFunction>::notify();
+
+template void UnionFind<TNode, TNodeHashFunction>::notify();
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
new file mode 100644
index 000000000..4a882806c
--- /dev/null
+++ b/src/theory/arrays/union_find.h
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file union_find.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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__UNION_FIND_H
+#define __CVC4__THEORY__ARRAYS__UNION_FIND_H
+
+#include <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+
+namespace context {
+  class Context;
+}/* CVC4::context namespace */
+
+namespace theory {
+namespace arrays {
+
+// NodeType \in { Node, TNode }
+template <class NodeType, class NodeHash>
+class UnionFind : context::ContextNotifyObj {
+  /** Our underlying map type. */
+  typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> 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;
+
+  /** Our undo stack for changes made to d_map. */
+  std::vector<std::pair<TNode, TNode> > d_trace;
+
+  /** Our current offset in the d_trace stack (context-dependent). */
+  context::CDO<size_t> d_offset;
+
+public:
+  UnionFind(context::Context* ctxt) :
+    context::ContextNotifyObj(ctxt),
+    d_offset(ctxt, 0) {
+  }
+
+  ~UnionFind() throw() { }
+
+  /**
+   * 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);
+
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::notify().
+   */
+  void notify();
+
+};/* class UnionFind<> */
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
+  typename MapType::const_iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    return n;
+  } else {
+    return debugFind((*i).second);
+  }
+}
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
+  Trace("arraysuf") << "arraysUF find of " << n << std::endl;
+  typename 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;
+    }
+    d_trace.push_back(std::make_pair(n, pr.second));
+    d_offset = d_trace.size();
+    Trace("arraysuf") << "arraysUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
+    pr.second = p;
+    d_map.insert(pr);
+    return p;
+  }
+}
+
+template <class NodeType, class NodeHash>
+inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
+  Assert(d_map.find(n) == d_map.end());
+  Assert(d_map.find(newParent) == d_map.end());
+  if(n != newParent) {
+    Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
+    d_map[n] = newParent;
+    d_trace.push_back(std::make_pair(n, TNode::null()));
+    d_offset = d_trace.size();
+  }
+}
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__ARRAYS__UNION_FIND_H */