13 files changed, 770 insertions, 410 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 0ac5096d2..9b429765e 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file equality_engine.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang, Tim King, Francois Bobot, Morgan Deters, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Guy Katz, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
 }
 
-
 /**
  * Data used in the BFS search through the equality graph.
  */
@@ -94,6 +93,8 @@ void EqualityEngine::init() {
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);
+
+  d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
 }
 
 EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -157,7 +158,7 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
-  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl;
   if (back) {
     d_propagationQueue.push_back(candidate);
   } else {
@@ -390,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
   return d_equalityNodes[nodeId];
 }
 
-void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
 
   Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl;
 
@@ -408,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me
   enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
 }
 
-void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead");
   assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid);
@@ -421,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
   propagate();
 }
 
-void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
   if (polarity) {
     // If two terms are already equal, don't assert anything
@@ -889,7 +890,7 @@ void EqualityEngine::backtrack() {
 
 }
 
-void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
+void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) {
   Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
   EqualityEdgeId edge = d_equalityEdges.size();
   d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
@@ -920,7 +921,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
 }
 
 void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
-  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
 
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));;
@@ -933,13 +934,72 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     // Get the explanation
     getExplanation(t1Id, t2Id, equalities, eqp);
   } else {
+    if (eqp) {
+      eqp->d_id = eq::MERGED_THROUGH_TRANS;
+      eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
+    }
+
     // Get the reason for this disequality
     EqualityPair pair(t1Id, t2Id);
     Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about");
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
+
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
+
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
-      getExplanation(toExplain.first, toExplain.second, equalities, eqp);
+      EqProof* eqpc = NULL;
+
+      // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
+      if (eqp && toExplain.first != toExplain.second) {
+        eqpc = new EqProof;
+      }
+
+      getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
+
+      if (eqpc) {
+        Debug("pf::ee") << "Child proof is:" << std::endl;
+        eqpc->debug_print("pf::ee", 1);
+
+        if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
+          std::vector<EqProof *> orderedChildren;
+          bool nullCongruenceFound = false;
+          for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
+
+              // For now, assume there can only be one null congruence child
+              Assert(!nullCongruenceFound);
+              nullCongruenceFound = true;
+
+              Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
+              orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
+              orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
+            } else {
+              orderedChildren.push_back(eqpc->d_children[i]);
+            }
+          }
+
+          if (nullCongruenceFound) {
+            eqpc->d_children = orderedChildren;
+            Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl;
+            eqpc->debug_print("pf::ee", 1);
+          }
+        }
+
+        eqp->d_children.push_back(eqpc);
+      }
+    }
+
+    if (eqp) {
+      if(eqp->d_children.size() == 1) {
+        // The transitivity proof has just one child. Simplify.
+        EqProof* temp = eqp->d_children[0];
+        eqp->d_children.clear();
+        *eqp = *temp;
+        delete temp;
+      }
+
+      Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
+      eqp->debug_print("pf::ee", 1);
     }
   }
 }
@@ -972,7 +1032,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
   // If the nodes are the same, we're done
   if (t1Id == t2Id){
     if( eqp ) {
-      eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)) {
+        std::vector<Node> no_children;
+        eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children);
+      } else {
+        eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      }
     }
     return;
   }
@@ -1019,24 +1084,28 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
           Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
 
-          std::vector< EqProof * > eqp_trans;
+          std::vector<EqProof *> eqp_trans;
 
           // Reconstruct the path
           do {
             // The current node
             currentNode = bfsQueue[currentIndex].nodeId;
             EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
-            MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+            unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
+            Node reason = d_equalityEdges[currentEdge].getReason();
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+            Debug("equality") << d_name << "                     targetNode = " << d_nodes[edgeNode] << std::endl;
             Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+            Debug("equality") << d_name << "                     reason type = " << reasonType << std::endl;
 
-            EqProof * eqpc = NULL;
-            //make child proof if a proof is being constructed
-            if( eqp ){
+            EqProof* eqpc = NULL;
+            // Make child proof if a proof is being constructed
+            if (eqp) {
               eqpc = new EqProof;
               eqpc->d_id = reasonType;
             }
+
             // Add the actual equality to the vector
             switch (reasonType) {
             case MERGED_THROUGH_CONGRUENCE: {
@@ -1044,32 +1113,47 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl;
               const FunctionApplication& f1 = d_applications[currentNode].original;
               const FunctionApplication& f2 = d_applications[edgeNode].original;
+
               Debug("equality") << push;
+              Debug("equality") << "Explaining left hand side equalities" << std::endl;
               EqProof * eqpc1 = eqpc ? new EqProof : NULL;
               getExplanation(f1.a, f2.a, equalities, eqpc1);
+              Debug("equality") << "Explaining right hand side equalities" << std::endl;
               EqProof * eqpc2 = eqpc ? new EqProof : NULL;
               getExplanation(f1.b, f2.b, equalities, eqpc2);
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
-                Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
                 if( d_nodes[currentNode].getKind()==kind::EQUAL ){
                   //leave node null for now
                   eqpc->d_node = Node::null();
-                }else{
-                  Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
+                } else {
                   if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
                      d_nodes[f1.a].getKind() == kind::SELECT ||
                      d_nodes[f1.a].getKind() == kind::STORE) {
                     eqpc->d_node = d_nodes[f1.a];
                   } else {
-                    eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]);
+                    if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
+                      // The first child is a PARTIAL_SELECT_0.
+                      // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
+                      Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
+                      Assert(eqpc->d_children[0]->d_children.size() == 0);
+
+                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
+                                                                                     d_nodes[f1.b]);
+                    } else {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
+                                                                      ProofManager::currentPM()->mkOp(d_nodes[f1.a]),
+                                                                      d_nodes[f1.b]);
+                    }
                   }
                 }
               }
               Debug("equality") << pop;
               break;
             }
+
             case MERGED_THROUGH_REFLEXIVITY: {
               // x1 == x1
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
@@ -1088,6 +1172,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               break;
             }
+
             case MERGED_THROUGH_CONSTANTS: {
               // f(c1, ..., cn) = c semantically, we can just ignore it
               Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
@@ -1111,23 +1196,41 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               }
 
               Debug("equality") << pop;
-
               break;
             }
+
             default: {
               // Construct the equality
-              Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
-              if( eqpc ){
-                if(reasonType == MERGED_THROUGH_EQUALITY) {
-                  eqpc->d_node = d_equalityEdges[currentEdge].getReason();
+              Debug("equality") << d_name << "::eq::getExplanation(): adding: "
+                                << reason << std::endl;
+              Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
+
+              Node a = d_nodes[currentNode];
+              Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+
+              if (eqpc) {
+                //apply proof reconstruction processing (when eqpc is non-null)
+                if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
+                  d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
+                                                                                equalities, eqpc);
+                }
+                if (reasonType == MERGED_THROUGH_EQUALITY) {
+                  eqpc->d_node = reason;
                 } else {
-                  // theory-specific proof rule
-                  eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]);
-                  Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl;
+                  // The LFSC translator prefers (not (= a b)) over (= (= a b) false)
+
+                  if (a == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = b.notNode();
+                  } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = a.notNode();
+                  } else {
+                    eqpc->d_node = b.eqNode(a);
+                  }
                 }
                 eqpc->d_id = reasonType;
               }
-              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+
+              equalities.push_back(reason);
               break;
             }
             }
@@ -1137,7 +1240,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             currentIndex = bfsQueue[currentIndex].previousIndex;
 
             //---from Morgan---
-            if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
+            if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
               if(eqpc->d_node.isNull()) {
                 Assert(eqpc->d_children.size() == 1);
                 EqProof *p = eqpc;
@@ -1149,11 +1252,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             }
             //---end from Morgan---
 
-            eqp_trans.push_back( eqpc );
-
+            eqp_trans.push_back(eqpc);
           } while (currentEdge != null_id);
 
-          if(eqp) {
+          if (eqp) {
             if(eqp_trans.size() == 1) {
               *eqp = *eqp_trans[0];
               delete eqp_trans[0];
@@ -1162,6 +1264,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
               eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
             }
+
+            eqp->debug_print("pf::ee", 1);
           }
 
           // Done
@@ -1508,7 +1612,7 @@ void EqualityEngine::debugPrintGraph() const {
     EqualityEdgeId edgeId = d_equalityGraph[nodeId];
     while (edgeId != null_edge) {
       const EqualityEdge& edge = d_equalityEdges[edgeId];
-      Debug("equality::graph") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+      Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
       edgeId = edge.getNext();
     }
 
@@ -1517,17 +1621,19 @@ void EqualityEngine::debugPrintGraph() const {
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
-  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
 
   Assert(hasTerm(t1));
   Assert(hasTerm(t2));
 
-  return getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl;
+  return result;
 }
 
 bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 {
-  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")";
 
   // Add the terms
   Assert(hasTerm(t1));
@@ -1539,6 +1645,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 
   // If we propagated this disequality we're true
   if (hasPropagatedDisequality(t1Id, t2Id)) {
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1556,6 +1663,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId));
       nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
     }
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1571,6 +1679,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
@@ -1587,21 +1696,33 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
 
   // Couldn't deduce dis-equalityReturn whether the terms are disequal
+  Debug("equality") << "\t(NO)" << std::endl;
   return false;
 }
 
-size_t EqualityEngine::getSize(TNode t)
-{
+size_t EqualityEngine::getSize(TNode t) {
   // Add the term
   addTermInternal(t);
   return getEqualityNode(getEqualityNode(t).getFind()).getSize();
 }
 
+
+void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) {
+  // Currently we can only inform one callback per trigger
+  Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end());
+  d_pathReconstructionTriggers[trigger] = notify;
+}
+
+unsigned EqualityEngine::getFreshMergeReasonType() {
+  return d_freshMergeReasonType++;
+}
+
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
   Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
@@ -2103,10 +2224,9 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
       d_children[i]->debug_print( c, tb+1 );
     }
   }
-  Debug( c ) << ")";
+  Debug( c ) << ")" << std::endl;
 }
 
-
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9cfa16adf..f30f1e8a0 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file equality_engine.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King, Kshitij Bansal, Dejan Jovanovic, Liana Hadarean, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -140,6 +140,18 @@ public:
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 };/* class EqualityEngineNotifyNone */
 
+/**
+ * An interface for equality engine notifications during equality path reconstruction.
+ * Can be used to add theory-specific logic for, e.g., proof construction.
+ */
+class PathReconstructionNotify {
+public:
+
+  virtual ~PathReconstructionNotify() {}
+
+  virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
+                      std::vector<TNode>& equalities, EqProof* proof) const = 0;
+};
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
@@ -218,6 +230,9 @@ private:
   /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
   KindMap d_congruenceKindsInterpreted;
 
+  /** Objects that need to be notified during equality path reconstruction */
+  std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
+
   /** Map from nodes to their ids */
   __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
@@ -259,6 +274,9 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
+  /** A fresh merge reason type to return upon request */
+  unsigned d_freshMergeReasonType;
+
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -289,7 +307,7 @@ private:
     // The next edge
     EqualityEdgeId d_nextId;
     // Type of reason for this equality
-    MergeReasonType d_mergeType;
+    unsigned d_mergeType;
     // Reason of this equality
     TNode d_reason;
 
@@ -298,7 +316,7 @@ private:
     EqualityEdge():
       d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
 
-    EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason):
+    EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason):
       d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
 
     /** Returns the id of the next edge */
@@ -308,7 +326,7 @@ private:
     EqualityNodeId getNodeId() const { return d_nodeId; }
 
     /** The reason of this edge */
-    MergeReasonType getReasonType() const { return d_mergeType; }
+    unsigned getReasonType() const { return d_mergeType; }
 
     /** The reason of this edge */
     TNode getReason() const { return d_reason; }
@@ -333,7 +351,7 @@ private:
   std::vector<EqualityEdgeId> d_equalityGraph;
 
   /** Add an edge to the equality graph */
-  void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason);
+  void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason);
 
   /** Returns the equality node of the given node */
   EqualityNode& getEqualityNode(TNode node);
@@ -505,7 +523,7 @@ private:
   /**
    * Adds an equality of terms t1 and t2 to the database.
    */
-  void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds a trigger equality to the database with the trigger node and polarity for notification.
@@ -729,7 +747,7 @@ public:
    *                 asserting the negated predicate
    * @param reason the reason to keep for building explanations
    */
-  void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds predicate p and q and makes them equal.
@@ -744,7 +762,7 @@ public:
    *                 asserting the negated equality
    * @param reason the reason to keep for building explanations
    */
-  void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Returns the current representative of the term t.
@@ -833,6 +851,15 @@ public:
    */
   bool consistent() const { return !d_done; }
 
+  /**
+   * Marks an object for merge type based notification during equality path reconstruction.
+   */
+  void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify);
+
+  /**
+   * Returns a fresh merge reason type tag for the client to use.
+   */
+  unsigned getFreshMergeReasonType();
 };
 
 /**
@@ -876,7 +903,7 @@ class EqProof
 {
 public:
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
-  MergeReasonType d_id;
+  unsigned d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
   void debug_print( const char * c, unsigned tb = 0 ) const;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index fb1e73575..346aebca7 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file equality_engine_types.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Andrew Reynolds, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -67,14 +67,11 @@ enum MergeReasonType {
   MERGED_THROUGH_REFLEXIVITY,
   /** Equality was merged to false, due to both sides of equality being a constant */
   MERGED_THROUGH_CONSTANTS,
-
   /** (for proofs only) Equality was merged due to transitivity */
   MERGED_THROUGH_TRANS,
 
-  /** Theory specific proof rules */
-  MERGED_ARRAYS_ROW,
-  MERGED_ARRAYS_ROW1,
-  MERGED_ARRAYS_EXT
+  /** Reason types beyond this constant are theory specific reasons */
+  NUMBER_OF_MERGE_REASONS
 };
 
 inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
@@ -91,10 +88,10 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_CONSTANTS:
     out << "constants disequal";
     break;
-  // (for proofs only)
   case MERGED_THROUGH_TRANS:
     out << "transitivity";
     break;
+
   default:
     out << "[theory]";
     break;
@@ -108,9 +105,9 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
  */
 struct MergeCandidate {
   EqualityNodeId t1Id, t2Id;
-  MergeReasonType type;
+  unsigned type;
   TNode reason;
-  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+  MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason)
   : t1Id(x), t2Id(y), type(type), reason(reason)
   {}
 };
@@ -365,4 +362,3 @@ struct TriggerInfo {
 } // namespace eq
 } // namespace theory
 } // namespace CVC4
-
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 4f7a2667c..ed5d99bdf 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file symmetry_breaker.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
  ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 5523c1c0d..b706f340f 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file symmetry_breaker.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
  ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ffb537734..0c7bed773 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is the interface to TheoryUF implementations
  **
@@ -105,6 +105,8 @@ void TheoryUF::check(Effort level) {
     TNode fact = assertion.assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+    Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;
+
     if (d_thss != NULL) {
       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
       d_thss->assertNode(fact, isDecision);
@@ -219,9 +221,15 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
   }
   if( pf ){
-    Debug("uf-pf") << std::endl;
-    pf->debug_print("uf-pf");
+    Debug("pf::uf") << std::endl;
+    pf->debug_print("pf::uf");
+  }
+
+  Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t";
+  for (unsigned i = 0; i < assumptions.size(); ++i) {
+    Debug("pf::uf") << assumptions[i] << " ";
   }
+  Debug("pf::uf") << std::endl;
 }
 
 Node TheoryUF::explain(TNode literal) {
@@ -270,6 +278,7 @@ void TheoryUF::presolve() {
     for(vector<Node>::const_iterator i = newClauses.begin();
         i != newClauses.end();
         ++i) {
+      Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
       d_out->lemma(*i);
     }
   }
@@ -521,7 +530,7 @@ void TheoryUF::conflict(TNode a, TNode b) {
   } else {
     d_conflictNode = explain(a.eqNode(b),pf);
   }
-  ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
+  ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
   d_out->conflict(d_conflictNode, puf);
   d_conflict = true;
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index e29b923f9..42a804c09 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: Dejan Jovanovic, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief This is the interface to TheoryUF implementations
  **
@@ -136,7 +136,7 @@ private:
    * Explain a literal, with proof (if "pf" is non-NULL).
    */
   Node explain(TNode literal, eq::EqProof* pf);
-  
+
   /** Literals to propagate */
   context::CDList<Node> d_literalsToPropagate;
 
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 6d0123a19..f6568ad7f 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_model.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of Theory UF Model
  **/
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 970a7d6b3..39e7ee6f0 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_model.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Model for Theory UF
  **/
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 82dacb6c2..166d11451 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_rewriter.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 3ed1c4d40..ed28cc2fc 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_strong_solver.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Clark Barrett
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of theory uf strong solver class
  **/
@@ -29,17 +29,44 @@
 //#define LAZY_REL_EQC
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
 
-void StrongSolverTheoryUF::SortModel::Region::addRep( Node n ) {
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+/* These are names are unambigious are we use abbreviations. */
+typedef StrongSolverTheoryUF::SortModel SortModel;
+typedef SortModel::Region Region;
+typedef Region::RegionNodeInfo RegionNodeInfo;
+typedef RegionNodeInfo::DiseqList DiseqList;
+
+Region::Region(SortModel* cf, context::Context* c)
+  : d_cf( cf )
+  , d_testCliqueSize( c, 0 )
+  , d_splitsSize( c, 0 )
+  , d_testClique( c )
+  , d_splits( c )
+  , d_reps_size( c, 0 )
+  , d_total_diseq_external( c, 0 )
+  , d_total_diseq_internal( c, 0 )
+  , d_valid( c, true ) {}
+
+Region::~Region() {
+  for(iterator i = begin(), iend = end(); i != iend; ++i) {
+    RegionNodeInfo* regionNodeInfo = (*i).second;
+    delete regionNodeInfo;
+  }
+  d_nodes.clear();
+}
+
+void Region::addRep( Node n ) {
   setRep( n, true );
 }
 
-void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::SortModel::Region* r, Node n ){
+void Region::takeNode( Region* r, Node n ){
   Assert( !hasRep( n ) );
   Assert( r->hasRep( n ) );
   //add representative
@@ -47,8 +74,8 @@ void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::So
   //take disequalities from r
   RegionNodeInfo* rni = r->d_nodes[n];
   for( int t=0; t<2; t++ ){
-    RegionNodeInfo::DiseqList* del = rni->d_disequalities[t];
-    for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+    DiseqList* del = rni->get(t);
+    for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
       if( (*it).second ){
         r->setDisequal( n, (*it).first, t, false );
         if( t==0 ){
@@ -71,21 +98,22 @@ void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::So
   r->setRep( n, false );
 }
 
-void StrongSolverTheoryUF::SortModel::Region::combine( StrongSolverTheoryUF::SortModel::Region* r ){
+void Region::combine( Region* r ){
   //take all nodes from r
-  for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
-    if( it->second->d_valid ){
+  for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) {
+    if( it->second->valid() ){
       setRep( it->first, true );
     }
   }
-  for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
-    if( it->second->d_valid ){
+  for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){
+    if( it->second->valid() ){
       //take disequalities from r
       Node n = it->first;
       RegionNodeInfo* rni = it->second;
       for( int t=0; t<2; t++ ){
-        RegionNodeInfo::DiseqList* del = rni->d_disequalities[t];
-        for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+        RegionNodeInfo::DiseqList* del = rni->get(t);
+        for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
+               it2end = del->end(); it2 != it2end; ++it2 ){
           if( (*it2).second ){
             if( t==0 && hasRep( (*it2).first ) ){
               setDisequal( (*it2).first, n, 0, false );
@@ -103,12 +131,12 @@ void StrongSolverTheoryUF::SortModel::Region::combine( StrongSolverTheoryUF::Sor
 }
 
 /** setEqual */
-void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){
+void Region::setEqual( Node a, Node b ){
   Assert( hasRep( a ) && hasRep( b ) );
   //move disequalities of b over to a
   for( int t=0; t<2; t++ ){
-    RegionNodeInfo::DiseqList* del = d_nodes[b]->d_disequalities[t];
-    for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+    DiseqList* del = d_nodes[b]->get(t);
+    for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
       if( (*it).second ){
         Node n = (*it).first;
         //get the region that contains the endpoint of the disequality b != ...
@@ -133,12 +161,13 @@ void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){
   setRep( b, false );
 }
 
-void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int type, bool valid ){
-  //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " << type << " " << valid << std::endl;
+void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
+  //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
+  //                            << type << " " << valid << std::endl;
   //debugPrint("uf-ss-region-debug");
   //Assert( isDisequal( n1, n2, type )!=valid );
   if( isDisequal( n1, n2, type )!=valid ){    //DO_THIS: make assertion
-    d_nodes[ n1 ]->d_disequalities[type]->setDisequal( n2, valid );
+    d_nodes[ n1 ]->get(type)->setDisequal( n2, valid );
     if( type==0 ){
       d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
     }else{
@@ -149,7 +178,8 @@ void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int
             d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
           Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
           if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
-            Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2 << std::endl;
+            Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2
+                                 << std::endl;
             d_splits[ eq ] = false;
             d_splitsSize = d_splitsSize - 1;
           }
@@ -159,20 +189,20 @@ void StrongSolverTheoryUF::SortModel::Region::setDisequal( Node n1, Node n2, int
   }
 }
 
-void StrongSolverTheoryUF::SortModel::Region::setRep( Node n, bool valid ){
+void Region::setRep( Node n, bool valid ) {
   Assert( hasRep( n )!=valid );
   if( valid && d_nodes.find( n )==d_nodes.end() ){
     d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
   }
-  d_nodes[n]->d_valid = valid;
+  d_nodes[n]->setValid(valid);
   d_reps_size = d_reps_size + ( valid ? 1 : -1 );
   //removing a member of the test clique from this region
-  if( d_testClique.find( n )!=d_testClique.end() && d_testClique[n] ){
+  if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
     Assert( !valid );
     d_testClique[n] = false;
     d_testCliqueSize = d_testCliqueSize - 1;
     //remove all splits involving n
-    for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){
+    for( split_iterator it = begin_splits(); it != end_splits(); ++it ){
       if( (*it).second ){
         if( (*it).first[0]==n || (*it).first[1]==n ){
           d_splits[ (*it).first ] = false;
@@ -183,33 +213,41 @@ void StrongSolverTheoryUF::SortModel::Region::setRep( Node n, bool valid ){
   }
 }
 
-bool StrongSolverTheoryUF::SortModel::Region::isDisequal( Node n1, Node n2, int type ){
-  RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->d_disequalities[type];
-  return del->d_disequalities.find( n2 )!=del->d_disequalities.end() && del->d_disequalities[n2];
+bool Region::isDisequal( Node n1, Node n2, int type ) {
+  RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type);
+  return del->isSet(n2) && del->getDisequalityValue(n2);
 }
 
 struct sortInternalDegree {
-  StrongSolverTheoryUF::SortModel::Region* r;
-  bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());}
+  Region* r;
+  bool operator() (Node i, Node j) {
+    return (r->getRegionInfo(i)->getNumInternalDisequalities() >
+            r->getRegionInfo(j)->getNumInternalDisequalities());
+  }
 };
 
 struct sortExternalDegree {
-  StrongSolverTheoryUF::SortModel::Region* r;
-  bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumExternalDisequalities()>r->d_nodes[j]->getNumExternalDisequalities());}
+  Region* r;
+  bool operator() (Node i,Node j) {
+    return (r->getRegionInfo(i)->getNumExternalDisequalities() >
+            r->getRegionInfo(j)->getNumExternalDisequalities());
+  }
 };
 
 int gmcCount = 0;
 
-bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){
+bool Region::getMustCombine( int cardinality ){
   if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){
-    //The number of external disequalities is greater than or equal to cardinality.
-    //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions
-    //Check if this is actually the case:  must have n nodes with outgoing degree (cardinality+1-n) for some n>0
+    //The number of external disequalities is greater than or equal to
+    //cardinality.  Thus, a clique of size cardinality+1 may exist
+    //between nodes in d_regions[i] and other regions Check if this is
+    //actually the case: must have n nodes with outgoing degree
+    //(cardinality+1-n) for some n>0
     std::vector< int > degrees;
-    for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+    for( Region::iterator it = begin(); it != end(); ++it ){
       RegionNodeInfo* rni = it->second;
-      if( rni->d_valid ){
-        if( rni->getNumDisequalities()>=cardinality ){
+      if( rni->valid() ){
+        if( rni->getNumDisequalities() >= cardinality ){
           int outDeg = rni->getNumExternalDisequalities();
           if( outDeg>=cardinality ){
             //we have 1 node of degree greater than (cardinality)
@@ -226,7 +264,8 @@ bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){
     }
     gmcCount++;
     if( gmcCount%100==0 ){
-      Trace("gmc-count") << gmcCount << " " << cardinality << " sample : " << degrees.size() << std::endl;
+      Trace("gmc-count") << gmcCount << " " << cardinality
+                         << " sample : " << degrees.size() << std::endl;
     }
     //this should happen relatively infrequently....
     std::sort( degrees.begin(), degrees.end() );
@@ -239,13 +278,14 @@ bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){
   return false;
 }
 
-bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
+bool Region::check( Theory::Effort level, int cardinality,
+                    std::vector< Node >& clique ) {
   if( d_reps_size>unsigned(cardinality) ){
     if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
       if( d_reps_size>1 ){
         //quick clique check, all reps form a clique
-        for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
-          if( it->second->d_valid ){
+        for( iterator it = begin(); it != end(); ++it ){
+          if( it->second->valid() ){
             clique.push_back( it->first );
           }
         }
@@ -254,15 +294,19 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
       }else{
         return false;
       }
-    }else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){
+    }else if( options::ufssRegions() || options::ufssEagerSplits() ||
+              level==Theory::EFFORT_FULL ) {
       //build test clique, up to size cardinality+1
       if( d_testCliqueSize<=unsigned(cardinality) ){
         std::vector< Node > newClique;
         if( d_testCliqueSize<unsigned(cardinality) ){
-          for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+          for( iterator it = begin(); it != end(); ++it ){
             //if not in the test clique, add it to the set of new members
-            if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){
-              //if( it->second->getNumInternalDisequalities()>cardinality || level==Theory::EFFORT_FULL ){
+            if( it->second->valid() &&
+                ( d_testClique.find( it->first ) == d_testClique.end() ||
+                  !d_testClique[ it->first ] ) ){
+              //if( it->second->getNumInternalDisequalities()>cardinality ||
+              //    level==Theory::EFFORT_FULL ){
               newClique.push_back( it->first );
               //}
             }
@@ -271,14 +315,18 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
           sortInternalDegree sidObj;
           sidObj.r = this;
           std::sort( newClique.begin(), newClique.end(), sidObj );
-          newClique.erase( newClique.begin() + ( cardinality - d_testCliqueSize ) + 1, newClique.end() );
+          int offset = ( cardinality - d_testCliqueSize ) + 1;
+          newClique.erase( newClique.begin() + offset, newClique.end() );
         }else{
           //scan for the highest degree
           int maxDeg = -1;
           Node maxNode;
-          for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+          for( std::map< Node, RegionNodeInfo* >::iterator
+                 it = d_nodes.begin(); it != d_nodes.end(); ++it ){
             //if not in the test clique, add it to the set of new members
-            if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){
+            if( it->second->valid() &&
+                ( d_testClique.find( it->first )==d_testClique.end() ||
+                  !d_testClique[ it->first ] ) ){
               if( it->second->getNumInternalDisequalities()>maxDeg ){
                 maxDeg = it->second->getNumInternalDisequalities();
                 maxNode = it->first;
@@ -290,18 +338,27 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
         }
         //check splits internal to new members
         for( int j=0; j<(int)newClique.size(); j++ ){
-          Debug("uf-ss-debug") << "Choose to add clique member " << newClique[j] << std::endl;
+          Debug("uf-ss-debug") << "Choose to add clique member "
+                               << newClique[j] << std::endl;
           for( int k=(j+1); k<(int)newClique.size(); k++ ){
             if( !isDisequal( newClique[j], newClique[k], 1 ) ){
-              d_splits[ NodeManager::currentNM()->mkNode( EQUAL, newClique[j], newClique[k] ) ] = true;
+              Node at_j = newClique[j];
+              Node at_k = newClique[k];              
+              Node j_eq_k =
+                NodeManager::currentNM()->mkNode( EQUAL, at_j, at_k );
+              d_splits[ j_eq_k ] = true;
               d_splitsSize = d_splitsSize + 1;
             }
           }
           //check disequalities with old members
-          for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+          for( NodeBoolMap::iterator it = d_testClique.begin();
+               it != d_testClique.end(); ++it ){
             if( (*it).second ){
               if( !isDisequal( (*it).first, newClique[j], 1 ) ){
-                d_splits[ NodeManager::currentNM()->mkNode( EQUAL, (*it).first, newClique[j] ) ] = true;
+                Node at_it = (*it).first;
+                Node at_j = newClique[j];
+                Node it_eq_j = at_it.eqNode(at_j);
+                d_splits[ it_eq_j ] = true;
                 d_splitsSize = d_splitsSize + 1;
               }
             }
@@ -313,10 +370,12 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
           d_testCliqueSize = d_testCliqueSize + 1;
         }
       }
-      //check if test clique has larger size than cardinality, and forms a clique
-      if( d_testCliqueSize>=unsigned(cardinality+1) && d_splitsSize==0 ){
+      // Check if test clique has larger size than cardinality, and
+      // forms a clique.
+      if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){
         //test clique is a clique
-        for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+        for( NodeBoolMap::iterator it = d_testClique.begin();
+             it != d_testClique.end(); ++it ){
           if( (*it).second ){
             clique.push_back( (*it).first );
           }
@@ -328,10 +387,12 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c
   return false;
 }
 
-bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) {
+bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique )
+{
   if( d_testCliqueSize>=unsigned(cardinality+1) ){
     //test clique is a clique
-    for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+    for( NodeBoolMap::iterator it = d_testClique.begin();
+         it != d_testClique.end(); ++it ){
       if( (*it).second ){
         clique.push_back( (*it).first );
       }
@@ -341,12 +402,13 @@ bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinalit
   return false;
 }
 
-void StrongSolverTheoryUF::SortModel::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
-  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+void Region::getNumExternalDisequalities(
+    std::map< Node, int >& num_ext_disequalities ){
+  for( Region::iterator it = begin(); it != end(); ++it ){
     RegionNodeInfo* rni = it->second;
-    if( rni->d_valid ){
-      RegionNodeInfo::DiseqList* del = rni->d_disequalities[0];
-      for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+    if( rni->valid() ){
+      DiseqList* del = rni->get(0);
+      for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
         if( (*it2).second ){
           num_ext_disequalities[ (*it2).first ]++;
         }
@@ -355,32 +417,35 @@ void StrongSolverTheoryUF::SortModel::Region::getNumExternalDisequalities( std::
   }
 }
 
-void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool incClique ){
+void Region::debugPrint( const char* c, bool incClique ) {
   Debug( c ) << "Num reps: " << d_reps_size << std::endl;
-  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+  for( Region::iterator it = begin(); it != end(); ++it ){
     RegionNodeInfo* rni = it->second;
-    if( rni->d_valid ){
+    if( rni->valid() ){
       Node n = it->first;
       Debug( c ) << "   " << n << std::endl;
       for( int i=0; i<2; i++ ){
         Debug( c ) << "      " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
-        RegionNodeInfo::DiseqList* del = rni->d_disequalities[i];
-        for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+        DiseqList* del = rni->get(i);
+        for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
           if( (*it2).second ){
             Debug( c ) << " " << (*it2).first;
           }
         }
-        Debug( c ) << ", total = " << del->d_size << std::endl;
+        Debug( c ) << ", total = " << del->size() << std::endl;
       }
     }
   }
-  Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," << std::endl;
-  Debug( c ) << "                " << d_total_diseq_internal<< " internal." << std::endl;
+  Debug( c ) << "Total disequal: " << d_total_diseq_external << " external,"
+             << std::endl;
+  Debug( c ) << "                " << d_total_diseq_internal << " internal."
+             << std::endl;
 
   if( incClique ){
     Debug( c ) << "Candidate clique members: " << std::endl;
     Debug( c ) << "   ";
-    for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++ it ){
+    for( NodeBoolMap::iterator it = d_testClique.begin();
+         it != d_testClique.end(); ++ it ){
       if( (*it).second ){
         Debug( c ) << (*it).first << " ";
       }
@@ -388,7 +453,8 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
     Debug( c ) << ", size = " << d_testCliqueSize << std::endl;
     Debug( c ) << "Required splits: " << std::endl;
     Debug( c ) << "   ";
-    for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++ it ){
+    for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
+         ++ it ){
       if( (*it).second ){
         Debug( c ) << (*it).first << " ";
       }
@@ -397,17 +463,25 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
   }
 }
 
-
-
-
-
-
-
-
-StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
-          d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
-          d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
+SortModel::SortModel( Node n,
+                      context::Context* c,
+                      context::UserContext* u,
+                      StrongSolverTheoryUF* thss )
+  : d_type( n.getType() )
+  , d_thss( thss )
+  , d_regions_index( c, 0 )
+  , d_regions_map( c )
+  , d_split_score( c )
+  , d_disequalities_index( c, 0 )
+  , d_reps( c, 0 )
+  , d_conflict( c, false )
+  , d_cardinality( c, 1 )
+  , d_aloc_cardinality( u, 0 )
+  , d_hasCard( c, false )
+  , d_maxNegCard( c, 0 )
+  , d_initialized( u, false )
+  , d_lemma_cache( u )
+{
   d_cardinality_term = n;
   //if( d_type.isSort() ){
   //  TypeEnumerator te(tn);
@@ -417,8 +491,17 @@ StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context
   //}
 }
 
+SortModel::~SortModel() {
+  for(std::vector<Region*>::iterator i = d_regions.begin();
+      i != d_regions.end(); ++i) {
+    Region* region = *i;
+    delete region;
+  }
+  d_regions.clear();
+}
+
 /** initialize */
-void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
+void SortModel::initialize( OutputChannel* out ){
   if( !d_initialized ){
     d_initialized = true;
     allocateCardinality( out );
@@ -426,17 +509,20 @@ void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
 }
 
 /** new node */
-void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
+void SortModel::newEqClass( Node n ){
   if( !d_conflict ){
     if( d_regions_map.find( n )==d_regions_map.end() ){
-      //must generate totality axioms for every cardinality we have allocated thus far
-      for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
+      // Must generate totality axioms for every cardinality we have
+      // allocated thus far.
+      for( std::map< int, Node >::iterator it = d_cardinality_literal.begin();
+           it != d_cardinality_literal.end(); ++it ){
         if( applyTotality( it->first ) ){
           addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
         }
       }
       if( options::ufssTotality() ){
-        //regions map will store whether we need to equate this term with a constant equivalence class
+        // Regions map will store whether we need to equate this term
+        // with a constant equivalence class.
         if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
           d_regions_map[n] = 0;
         }else{
@@ -444,16 +530,20 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
         }
       }else{
         if( !options::ufssRegions() ){
-          //if not using regions, always add new equivalence classes to region index = 0
+          // If not using regions, always add new equivalence classes
+          // to region index = 0.
           d_regions_index = 0;
         }
         d_regions_map[n] = d_regions_index;
-        Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n << std::endl;
-        Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
+        Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n
+                       << std::endl;
+        Debug("uf-ss-debug") << d_regions_index << " "
+                             << (int)d_regions.size() << std::endl;
         if( d_regions_index<d_regions.size() ){
           d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
-          d_regions[ d_regions_index ]->d_valid = true;
-          Assert( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 );
+          d_regions[ d_regions_index ]->setValid(true);
+          Assert( !options::ufssRegions() ||
+                  d_regions[ d_regions_index ]->getNumReps()==0 );
         }else{
           d_regions.push_back( new Region( this, d_thss->getSatContext() ) );
         }
@@ -466,7 +556,7 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
 }
 
 /** merge */
-void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
+void SortModel::merge( Node a, Node b ){
   if( !d_conflict ){
     if( options::ufssTotality() ){
       if( d_regions_map[b]==-1 ){
@@ -476,7 +566,8 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
     }else{
       //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
       //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
-      Debug("uf-ss") << "StrongSolverTheoryUF: Merging " << a << " = " << b << "..." << std::endl;
+      Debug("uf-ss") << "StrongSolverTheoryUF: Merging "
+                     << a << " = " << b << "..." << std::endl;
       if( a!=b ){
         Assert( d_regions_map.find( a )!=d_regions_map.end() );
         Assert( d_regions_map.find( b )!=d_regions_map.end() );
@@ -493,10 +584,15 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
             d_regions[ri]->setEqual( a, b );
             checkRegion( ri );
           }else{
-            // either move a to d_regions[bi], or b to d_regions[ai]
-            int aex = d_regions[ai]->d_nodes[a]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( a, bi );
-            int bex = d_regions[bi]->d_nodes[b]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( b, ai );
-            //based on which would produce the fewest number of external disequalities
+            // Either move a to d_regions[bi], or b to d_regions[ai].
+            RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
+            RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
+            int aex = ( a_region_info->getNumInternalDisequalities() -
+                        getNumDisequalitiesToRegion( a, bi ) );
+            int bex = ( b_region_info->getNumInternalDisequalities() -
+                        getNumDisequalitiesToRegion( b, ai ) );
+            // Based on which would produce the fewest number of
+            // external disequalities.
             if( aex<bex ){
               moveNode( a, bi );
               d_regions[bi]->setEqual( a, b );
@@ -529,7 +625,7 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
 }
 
 /** assert terms are disequal */
-void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reason ){
+void SortModel::assertDisequal( Node a, Node b, Node reason ){
   if( !d_conflict ){
     if( options::ufssTotality() ){
       //do nothing
@@ -584,7 +680,7 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso
   }
 }
 
-bool StrongSolverTheoryUF::SortModel::areDisequal( Node a, Node b ) {
+bool SortModel::areDisequal( Node a, Node b ) {
   Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) );
   Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) );
   if( d_regions_map.find( a )!=d_regions_map.end() &&
@@ -598,7 +694,7 @@ bool StrongSolverTheoryUF::SortModel::areDisequal( Node a, Node b ) {
 }
 
 /** check */
-void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel* out ){
+void SortModel::check( Theory::Effort level, OutputChannel* out ){
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
     Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl;
     //Notice() << "StrongSolverTheoryUF: Check " << level << std::endl;
@@ -616,7 +712,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
       if( !options::ufssTotality() ){
         //do a check within each region
         for( int i=0; i<(int)d_regions_index; i++ ){
-          if( d_regions[i]->d_valid ){
+          if( d_regions[i]->valid() ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
               if( options::ufssMode()==UF_SS_FULL ){
@@ -637,7 +733,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           Trace("uf-ss-debug") << "Add splits?" << std::endl;
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
-            if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){
+            if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
               //just add the clique lemma
               if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
                 std::vector< Node > clique;
@@ -661,18 +757,19 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
             }
           }
         }
-        //if no added lemmas, force continuation via combination of regions
+        //If no added lemmas, force continuation via combination of regions.
         if( level==Theory::EFFORT_FULL ){
           if( !addedLemma ){
-            Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
+            Trace("uf-ss-debug") << "No splits added. " << d_cardinality
+                                 << std::endl;
             Trace("uf-ss-si")  << "Must combine region" << std::endl;
             bool recheck = false;
             if( options::sortInference()){
-              //if sort inference is enabled, search for regions with same sort
+              //If sort inference is enabled, search for regions with same sort.
               std::map< int, int > sortsFound;
               for( int i=0; i<(int)d_regions_index; i++ ){
-                if( d_regions[i]->d_valid ){
-                  Node op = d_regions[i]->d_nodes.begin()->first;
+                if( d_regions[i]->valid() ){
+                  Node op = d_regions[i]->frontKey();
                   int sort_id = d_thss->getSortInference()->getSortId(op);
                   if( sortsFound.find( sort_id )!=sortsFound.end() ){
                     combineRegions( sortsFound[sort_id], i );
@@ -687,7 +784,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
             if( !recheck ) {
               //naive strategy, force region combination involving the first valid region
               for( int i=0; i<(int)d_regions_index; i++ ){
-                if( d_regions[i]->d_valid ){
+                if( d_regions[i]->valid() ){
                   int fcr = forceCombineRegion( i, false );
                   Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
                   if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){
@@ -708,26 +805,28 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
   }
 }
 
-void StrongSolverTheoryUF::SortModel::presolve() {
+void SortModel::presolve() {
   d_initialized = false;
   d_aloc_cardinality = 0;
 }
 
-void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){
+void SortModel::propagate( Theory::Effort level, OutputChannel* out ){
 
 }
 
-Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
+Node SortModel::getNextDecisionRequest(){
   //request the current cardinality as a decision literal, if not already asserted
   for( int i=1; i<=d_aloc_cardinality; i++ ){
     if( !d_hasCard || i<d_cardinality ){
       Node cn = d_cardinality_literal[ i ];
       Assert( !cn.isNull() );
-      if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
+      bool value;
+      if( !d_thss->getTheory()->d_valuation.hasSatValue( cn, value ) ){
         Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
         return cn;
       }else{
-        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl;
+        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << value << std::endl;
+        Assert( !value );
       }
     }
   }
@@ -737,7 +836,7 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
   return Node::null();
 }
 
-bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* m ){
+bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
   if( options::ufssTotality() ){
     //do nothing
   }else{
@@ -774,7 +873,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel*
       // if two equivalence classes are neither equal nor disequal, add a split
       int validRegionIndex = -1;
       for( int i=0; i<(int)d_regions_index; i++ ){
-        if( d_regions[i]->d_valid ){
+        if( d_regions[i]->valid() ){
           if( validRegionIndex!=-1 ){
             combineRegions( validRegionIndex, i );
             if( addSplit( d_regions[validRegionIndex], out )!=0 ){
@@ -798,11 +897,11 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel*
 }
 
 
-int StrongSolverTheoryUF::SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
+int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
   int ni = d_regions_map[n];
   int counter = 0;
-  Region::RegionNodeInfo::DiseqList* del = d_regions[ni]->d_nodes[n]->d_disequalities[0];
-  for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+  DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
+  for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
     if( (*it).second ){
       if( d_regions_map[ (*it).first ]==ri ){
         counter++;
@@ -812,12 +911,14 @@ int StrongSolverTheoryUF::SortModel::getNumDisequalitiesToRegion( Node n, int ri
   return counter;
 }
 
-void StrongSolverTheoryUF::SortModel::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){
-  for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[ri]->d_nodes.begin();
-       it != d_regions[ri]->d_nodes.end(); ++it ){
-    if( it->second->d_valid ){
-      Region::RegionNodeInfo::DiseqList* del = it->second->d_disequalities[0];
-      for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+void SortModel::getDisequalitiesToRegions(int ri,
+                                          std::map< int, int >& regions_diseq)
+{
+  Region* region = d_regions[ri];
+  for(Region::iterator it = region->begin(); it != region->end(); ++it ){
+    if( it->second->valid() ){
+      DiseqList* del = it->second->get(0);
+      for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
         if( (*it2).second ){
           Assert( isValid( d_regions_map[ (*it2).first ] ) );
           //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
@@ -828,7 +929,7 @@ void StrongSolverTheoryUF::SortModel::getDisequalitiesToRegions( int ri, std::ma
   }
 }
 
-void StrongSolverTheoryUF::SortModel::setSplitScore( Node n, int s ){
+void SortModel::setSplitScore( Node n, int s ){
   if( d_split_score.find( n )!=d_split_score.end() ){
     int ss = d_split_score[ n ];
     d_split_score[ n ] = s>ss ? s : ss;
@@ -840,13 +941,13 @@ void StrongSolverTheoryUF::SortModel::setSplitScore( Node n, int s ){
   }
 }
 
-void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
+void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
   if( !d_conflict ){
-    Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = ";
-    Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
+    Trace("uf-ss-assert")
+      << "Assert cardinality "<< d_type << " " << c << " " << val << " level = "
+      << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
     Assert( c>0 );
     Node cl = getCardinalityLiteral( c );
-    d_cardinality_assertions[ cl ] = val;
     if( val ){
       bool doCheckRegions = !d_hasCard;
       bool prevHasCard = d_hasCard;
@@ -861,7 +962,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
       //should check all regions now
       if( doCheckRegions ){
         for( int i=0; i<(int)d_regions_index; i++ ){
-          if( d_regions[i]->d_valid ){
+          if( d_regions[i]->valid() ){
             checkRegion( i );
             if( d_conflict ){
               return;
@@ -890,8 +991,9 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
         bool needsCard = true;
         for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
           if( it->first<=d_aloc_cardinality.get() ){
-            if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
-              Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
+            bool value;
+            if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){
+              Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl;
               needsCard = false;
               break;
             }
@@ -912,7 +1014,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
   }
 }
 
-void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
+void SortModel::checkRegion( int ri, bool checkCombine ){
   if( isValid(ri) && d_hasCard ){
     Assert( d_cardinality>0 );
     if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
@@ -941,10 +1043,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
   }
 }
 
-int StrongSolverTheoryUF::SortModel::forceCombineRegion( int ri, bool useDensity ){
+int SortModel::forceCombineRegion( int ri, bool useDensity ){
   if( !useDensity ){
     for( int i=0; i<(int)d_regions_index; i++ ){
-      if( ri!=i && d_regions[i]->d_valid ){
+      if( ri!=i && d_regions[i]->valid() ){
         return combineRegions( ri, i );
       }
     }
@@ -981,7 +1083,7 @@ int StrongSolverTheoryUF::SortModel::forceCombineRegion( int ri, bool useDensity
 }
 
 
-int StrongSolverTheoryUF::SortModel::combineRegions( int ai, int bi ){
+int SortModel::combineRegions( int ai, int bi ){
 #ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
   if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
     return combineRegions( bi, ai );
@@ -989,19 +1091,20 @@ int StrongSolverTheoryUF::SortModel::combineRegions( int ai, int bi ){
 #endif
   Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
   Assert( isValid( ai ) && isValid( bi ) );
-  for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[bi]->d_nodes.begin(); it != d_regions[bi]->d_nodes.end(); ++it ){
+  Region* region_bi = d_regions[bi];
+  for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
     Region::RegionNodeInfo* rni = it->second;
-    if( rni->d_valid ){
+    if( rni->valid() ){
       d_regions_map[ it->first ] = ai;
     }
   }
   //update regions disequal DO_THIS?
   d_regions[ai]->combine( d_regions[bi] );
-  d_regions[bi]->d_valid = false;
+  d_regions[bi]->setValid( false );
   return ai;
 }
 
-void StrongSolverTheoryUF::SortModel::moveNode( Node n, int ri ){
+void SortModel::moveNode( Node n, int ri ){
   Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
   Assert( isValid( d_regions_map[ n ] ) );
   Assert( isValid( ri ) );
@@ -1010,7 +1113,7 @@ void StrongSolverTheoryUF::SortModel::moveNode( Node n, int ri ){
   d_regions_map[n] = ri;
 }
 
-void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
+void SortModel::allocateCardinality( OutputChannel* out ){
   if( d_aloc_cardinality>0 ){
     Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl;
   }
@@ -1028,20 +1131,26 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 
   //allocate the lowest such that it is not asserted
   Node cl;
+  bool increment;
   do {
+    increment = false;
     d_aloc_cardinality = d_aloc_cardinality + 1;
     cl = getCardinalityLiteral( d_aloc_cardinality );
-  }while( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() && !d_cardinality_assertions[cl] );
-  //if one is already asserted postively, abort
-  if( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() ){
-    return;
-  }
+    bool value;
+    if( d_thss->getTheory()->d_valuation.hasSatValue( cl, value ) ){
+      if( value ){
+        //if one is already asserted postively, abort
+        return;
+      }else{
+        increment = true;
+      }
+    }
+  }while( increment );
 
   //check for abort case
   if( options::ufssAbortCardinality()==d_aloc_cardinality ){
-    //abort here DO_THIS
     Message() << "Maximum cardinality reached." << std::endl;
-    exit( 0 );
+    exit( 1 );
   }else{
     if( applyTotality( d_aloc_cardinality ) ){
       //must generate new cardinality lemma term
@@ -1093,11 +1202,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
   }
 }
 
-int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+int SortModel::addSplit( Region* r, OutputChannel* out ){
   Node s;
   if( r->hasSplits() ){
     //take the first split you find
-    for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+    for( Region::split_iterator it = r->begin_splits();
+         it != r->end_splits(); ++it ){
       if( (*it).second ){
         s = (*it).first;
         break;
@@ -1106,13 +1216,16 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
     Assert( s!=Node::null() );
   }else{
     if( options::ufssMode()!=UF_SS_FULL ){
-      //since candidate clique is not reported, we may need to find splits manually
-      for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
-        if ( it->second->d_valid ){
-          for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){
-            if ( it->second!=it2->second && it2->second->d_valid ){
+      // Since candidate clique is not reported, we may need to find
+      // splits manually.
+      for ( Region::iterator it = r->begin(); it != r->end(); ++it ){
+        if ( it->second->valid() ){
+          for ( Region::iterator it2 = r->begin(); it2 != r->end(); ++it2 ){
+            if ( it->second!=it2->second && it2->second->valid() ){
               if( !r->isDisequal( it->first, it2->first, 1 ) ){
-                s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first );
+                Node it_node = it->first;
+                Node it2_node = it2->first;
+                s = it_node.eqNode(it2_node);
               }
             }
           }
@@ -1128,7 +1241,8 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
       Node b_t = NodeManager::currentNM()->mkConst( true );
       Node b_f = NodeManager::currentNM()->mkConst( false );
       if( ss==b_f ){
-        Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl;
+        Trace("uf-ss-lemma") << "....Assert disequal directly : "
+                             << s[0] << " " << s[1] << std::endl;
         assertDisequal( s[0], s[1], b_t );
         return -1;
       }else{
@@ -1165,7 +1279,7 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
 }
 
 
-void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
   Assert( d_hasCard );
   Assert( d_cardinality>0 );
   while( clique.size()>size_t(d_cardinality+1) ){
@@ -1318,7 +1432,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
   }
 }
 
-void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
+void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
   if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
     if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
       d_totality_lems[n].push_back( cardinality );
@@ -1346,7 +1460,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
               for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
                 eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
               }
-              Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+              Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs );
               Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
               Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
               d_thss->getOutputChannel().lemma( lem );
@@ -1369,7 +1483,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
   }
 }
 
-void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) {
+void SortModel::addClique( int c, std::vector< Node >& clique ) {
   //if( d_clique_trie[c].add( clique ) ){
   //  d_cliques[ c ].push_back( clique );
   //}
@@ -1377,20 +1491,20 @@ void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& cli
 
 
 /** apply totality */
-bool StrongSolverTheoryUF::SortModel::applyTotality( int cardinality ){
+bool SortModel::applyTotality( int cardinality ){
   return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
   // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
 }
 
 /** get totality lemma terms */
-Node StrongSolverTheoryUF::SortModel::getTotalityLemmaTerm( int cardinality, int i ){
+Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
   return d_totality_terms[0][i];
   //}else{
   //  return d_totality_terms[cardinality][i];
   //}
 }
 
-void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() {
+void SortModel::simpleCheckCardinality() {
   if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
                                                       getCardinalityLiteral( d_maxNegCard.get() ).negate() );
@@ -1400,7 +1514,7 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() {
   }
 }
 
-bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) {
+bool SortModel::doSendLemma( Node lem ) {
   if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
     d_lemma_cache[lem] = true;
     d_thss->getOutputChannel().lemma( lem );
@@ -1410,32 +1524,36 @@ bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) {
   }
 }
 
-void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
+void SortModel::debugPrint( const char* c ){
   Debug( c ) << "--  Conflict Find:" << std::endl;
   Debug( c ) << "Number of reps = " << d_reps << std::endl;
   Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
   unsigned debugReps = 0;
   for( int i=0; i<(int)d_regions_index; i++ ){
-    if( d_regions[i]->d_valid ){
+    Region* region = d_regions[i]; 
+    if( region->valid() ){
       Debug( c ) << "Region #" << i << ": " << std::endl;
-      d_regions[i]->debugPrint( c, true );
+      region->debugPrint( c, true );
       Debug( c ) << std::endl;
-      for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[i]->d_nodes.begin(); it != d_regions[i]->d_nodes.end(); ++it ){
-        if( it->second->d_valid ){
+      for( Region::iterator it = region->begin(); it != region->end(); ++it ){
+        if( it->second->valid() ){
           if( d_regions_map[ it->first ]!=i ){
-            Debug( c ) << "***Bad regions map : " << it->first << " " << d_regions_map[ it->first ].get() << std::endl;
+            Debug( c ) << "***Bad regions map : " << it->first
+                       << " " << d_regions_map[ it->first ].get() << std::endl;
           }
         }
       }
-      debugReps += d_regions[i]->getNumReps();
+      debugReps += region->getNumReps();
     }
   }
+
   if( debugReps!=d_reps ){
-    Debug( c ) << "***Bad reps: " << d_reps << ", actual = " << debugReps << std::endl;
+    Debug( c ) << "***Bad reps: " << d_reps << ", "
+               << "actual = " << debugReps << std::endl;
   }
 }
 
-bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
+bool SortModel::debugModel( TheoryModel* m ){
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine );
@@ -1503,27 +1621,42 @@ bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
   return true;
 }
 
-int StrongSolverTheoryUF::SortModel::getNumRegions(){
+int SortModel::getNumRegions(){
   int count = 0;
   for( int i=0; i<(int)d_regions_index; i++ ){
-    if( d_regions[i]->d_valid ){
+    if( d_regions[i]->valid() ){
       count++;
     }
   }
   return count;
 }
 
-Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
-  if( d_cardinality_literal.find( c )==d_cardinality_literal.end() ){
-    d_cardinality_literal[c] = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
-                                                                 NodeManager::currentNM()->mkConst( Rational( c ) ) );
+Node SortModel::getCardinalityLiteral( int c ) {
+  if( d_cardinality_literal.find(c) == d_cardinality_literal.end() ){
+    Node c_as_rational = NodeManager::currentNM()->mkConst(Rational(c));
+    d_cardinality_literal[c] =
+      NodeManager::currentNM()->mkNode(CARDINALITY_CONSTRAINT,
+                                       d_cardinality_term,
+                                       c_as_rational);
+
   }
   return d_cardinality_literal[c];
 }
 
-StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
-d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), d_min_pos_com_card( c, -1 ),
-d_card_assertions_eqv_lemma( u ), d_min_pos_tn_master_card( c, -1 ), d_rel_eqc( c )
+StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
+                                           context::UserContext* u,
+                                           OutputChannel& out,
+                                           TheoryUF* th)
+  : d_out( &out )
+  , d_th( th )
+  , d_conflict( c, false )
+  , d_rep_model()
+  , d_aloc_com_card( u, 0 )
+  , d_com_card_assertions( c )
+  , d_min_pos_com_card( c, -1 )
+  , d_card_assertions_eqv_lemma( u )
+  , d_min_pos_tn_master_card( c, -1 )
+  , d_rel_eqc( c )
 {
   if( options::ufssDiseqPropagation() ){
     d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
@@ -1899,7 +2032,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
 //}
 
 
-StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
+SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
   TypeNode tn = n.getType();
   std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
   //pre-register the type if not done already
@@ -1914,9 +2047,7 @@ StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
   }
 }
 
-void StrongSolverTheoryUF::notifyRestart(){
-
-}
+void StrongSolverTheoryUF::notifyRestart(){}
 
 /** get cardinality for sort */
 int StrongSolverTheoryUF::getCardinality( Node n ) {
@@ -2021,27 +2152,31 @@ void StrongSolverTheoryUF::checkCombinedCardinality() {
         conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
         conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
         Node cf = NodeManager::currentNM()->mkNode( AND, conf );
-        Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict : " << cf << std::endl;
-        Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict : " << cf << std::endl;
+        Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
+                             << " : " << cf << std::endl;
+        Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
+                                << " : " << cf << std::endl;
         getOutputChannel().conflict( cf );
         d_conflict.set( true );
         return;
       }
     }
-    if( d_min_pos_com_card.get()!=-1 && totalCombinedCard>d_min_pos_com_card.get() ){
+    int cc = d_min_pos_com_card.get();
+    if( cc !=-1 && totalCombinedCard > cc ){
       //conflict
-      int cc = d_min_pos_com_card.get();
-      Assert( d_com_card_literal.find( cc )!=d_com_card_literal.end() );
+      Assert( d_com_card_literal.find( cc ) != d_com_card_literal.end() );
       Node com_lit = d_com_card_literal[cc];
-      Assert( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() );
+      Assert(d_com_card_assertions.find(com_lit)!=d_com_card_assertions.end());
       Assert( d_com_card_assertions[com_lit] );
       std::vector< Node > conf;
       conf.push_back( com_lit );
       int totalAdded = 0;
-      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); 
+           it != d_rep_model.end(); ++it ){
         bool doAdd = true;
         if( options::ufssFairnessMonotone() ){
-          std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
+          std::map< TypeNode, bool >::iterator its =
+            d_tn_mono_slave.find( it->first );
           if( its!=d_tn_mono_slave.end() && its->second ){
             doAdd = false;
           }
@@ -2058,8 +2193,10 @@ void StrongSolverTheoryUF::checkCombinedCardinality() {
         }
       }
       Node cf = NodeManager::currentNM()->mkNode( AND, conf );
-      Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf << std::endl;
-      Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf << std::endl;
+      Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
+                           << std::endl;
+      Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
+                              << std::endl;
       getOutputChannel().conflict( cf );
       d_conflict.set( true );
     }
@@ -2113,8 +2250,10 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
 }
 
 
-DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) :
-  d_qe(qe), d_ufss(ufss){
+DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe,
+                                             StrongSolverTheoryUF* ufss)
+  : d_qe(qe), d_ufss(ufss)
+{
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 }
@@ -2182,3 +2321,7 @@ DisequalityPropagator::Statistics::Statistics():
 DisequalityPropagator::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(& d_propagations);
 }
+
+}/* CVC4::theory namespace::uf */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index db4c50423..11f0664f3 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_strong_solver.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Theory uf strong solver
  **/
@@ -25,17 +25,19 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-
 class SortInference;
-
 namespace theory {
-
 class SubsortSymmetryBreaker;
-
 namespace uf {
-
 class TheoryUF;
 class DisequalityPropagator;
+} /* namespace CVC4::theory::uf */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
 
 class StrongSolverTheoryUF{
 protected:
@@ -44,83 +46,135 @@ protected:
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
 public:
-  /** information for incremental conflict/clique finding for a particular sort */
+  /**
+   * Information for incremental conflict/clique finding for a
+   * particular sort.
+   */
   class SortModel {
   private:
     std::map< Node, std::vector< int > > d_totality_lems;
     std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
     std::map< Node, int > d_sym_break_index;
   public:
-    /** a partition of the current equality graph for which cliques can occur internally */
+
+    /**
+     * A partition of the current equality graph for which cliques
+     * can occur internally.
+     */
     class Region {
     public:
-      /** conflict find pointer */
-      SortModel* d_cf;
       /** information stored about each node in region */
       class RegionNodeInfo {
       public:
         /** disequality list for node */
         class DiseqList {
         public:
-          DiseqList( context::Context* c ) : d_size( c, 0 ), d_disequalities( c ){}
+          DiseqList( context::Context* c )
+            : d_size( c, 0 ), d_disequalities( c ) {}
           ~DiseqList(){}
-          context::CDO< unsigned > d_size;
-          NodeBoolMap d_disequalities;
+
           void setDisequal( Node n, bool valid ){
-            Assert( d_disequalities.find( n )==d_disequalities.end() || d_disequalities[n]!=valid );
+            Assert( (!isSet(n)) || getDisequalityValue(n) != valid );
             d_disequalities[ n ] = valid;
             d_size = d_size + ( valid ? 1 : -1 );
           }
-        };
-      private:
-        DiseqList d_internal;
-        DiseqList d_external;
+          bool isSet(Node n) const {
+            return d_disequalities.find(n) != d_disequalities.end();
+          }
+          bool getDisequalityValue(Node n) const {
+            Assert(isSet(n));
+            return (*(d_disequalities.find(n))).second;
+          }
+
+          int size() const { return d_size; }
+          
+          typedef NodeBoolMap::iterator iterator;
+          iterator begin() { return d_disequalities.begin(); }
+          iterator end() { return d_disequalities.end(); }
+
+        private:
+          context::CDO< int > d_size;
+          NodeBoolMap d_disequalities;
+        }; /* class DiseqList */
       public:
         /** constructor */
-        RegionNodeInfo( context::Context* c ) :
-          d_internal( c ), d_external( c ), d_valid( c, true ){
+        RegionNodeInfo( context::Context* c )
+          : d_internal(c), d_external(c), d_valid(c, true) {
           d_disequalities[0] = &d_internal;
           d_disequalities[1] = &d_external;
         }
         ~RegionNodeInfo(){}
+       
+        int getNumDisequalities() const {
+          return d_disequalities[0]->size() + d_disequalities[1]->size();
+        }
+        int getNumExternalDisequalities() const {
+          return d_disequalities[0]->size();
+        }
+        int getNumInternalDisequalities() const {
+          return d_disequalities[1]->size();
+        }
+
+        bool valid() const { return d_valid; }
+        void setValid(bool valid) { d_valid = valid; }
+
+        DiseqList* get(unsigned i) { return d_disequalities[i]; }
+
+      private:
+        DiseqList d_internal;
+        DiseqList d_external;
         context::CDO< bool > d_valid;
         DiseqList* d_disequalities[2];
+      }; /* class RegionNodeInfo */
 
-        int getNumDisequalities() { return d_disequalities[0]->d_size + d_disequalities[1]->d_size; }
-        int getNumExternalDisequalities() { return d_disequalities[0]->d_size; }
-        int getNumInternalDisequalities() { return d_disequalities[1]->d_size; }
-      };
-      ///** end class RegionNodeInfo */
     private:
+      /** conflict find pointer */
+      SortModel* d_cf;
+
       context::CDO< unsigned > d_testCliqueSize;
       context::CDO< unsigned > d_splitsSize;
-    public:
       //a postulated clique
       NodeBoolMap d_testClique;
       //disequalities needed for this clique to happen
       NodeBoolMap d_splits;
-    private:
       //number of valid representatives in this region
       context::CDO< unsigned > d_reps_size;
       //total disequality size (external)
       context::CDO< unsigned > d_total_diseq_external;
       //total disequality size (internal)
       context::CDO< unsigned > d_total_diseq_internal;
-    private:
       /** set rep */
       void setRep( Node n, bool valid );
-    public:
-      //constructor
-      Region( SortModel* cf, context::Context* c ) : d_cf( cf ), d_testCliqueSize( c, 0 ),
-        d_splitsSize( c, 0 ), d_testClique( c ), d_splits( c ), d_reps_size( c, 0 ),
-        d_total_diseq_external( c, 0 ), d_total_diseq_internal( c, 0 ), d_valid( c, true ) {
-      }
-      virtual ~Region(){}
       //region node infomation
       std::map< Node, RegionNodeInfo* > d_nodes;
       //whether region is valid
       context::CDO< bool > d_valid;
+
     public:
+      //constructor
+      Region( SortModel* cf, context::Context* c );
+      virtual ~Region();
+
+      typedef std::map< Node, RegionNodeInfo* >::iterator iterator;
+      iterator begin() { return d_nodes.begin(); }
+      iterator end() { return d_nodes.end(); }
+
+      typedef NodeBoolMap::iterator split_iterator;
+      split_iterator begin_splits() { return d_splits.begin(); }
+      split_iterator end_splits() { return d_splits.end(); }
+
+      /** Returns a RegionInfo. */
+      RegionNodeInfo* getRegionInfo(Node n) {
+        Assert(d_nodes.find(n) != d_nodes.end());
+        return (* (d_nodes.find(n))).second;
+      }
+
+      /** Returns whether or not d_valid is set in current context. */
+      bool valid() const { return d_valid; }
+
+      /** Sets d_valid to the value valid in the current context.*/
+      void setValid(bool valid) { d_valid = valid; }
+
       /** add rep */
       void addRep( Node n );
       //take node from region
@@ -131,13 +185,14 @@ public:
       void setEqual( Node a, Node b );
       //set n1 != n2 to value 'valid', type is whether it is internal/external
       void setDisequal( Node n1, Node n2, int type, bool valid );
-    public:
       //get num reps
       int getNumReps() { return d_reps_size; }
       //get test clique size
       int getTestCliqueSize() { return d_testCliqueSize; }
       // has representative
-      bool hasRep( Node n ) { return d_nodes.find( n )!=d_nodes.end() && d_nodes[n]->d_valid; }
+      bool hasRep( Node n ) {
+        return d_nodes.find(n) != d_nodes.end() && d_nodes[n]->valid();
+      }
       // is disequal
       bool isDisequal( Node n1, Node n2, int type );
       /** get must merge */
@@ -145,15 +200,18 @@ public:
       /** has splits */
       bool hasSplits() { return d_splitsSize>0; }
       /** get external disequalities */
-      void getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities );
-    public:
+      void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
       /** check for cliques */
       bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
       /** get candidate clique */
       bool getCandidateClique( int cardinality, std::vector< Node >& clique );
       //print debug
       void debugPrint( const char* c, bool incClique = false );
-    };
+
+      // Returns the first key in d_nodes.
+      Node frontKey() const { return d_nodes.begin()->first; }
+    }; /* class Region */
+
   private:
     /** the type this model is for */
     TypeNode d_type;
@@ -173,16 +231,17 @@ public:
     std::vector< Node > d_disequalities;
     /** number of representatives in all regions */
     context::CDO< unsigned > d_reps;
-  private:
+
     /** get number of disequalities from node n to region ri */
     int getNumDisequalitiesToRegion( Node n, int ri );
     /** get number of disequalities from Region r to other regions */
     void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
     /** is valid */
-    bool isValid( int ri ) { return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->d_valid; }
+    bool isValid( int ri ) {
+      return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->valid();
+    }
     /** set split score */
     void setSplitScore( Node n, int s );
-  private:
     /** check if we need to combine region ri */
     void checkRegion( int ri, bool checkCombine = true );
     /** force combine region */
@@ -191,18 +250,21 @@ public:
     int combineRegions( int ai, int bi );
     /** move node n to region ri */
     void moveNode( Node n, int ri );
-  private:
     /** allocate cardinality */
     void allocateCardinality( OutputChannel* out );
-    /** add split 0 = no split, -1 = entailed disequality added, 1 = split added */
+    /**
+     * Add splits. Returns
+     *   0 = no split,
+     *  -1 = entailed disequality added, or
+     *   1 = split added.
+     */
     int addSplit( Region* r, OutputChannel* out );
     /** add clique lemma */
     void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
     /** add totality axiom */
     void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
-  private:
+
     class NodeTrie {
-      std::map< Node, NodeTrie > d_children;
     public:
       bool add( std::vector< Node >& n, unsigned i = 0 ){
         Assert( i<n.size() );
@@ -214,10 +276,13 @@ public:
           return d_children[n[i]].add( n, i+1 );
         }
       }
-    };
+    private:
+      std::map< Node, NodeTrie > d_children;
+    }; /* class NodeTrie */
+
     std::map< int, NodeTrie > d_clique_trie;
     void addClique( int c, std::vector< Node >& clique );
-  private:
+
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
     /** cardinality */
@@ -232,8 +297,6 @@ public:
     std::map< int, Node > d_cardinality_literal;
     /** cardinality lemmas */
     std::map< int, Node > d_cardinality_lemma;
-    /** cardinality assertions (indexed by cardinality literals ) */
-    NodeBoolMap d_cardinality_assertions;
     /** whether a positive cardinality constraint has been asserted */
     context::CDO< bool > d_hasCard;
     /** clique lemmas that have been asserted */
@@ -246,18 +309,20 @@ public:
     context::CDO< bool > d_initialized;
     /** cache for lemmas */
     NodeBoolMap d_lemma_cache;
-  private:
+
     /** apply totality */
     bool applyTotality( int cardinality );
     /** get totality lemma terms */
     Node getTotalityLemmaTerm( int cardinality, int i );
     /** simple check cardinality */
     void simpleCheckCardinality();
-  private:
+
     bool doSendLemma( Node lem );
+
   public:
-    SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
-    virtual ~SortModel(){}
+    SortModel( Node n, context::Context* c, context::UserContext* u,
+               StrongSolverTheoryUF* thss );
+    virtual ~SortModel();
     /** initialize */
     void initialize( OutputChannel* out );
     /** new node */
@@ -420,18 +485,7 @@ public:
   Statistics d_statistics;
 };/* class StrongSolverTheoryUF */
 
-class DisequalityPropagator
-{
-private:
-  /** quantifiers engine */
-  QuantifiersEngine* d_qe;
-  /** strong solver */
-  StrongSolverTheoryUF* d_ufss;
-  /** true,false */
-  Node d_true;
-  Node d_false;
-  /** check term t against equivalence class that t is disequal from */
-  void checkEquivalenceClass( Node t, Node eqc );
+class DisequalityPropagator {
 public:
   DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss);
   /** merge */
@@ -440,7 +494,7 @@ public:
   void assertDisequal( Node a, Node b, Node reason );
   /** assert predicate */
   void assertPredicate( Node p, bool polarity );
-public:
+
   class Statistics {
   public:
     IntStat d_propagations;
@@ -449,9 +503,20 @@ public:
   };
   /** statistics class */
   Statistics d_statistics;
-};
 
-}
+private:
+  /** quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** strong solver */
+  StrongSolverTheoryUF* d_ufss;
+  /** true,false */
+  Node d_true;
+  Node d_false;
+  /** check term t against equivalence class that t is disequal from */
+  void checkEquivalenceClass( Node t, Node eqc );
+}; /* class DisequalityPropagator */
+
+}/* CVC4::theory namespace::uf */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 05b95e9e1..ab42aaf15 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_uf_type_rules.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Andrew Reynolds, Morgan Deters
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add brief comments here ]]
  **