From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Apr 2011 23:32:16 +0000 (+0000)
Subject: more fixes/improvements to datatypes theory and transitive closure
X-Git-Tag: cvc5-1.0.0~8572
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40449557777db2d1170cb86274f83b431b5fef04;p=cvc5.git

more fixes/improvements to datatypes theory and transitive closure
---

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 9bfbaf12e..eea15d6b6 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -22,7 +22,6 @@
 #define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
 
 #include "theory/rewriter.h"
-#include "theory/datatypes/theory_datatypes.h"
 
 namespace CVC4 {
 namespace theory {
@@ -37,7 +36,7 @@ public:
 
     if(in.getKind() == kind::APPLY_TESTER) {
       if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
-        bool result = TheoryDatatypes::checkTrivialTester(in);
+        bool result = Datatype::indexOf(in.getOperator().toExpr()) == Datatype::indexOf(in[0].getOperator().toExpr());
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                    << "Rewrite trivial tester " << in
                                    << " " << result << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9bc195aed..88667de8d 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -25,6 +25,7 @@
 
 #include <map>
 
+//#define USE_TRANSITIVE_CLOSURE
 
 using namespace std;
 using namespace CVC4;
@@ -33,23 +34,31 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-bool TheoryDatatypes::isConstructorFinite( Node cons ){
+const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons )
+{
   Expr consExpr = cons.toExpr();
-  size_t consIndex = Datatype::indexOf(consExpr);
-  const Datatype& dt = Datatype::datatypeOf(consExpr);
-  const Datatype::Constructor& c = dt[consIndex];
-  Debug("datatypes-fin-check") << cons << " is ";
-  if( !c.isFinite() ){
-    Debug("datatypes-fin-check") << "not ";
+  return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ];
+}
+
+Node TheoryDatatypes::getConstructorForSelector( Node sel )
+{
+  size_t selIndex = Datatype::indexOf( sel.toExpr() );
+  const Datatype& dt = ((DatatypeType)((sel.getType()[0]).toType())).getDatatype();
+  for( unsigned i = 0; i<dt.getNumConstructors(); i++ ){
+    if( dt[i].getNumArgs()>selIndex && 
+        Node::fromExpr( dt[i][selIndex].getSelector() )==sel ){
+      return Node::fromExpr( dt[i].getConstructor() );
+    }
   }
-  Debug("datatypes-fin-check") << "finite." << std::endl;
-  return c.isFinite();
+  Assert( false );
+  return Node::null();
 }
 
+
 TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_DATATYPES, c, out, valuation),
-  //d_currAsserts(c),
-  //d_currEqualities(c),
+  d_currAsserts(c),
+  d_currEqualities(c),
   d_drv_map(c),
   d_axioms(c),
   d_selectors(c),
@@ -58,6 +67,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua
   d_equivalence_class(c),
   d_inst_map(c),
   d_cycle_check(c),
+  d_hasSeenCycle(c, false),
   d_labels(c),
   d_ccChannel(this),
   d_cc(c, &d_ccChannel),
@@ -65,42 +75,20 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua
   d_disequalities(c),
   d_equalities(c),
   d_conflict(),
-  d_noMerge(false) {
-
+  d_noMerge(false),
+  d_inCheck(false){
+
+  ////bug test for transitive closure
+  //TransitiveClosure tc( c );
+  //Debug("datatypes-tc") << "1 -> 0 : " << tc.addEdge( 1, 0 ) << std::endl;
+  //Debug("datatypes-tc") << "32 -> 1 : " << tc.addEdge( 32, 1 ) << std::endl;
+  //tc.debugPrintMatrix();
 }
 
 
 TheoryDatatypes::~TheoryDatatypes() {
 }
 
-
-void TheoryDatatypes::addDatatypeDefinitions(TypeNode dttn) {
-  AssertArgument(dttn.getKind() == DATATYPE_TYPE, dttn, "expected a datatype");
-
-  Debug("datatypes") << "TheoryDatatypes::addDataTypeDefinitions(): "
-                     << dttn.getConst<Datatype>().getName() << endl;
-  if(d_addedDatatypes.find(dttn) != d_addedDatatypes.end()) {
-    // already have incorporated this datatype definition
-    Debug("datatypes") << "+ can skip" << endl;
-    return;
-  }
-
-  const Datatype& dt = dttn.getConst<Datatype>();
-  Debug("datatypes") << dt << endl;
-  for(Datatype::const_iterator it = dt.begin(); it != dt.end(); ++it) {
-    Node constructor = Node::fromExpr((*it).getConstructor());
-    d_cons[dttn].push_back(constructor);
-    d_testers[dttn].push_back(Node::fromExpr((*it).getTester()));
-    for(Datatype::Constructor::const_iterator itc = (*it).begin(); itc != (*it).end(); ++itc) {
-      Node selector = Node::fromExpr((*itc).getSelector());
-      d_sels[constructor].push_back(selector);
-      d_sel_cons[selector] = constructor;
-    }
-  }
-  d_addedDatatypes.insert(dttn);
-}
-
-
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
                      << t << endl;
@@ -129,6 +117,10 @@ void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
   Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl;
 }
 
+void TheoryDatatypes::preRegisterTerm(TNode n) {  
+  Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+}
+
 
 void TheoryDatatypes::presolve() {
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
@@ -136,99 +128,92 @@ void TheoryDatatypes::presolve() {
 
 void TheoryDatatypes::check(Effort e) {
 
-  //for( int i=0; i<(int)d_currAsserts.size(); i++ ) {
-  //  Debug("datatypes") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl;
-  //}
-  //for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
-  //  Debug("datatypes") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
-  //}
-  //for( BoolMap::iterator i = d_inst_map.begin(); i != d_inst_map.end(); i++ ) {
-  //  Debug("datatypes") << "inst_map = " << (*i).first << endl;
-  //}
-  //for( EqListsN::iterator i = d_selector_eq.begin(); i != d_selector_eq.end(); i++ ) {
-  //  EqListN* m = (*i).second;
-  //  Debug("datatypes") << "selector_eq " << (*i).first << ":" << endl;
-  //  for( EqListN::const_iterator j = m->begin(); j != m->end(); j++ ) {
-  //    Debug("datatypes") << "  : " << (*j) << endl;
-  //  }
-  //}
+  for( int i=0; i<(int)d_currAsserts.size(); i++ ) {
+    Debug("datatypes") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl;
+  }
+  for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
+    Debug("datatypes") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
+  }
 
   while(!done()) {
     Node assertion = get();
-    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
+    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) {
       cout << "*** TheoryDatatypes::check(): " << assertion << endl;
+      d_currAsserts.push_back( assertion );
     }
-    //d_currAsserts.push_back( assertion );
 
     //clear from the derived map
-    if( !d_drv_map[assertion].get().isNull() ) {
-      Debug("datatypes") << "Assertion has already been derived" << endl;
-      d_drv_map[assertion] = Node::null();
-    } else {
-      collectTerms( assertion );
-      switch(assertion.getKind()) {
-      case kind::EQUAL:
-      case kind::IFF:
-        addEquality(assertion);
-        break;
-      case kind::APPLY_TESTER:
-        checkTester( assertion );
-        break;
-      case kind::NOT:
-        {
-          switch( assertion[0].getKind()) {
-          case kind::EQUAL:
-          case kind::IFF:
-            {
-              Node a = assertion[0][0];
-              Node b = assertion[0][1];
-              addDisequality(assertion[0]);
-              d_cc.addTerm(a);
-              d_cc.addTerm(b);
-              if(Debug.isOn("datatypes")) {
-                Debug("datatypes") << "       a  == > " << a << endl
-                            << "       b  == > " << b << endl
-                            << "  find(a) == > " << debugFind(a) << endl
-                            << "  find(b) == > " << debugFind(b) << endl;
-              }
-              // There are two ways to get a conflict here.
-              if(d_conflict.isNull()) {
-                if(find(a) == find(b)) {
-                  // We get a conflict this way if we WERE previously watching
-                  // a, b and were notified previously (via notifyCongruent())
-                  // that they were congruent.
-                  NodeBuilder<> nb(kind::AND);
-                  nb << d_cc.explain( assertion[0][0], assertion[0][1] );
-                  nb << assertion;
-                  d_conflict = nb;
-                  Debug("datatypes") << "Disequality conflict " << d_conflict << endl;
-                } else {
-
-                  // If we get this far, there should be nothing conflicting due
-                  // to this disequality.
-                  Assert(!d_cc.areCongruent(a, b));
+    d_inCheck = true;
+    collectTerms( assertion );
+    if( d_conflict.isNull() ){
+      if( !d_drv_map[assertion].get().isNull() ) {
+        Debug("datatypes") << "Assertion has already been derived" << endl;
+        d_drv_map[assertion] = Node::null();
+      } else {
+        switch(assertion.getKind()) {
+        case kind::EQUAL:
+        case kind::IFF:
+          addEquality(assertion);
+          break;
+        case kind::APPLY_TESTER:
+          checkTester( assertion );
+          break;
+        case kind::NOT:
+          {
+            switch( assertion[0].getKind()) {
+            case kind::EQUAL:
+            case kind::IFF:
+              {
+                Node a = assertion[0][0];
+                Node b = assertion[0][1];
+                addDisequality(assertion[0]);
+                d_cc.addTerm(a);
+                d_cc.addTerm(b);
+                if(Debug.isOn("datatypes")) {
+                  Debug("datatypes") << "       a  == > " << a << endl
+                              << "       b  == > " << b << endl
+                              << "  find(a) == > " << debugFind(a) << endl
+                              << "  find(b) == > " << debugFind(b) << endl;
+                }
+                // There are two ways to get a conflict here.
+                if(d_conflict.isNull()) {
+                  if(find(a) == find(b)) {
+                    // We get a conflict this way if we WERE previously watching
+                    // a, b and were notified previously (via notifyCongruent())
+                    // that they were congruent.
+                    NodeBuilder<> nb(kind::AND);
+                    nb << d_cc.explain( assertion[0][0], assertion[0][1] );
+                    nb << assertion;
+                    d_conflict = nb;
+                    Debug("datatypes") << "Disequality conflict " << d_conflict << endl;
+                  } else {
+                    // If we get this far, there should be nothing conflicting due
+                    // to this disequality.
+                    Assert(!d_cc.areCongruent(a, b));
+                  }
                 }
               }
+              break;
+            case kind::APPLY_TESTER:
+              checkTester( assertion );
+              break;
+            default:
+              Unhandled(assertion[0].getKind());
+              break;
             }
-            break;
-          case kind::APPLY_TESTER:
-            checkTester( assertion );
-            break;
-          default:
-            Unhandled(assertion[0].getKind());
-            break;
           }
+          break;
+        default:
+          Unhandled(assertion.getKind());
+          break;
         }
-        break;
-      default:
-        Unhandled(assertion.getKind());
-        break;
-      }
-      if(!d_conflict.isNull()) {
-        throwConflict();
-        return;
       }
     }
+    d_inCheck = false;
+    if(!d_conflict.isNull()) {
+      throwConflict();
+      return;
+    }
   }
 
   if( e == FULL_EFFORT ) {
@@ -237,20 +222,14 @@ void TheoryDatatypes::check(Effort e) {
     for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
       Node sf = find( (*i).first );
       if( sf == (*i).first || sf.getKind() != APPLY_CONSTRUCTOR ) {
-        Debug("datatypes-split") << "Check for splitting " << (*i).first << ", ";
         EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second;
-        if( lbl->empty() ) {
-          Debug("datatypes-split") << "empty label" << endl;
-        } else {
-          Debug("datatypes-split") << "label size = " << lbl->size() << endl;
-        }
+        Debug("datatypes-split") << "Check for splitting " << (*i).first << ", ";
+        Debug("datatypes-split") << "label size = " << lbl->size() << endl;
         Node cons = getPossibleCons( (*i).first, false );
         if( !cons.isNull() ) {
+          const Datatype::Constructor& cn = getConstructor( cons );
           Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
-          TypeNode typ = (*i).first.getType();
-          int cIndex = Datatype::indexOf( cons.toExpr() );
-          Assert( cIndex != -1 );
-          Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], (*i).first );
+          Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
           NodeBuilder<> nb(kind::OR);
           nb << test << test.notNode();
           Node lemma = nb;
@@ -272,6 +251,7 @@ void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) {
   Debug("datatypes") << "Check tester " << assertion << endl;
 
   Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion;
+  const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() );
 
   //add the term into congruence closure consideration
   d_cc.addTerm( tassertion[0] );
@@ -317,7 +297,7 @@ void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) {
 
   //check if empty label (no possible constructors for term)
   bool add = true;
-  int notCount = 0;
+  unsigned int notCount = 0;
   if( !lbl->empty() ) {
     for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
       Node leqn = (*i);
@@ -351,8 +331,7 @@ void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) {
     }
   }
   if( add ) {
-    //Assert( (int)d_cons[ tRep.getType() ].size()== Datatype::datatypeOf(tassertion.getOperator).getNumConstructors() );
-    if( assertionRep.getKind() == NOT && notCount == (int)d_cons[ tRep.getType() ].size()-1 ) {
+    if( assertionRep.getKind() == NOT && notCount == dt.getNumConstructors()-1 ) {
       NodeBuilder<> nb(kind::AND);
       if( !lbl->empty() ) {
         for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
@@ -409,20 +388,16 @@ void TheoryDatatypes::checkInstantiate( Node t ) {
         //there is one remaining constructor
         if( !cons.isNull() && lbl_i != d_labels.end() ) {
           EqList* lbl = (*lbl_i).second;
+          const Datatype::Constructor& cn = Datatype::datatypeOf( cons.toExpr() )[ Datatype::indexOf( cons.toExpr() ) ];
+
           //only one constructor possible for term (label is singleton), apply instantiation rule
-          bool consFinite = isConstructorFinite( cons );
-          Debug("datatypes-fin-check") << "checkInst: " << cons << " is ";
-          if( !consFinite ){
-            Debug("datatypes-fin-check") << "not ";
-          }
-          Debug("datatypes-fin-check") << "finite. " << std::endl;
           //find if selectors have been applied to t
           vector< Node > selectorVals;
           selectorVals.push_back( cons );
           NodeBuilder<> justifyEq(kind::AND);
           bool foundSel = false;
-          for( int i=0; i<(int)d_sels[cons].size(); i++ ) {
-            Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], te );
+          for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
+            Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
             Debug("datatypes") << "Selector[" << i << "] = " << s << endl;
             if( d_selectors.find( s ) != d_selectors.end() ) {
               Node sf = find( s );
@@ -434,7 +409,7 @@ void TheoryDatatypes::checkInstantiate( Node t ) {
             }
             selectorVals.push_back( s );
           }
-          if( consFinite || foundSel ) {
+          if( cn.isFinite() || foundSel ) {
             d_inst_map[ te ] = true;
             //instantiate, add equality
             Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
@@ -450,13 +425,9 @@ void TheoryDatatypes::checkInstantiate( Node t ) {
                   }
                 }
               }
-              Node jeq;
-              if( justifyEq.getNumChildren() == 1 ) {
-                jeq = justifyEq.getChild( 0 );
-              } else {
-                jeq = justifyEq;
-              }
+              Node jeq = ( justifyEq.getNumChildren() == 1 ) ? justifyEq.getChild( 0 ) : justifyEq;
               Debug("datatypes-split") << "Instantiate " << newEq << endl;
+              preRegisterTerm( val );
               addDerivedEquality( newEq, jeq );
               return;
             }
@@ -477,15 +448,18 @@ Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) {
     EqList* lbl = (*lbl_i).second;
     TypeNode typ = t.getType();
 
+    const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype();
+
     //if ended by one positive tester
     if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
       if( checkInst ) {
-        return d_cons[typ][ Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() ) ];
+        size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() );
+        return Node::fromExpr( dt[ testerIndex ].getConstructor() );
       }
     //if (n-1) negative testers
-    } else if( !checkInst || (int)lbl->size() == (int)d_cons[ t.getType() ].size()-1 ) {
+    } else if( !checkInst || lbl->size() == dt.getNumConstructors()-1 ) {
       vector< bool > possibleCons;
-      possibleCons.resize( (int)d_cons[ t.getType() ].size(), true );
+      possibleCons.resize( dt.getNumConstructors(), true );
       if( !lbl->empty() ) {
         for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
           TNode leqn = (*i);
@@ -493,13 +467,13 @@ Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) {
         }
       }
       Node cons = Node::null();
-      for( int i=0; i<(int)possibleCons.size(); i++ ) {
+      for( unsigned int i=0; i<possibleCons.size(); i++ ) {
         if( possibleCons[i] ) {
-          cons = d_cons[typ][ i ];
+          cons = Node::fromExpr( dt[ i ].getConstructor() );
           if( !checkInst ) {
             //if there is a selector, split
-            for( int i=0; i<(int)d_sels[cons].size(); i++ ) {
-              Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], tf );
+            for( unsigned int j=0; j<dt[ i ].getNumArgs(); j++ ) {
+              Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[i][j].getSelector() ), tf );
               if( d_selectors.find( s ) != d_selectors.end() ) {
                 Debug("datatypes") << "  getPosCons: found selector " << s << endl;
                 return cons;
@@ -510,9 +484,9 @@ Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) {
       }
       if( !checkInst ) {
         for( int i=0; i<(int)possibleCons.size(); i++ ) {
-          if( possibleCons[i] && !isConstructorFinite( d_cons[typ][ i ] ) ) {
+          if( possibleCons[i] && !dt[ i ].isFinite() ) {
             Debug("datatypes") << "Did not find selector for " << tf;
-            Debug("datatypes") << " and " << d_cons[typ][ i ] << " is not finite." << endl;
+            Debug("datatypes") << " and " << dt[ i ].getConstructor() << " is not finite." << endl;
             return Node::null();
           }
         }
@@ -544,12 +518,17 @@ Node TheoryDatatypes::getValue(TNode n) {
 
 void TheoryDatatypes::merge(TNode a, TNode b) {
   if( d_noMerge ) {
-    Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl;
+    //Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl;
     d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) );
     return;
   }
   Assert(d_conflict.isNull());
-  Debug("datatypes") << "Merge "<< a << " " << b << endl;
+  a = find(a);
+  b = find(b);
+  if( a == b) {
+    return;
+  }
+  Debug("datatypes-cycles") << "Merge "<< a << " " << b << endl;
 
   // make "a" the one with shorter diseqList
   EqLists::iterator deq_ia = d_disequalities.find(a);
@@ -564,14 +543,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
     }
   }
 
-  a = find(a);
-  b = find(b);
-
-  //Debug("datatypes") << "After find: "<< a << " " << b << endl;
-
-  if( a == b) {
-    return;
-  }
   //if b is a selector, swap a and b
   if( b.getKind() == APPLY_SELECTOR && a.getKind() != APPLY_SELECTOR ) {
     TNode tmp = a;
@@ -591,23 +562,28 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
     b = tmp;
   }
 
-
+  //check for clash
   NodeBuilder<> explanation(kind::AND);
-  if( checkClash( a, b, explanation ) ) {
+  if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR 
+      && a.getOperator()!=b.getOperator() ){
     explanation << d_cc.explain( a, b );
     d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
     Debug("datatypes") << "Clash " << a << " " << b << endl;
     Debug("datatypes") << "Conflict is " << d_conflict << endl;
-    return;
+    return; 
   }
   Debug("datatypes-debug") << "Done clash" << endl;
 
   Debug("datatypes") << "Set canon: "<< a << " " << b << endl;
-
   // b becomes the canon of a
   d_unionFind.setCanon(a, b);
   d_reps[a] = false;
   d_reps[b] = true;
+#ifdef USE_TRANSITIVE_CLOSURE
+  bool result = d_cycle_check.addEdgeNode( a, b );
+  d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+#endif
+
   //merge equivalence classes
   initializeEqClass( a );
   initializeEqClass( b );
@@ -617,8 +593,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
     eqc_b->push_back( *i );
   }
 
- //Debug("datatypes") << "After check 1" << endl;
-
   deq_ia = d_disequalities.find(a);
   map<TNode, TNode> alreadyDiseqs;
   if(deq_ia != d_disequalities.end()) {
@@ -689,17 +663,37 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   }
 
   //Debug("datatypes-debug") << "Done clash" << endl;
-  //if( d_cycle_check.addEdgeNode( a, b ) ){
+#ifdef USE_TRANSITIVE_CLOSURE
+  Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl;
+  if( d_hasSeenCycle.get() ){
+    checkCycles();
+    if( !d_conflict.isNull() ){
+      return;
+    }
+  }else{
+    checkCycles();
+    if( !d_conflict.isNull() ){
+      Debug("datatypes-cycles") << "Cycle is " << d_conflict << std::endl;
+      for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
+        Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
+      }
+      d_cycle_check.debugPrint();
+      Assert( false );
+    }
+  }
+#else
   checkCycles();
-  //Assert( !d_conflict.isNull() );
-  if( !d_conflict.isNull() ) {
+  if( !d_conflict.isNull() ){
     return;
   }
-  //}
+#endif
   Debug("datatypes-debug") << "Done cycles" << endl;
 
   //merge selector lists
   updateSelectors( a );
+  if( !d_conflict.isNull() ){
+    return;
+  }
   Debug("datatypes-debug") << "Done collapse" << endl;
 
   //merge labels
@@ -718,18 +712,15 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   Debug("datatypes-debug") << "Done merge labels" << endl;
 
   //do unification
-  if( d_conflict.isNull() ) {
-    if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR &&
-        a.getOperator() == b.getOperator() ) {
-      Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl;
-      for( int i=0; i<(int)a.getNumChildren(); i++ ) {
-        if( find( a[i] ) != find( b[i] ) ) {
-          Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] );
-          Node jEq = d_cc.explain(a, b);
-          Debug("datatypes-drv") << "UEqual: " << newEq << ", justification: " << jEq << " from " << a << " " << b << endl;
-          Debug("datatypes-drv") << "UEqual find: " << find( a[i] ) << " " << find( b[i] ) << endl;
-          addDerivedEquality( newEq, jEq );
-        }
+  Assert( d_conflict.isNull() );
+  if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR &&
+      a.getOperator() == b.getOperator() ) {
+    Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl;
+    for( int i=0; i<(int)a.getNumChildren(); i++ ) {
+      if( find( a[i] ) != find( b[i] ) ) {
+        Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] );
+        Node jEq = d_cc.explain(a, b);
+        addDerivedEquality( newEq, jEq );
       }
     }
   }
@@ -743,19 +734,13 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
     TypeNode typ = t[0].getType();
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
-    Node cons = d_sel_cons[sel];
+    Node cons = getConstructorForSelector( sel );
+    const Datatype::Constructor& cn = getConstructor( cons );
     Node tmp = find( t[0] );
     Node retNode = t;
     if( tmp.getKind() == APPLY_CONSTRUCTOR ) {
       if( tmp.getOperator() == cons ) {
-        int selIndex = -1;
-        for(int i=0; i<(int)d_sels[cons].size(); i++ ) {
-          if( d_sels[cons][i] == sel ) {
-            selIndex = i;
-            break;
-          }
-        }
-        Assert( selIndex != -1 );
+        size_t selIndex = Datatype::indexOf( sel.toExpr() );
         Debug("datatypes") << "Applied selector " << t << " to correct constructor, index = " << selIndex << endl;
         Debug("datatypes") << "Return " << tmp[selIndex] << endl;
         retNode = tmp[selIndex];
@@ -773,10 +758,8 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
       }
     } else {
       if( useContext ) {
-        int cIndex = Datatype::indexOf( cons.toExpr() );
-        Assert( cIndex != -1 );
         //check labels
-        Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], tmp );
+        Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp );
         checkTester( tester, false );
         if( !d_conflict.isNull() ) {
           Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
@@ -853,39 +836,68 @@ void TheoryDatatypes::updateSelectors( Node a ) {
   }
 }
 
-void TheoryDatatypes::collectTerms( TNode t ) {
-  for( int i=0; i<(int)t.getNumChildren(); i++ ) {
-    collectTerms( t[i] );
-#if 0
-    if( t.getKind() == APPLY_CONSTRUCTOR ){
-      if( d_cycle_check.addEdgeNode( t, t[i] ) ){
-        checkCycles();
-        //Assert( !d_conflict.isNull() );
-        if( !d_conflict.isNull() ){
-          return;
-        }
+void TheoryDatatypes::addTermToLabels( Node t ) {
+  if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) {
+    Node tmp = find( t );
+    if( tmp == t ) {
+      //add to labels
+      EqLists::iterator lbl_i = d_labels.find(t);
+      if(lbl_i == d_labels.end()) {
+        EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false,
+                                                ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+        d_labels.insertDataFromContextMemory(tmp, lbl);
       }
     }
+  }
+}
+
+void TheoryDatatypes::initializeEqClass( Node t ) {
+  EqListsN::iterator eqc_i = d_equivalence_class.find( t );
+  if( eqc_i == d_equivalence_class.end() ) {
+    EqListN* eqc = new(getContext()->getCMM()) EqListN(true, getContext(), false,
+                                          ContextMemoryAllocator<Node>(getContext()->getCMM()));
+    eqc->push_back( t );
+    d_equivalence_class.insertDataFromContextMemory(t, eqc);
+  }
+}
+
+void TheoryDatatypes::collectTerms( Node n ) {
+  for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+    collectTerms( n[i] );
+  }
+  if( n.getKind() == APPLY_CONSTRUCTOR ){
+#ifdef USE_TRANSITIVE_CLOSURE
+    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+      Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl;
+      bool result = d_cycle_check.addEdgeNode( n, n[i] );
+      //if( result ){
+      //  for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
+      //    Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
+      //  }
+      //  d_cycle_check.debugPrint();
+      //}
+      Assert( !result );    //this should not create any new cycles (relevant terms should have been recorded before)
+    }
 #endif
   }
-  if( t.getKind() == APPLY_SELECTOR ) {
-    if( d_selectors.find( t ) == d_selectors.end() ) {
-      Debug("datatypes-split") << "  Found selector " << t << endl;
-      d_selectors[ t ] = true;
-      d_cc.addTerm( t );
-      Node tmp = find( t[0] );
+  if( n.getKind() == APPLY_SELECTOR ) {
+    if( d_selectors.find( n ) == d_selectors.end() ) {
+      Debug("datatypes-split") << "  Found selector " << n << endl;
+      d_selectors[ n ] = true;
+      d_cc.addTerm( n );
+      Node tmp = find( n[0] );
       checkInstantiate( tmp );
 
-      Node s = t;
-      if( tmp != t[0] ) {
-        s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
+      Node s = n;
+      if( tmp != n[0] ) {
+        s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp );
       }
       Debug("datatypes-split") << "  Before collapse: " << s << endl;
       s = collapseSelector( s, true );
       Debug("datatypes-split") << "  After collapse: " << s << endl;
       if( s.getKind() == APPLY_SELECTOR ) {
         //add selector to selector eq list
-        Debug("datatypes") << "  Add selector to list " << tmp << " " << t << endl;
+        Debug("datatypes") << "  Add selector to list " << tmp << " " << n << endl;
         EqListsN::iterator sel_i = d_selector_eq.find( tmp );
         EqListN* sel;
         if( sel_i == d_selector_eq.end() ) {
@@ -901,32 +913,7 @@ void TheoryDatatypes::collectTerms( TNode t ) {
       }
     }
   }
-  addTermToLabels( t );
-}
-
-void TheoryDatatypes::addTermToLabels( Node t ) {
-  if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) {
-    Node tmp = find( t );
-    if( tmp == t ) {
-      //add to labels
-      EqLists::iterator lbl_i = d_labels.find(t);
-      if(lbl_i == d_labels.end()) {
-        EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false,
-                                                ContextMemoryAllocator<TNode>(getContext()->getCMM()));
-        d_labels.insertDataFromContextMemory(tmp, lbl);
-      }
-    }
-  }
-}
-
-void TheoryDatatypes::initializeEqClass( Node t ) {
-  EqListsN::iterator eqc_i = d_equivalence_class.find( t );
-  if( eqc_i == d_equivalence_class.end() ) {
-    EqListN* eqc = new(getContext()->getCMM()) EqListN(true, getContext(), false,
-                                          ContextMemoryAllocator<Node>(getContext()->getCMM()));
-    eqc->push_back( t );
-    d_equivalence_class.insertDataFromContextMemory(t, eqc);
-  }
+  addTermToLabels( n );
 }
 
 void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) {
@@ -950,27 +937,6 @@ void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) {
   //}
 }
 
-void TheoryDatatypes::appendToEqList(TNode of, TNode eq) {
-  Debug("datatypes") << "appending " << eq << endl
-              << "  to eq list of " << of << endl;
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-  Assert(of == debugFind(of));
-  EqLists::iterator eq_i = d_equalities.find(of);
-  EqList* eql;
-  if(eq_i == d_equalities.end()) {
-    eql = new(getContext()->getCMM()) EqList(true, getContext(), false,
-                                             ContextMemoryAllocator<TNode>(getContext()->getCMM()));
-    d_equalities.insertDataFromContextMemory(of, eql);
-  } else {
-    eql = (*eq_i).second;
-  }
-  eql->push_back(eq);
-  //if(Debug.isOn("uf")) {
-  //  Debug("uf") << "  size is now " << eql->size() << endl;
-  //}
-}
-
 void TheoryDatatypes::addDerivedEquality(TNode eq, TNode jeq) {
   Debug("datatypes-drv") << "Justification for " << eq << "is: " << jeq << "." << endl;
   d_drv_map[eq] = jeq;
@@ -982,21 +948,32 @@ void TheoryDatatypes::addEquality(TNode eq) {
          eq.getKind() == kind::IFF);
   if( eq[0] != eq[1] ) {
     Debug("datatypes") << "Add equality " << eq << "." << endl;
+
+    //setup merge pending list
     d_merge_pending.push_back( vector< pair< Node, Node > >() );
     bool prevNoMerge = d_noMerge;
     d_noMerge = true;
+
     d_cc.addTerm(eq[0]);
     d_cc.addTerm(eq[1]);
     d_cc.addEquality(eq);
-    //d_currEqualities.push_back(eq);
+    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-cycles") ){
+      d_currEqualities.push_back(eq);
+    }
+
+    //record which nodes are waiting to be merged
     d_noMerge = prevNoMerge;
-    unsigned int mpi = d_merge_pending.size()-1;
     vector< pair< Node, Node > > mp;
-    mp.insert( mp.begin(), d_merge_pending[mpi].begin(), d_merge_pending[mpi].end() );
+    mp.insert( mp.begin(), 
+               d_merge_pending[d_merge_pending.size()-1].begin(), 
+               d_merge_pending[d_merge_pending.size()-1].end() );
     d_merge_pending.pop_back();
+
+    //merge original nodes
     if( d_conflict.isNull() ) {
       merge(eq[0], eq[1]);
     }
+    //merge nodes waiting to be merged
     for( int i=0; i<(int)mp.size(); i++ ) {
       if( d_conflict.isNull() ) {
         merge( mp[i].first, mp[i].second );
@@ -1016,40 +993,16 @@ void TheoryDatatypes::addDisequality(TNode eq) {
   appendToDiseqList(find(b), eq);
 }
 
-void TheoryDatatypes::registerEqualityForPropagation(TNode eq) {
-  // should NOT be in search at this point, this must be called during
-  // preregistration
-
-  // FIXME with lemmas on demand, this could miss future propagations,
-  // since we are not necessarily at context level 0, but are updating
-  // context-sensitive structures.
-
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-
-  TNode a = eq[0];
-  TNode b = eq[1];
-
-  appendToEqList(find(a), eq);
-  appendToEqList(find(b), eq);
-}
-
 void TheoryDatatypes::throwConflict() {
   Debug("datatypes") << "Convert conflict : " << d_conflict << endl;
   NodeBuilder<> nb(kind::AND);
   convertDerived( d_conflict, nb );
-  if( nb.getNumChildren() == 1 ) {
-    d_conflict = nb.getChild( 0 );
-  } else {
-    d_conflict = nb;
-  }
-  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
+  d_conflict = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
+  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) {
     cout << "Conflict constructed : " << d_conflict << endl;
   }
-  //if( d_conflict.getKind() != kind::AND ) {
-  //  NodeBuilder<> nb(kind::AND);
-  //  nb << d_conflict << d_conflict;
-  //  d_conflict = nb;
+  //if( d_conflict.getKind()!=kind::AND ){
+  //  d_conflict = NodeManager::currentNM()->mkNode(kind::AND, d_conflict, d_conflict);
   //}
   d_out->conflict( d_conflict, false );
   d_conflict = Node::null();
@@ -1095,8 +1048,23 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
       if( visited.find( nn ) == visited.end() ) {
         visited[nn] = true;
         if( nn == on || searchForCycle( nn, on, visited, explanation ) ) {
+          if( !d_cycle_check.isConnectedNode( n, n[i] ) ){
+            Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << n[i] << "!!!!" << std::endl;
+          }
           if( nn != n[i] ) {
-            explanation << d_cc.explain( nn, n[i] );
+            Node e = d_cc.explain( nn, n[i] );
+            if( !d_cycle_check.isConnectedNode( n[i], nn ) ){
+              Debug("datatypes-cycles") << "Cycle equality: " << n[i] << " is not -> " << nn << "!!!!" << std::endl;
+              Debug("datatypes-cycles") << "Explanation: " << e << std::endl;
+              if( e.getKind()==kind::AND ){
+                for( int a=0; a<e.getNumChildren(); a++ ){
+                  Debug("datatypes-cycles") << e[a][0] << " " << e[a][1] << " "
+                    << d_cycle_check.isConnectedNode( e[a][1], e[a][0] ) << " "
+                    << d_cycle_check.isConnectedNode( e[a][0], e[a][1] ) << std::endl;
+                }
+              }
+            }
+            explanation << e;
           }
           return true;
         }
@@ -1105,35 +1073,3 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
   }
   return false;
 }
-
-//should be called initially with explanation of why n1 and n2 are equal
-bool TheoryDatatypes::checkClash( Node n1, Node n2, NodeBuilder<>& explanation ) {
-  //Debug("datatypes") << "Check clash " << n1 << " " << n2 << endl;
-  Node n1f = find( n1 );
-  Node n2f = find( n2 );
-  bool retVal = false;
-  if( n1f != n2f ) {
-    if( n1f.getKind() == kind::APPLY_CONSTRUCTOR && n2f.getKind() == kind::APPLY_CONSTRUCTOR ) {
-      if( n1f.getOperator() != n2f.getOperator() ) {
-        retVal =true;
-      } else {
-        Assert( n1f.getNumChildren() == n2f.getNumChildren() );
-        for( int i=0; i<(int)n1f.getNumChildren(); i++ ) {
-          if( checkClash( n1f[i], n2f[i], explanation ) ) {
-            retVal = true;
-            break;
-          }
-        }
-      }
-    }
-    if( retVal ) {
-      if( n1f != n1 ) {
-        explanation << d_cc.explain( n1f, n1 );
-      }
-      if( n2f != n2 ) {
-        explanation << d_cc.explain( n2f, n2 );
-      }
-    }
-  }
-  return retVal;
-}
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index d6fc837fd..1a944a6e0 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -44,20 +44,9 @@ private:
   typedef context::CDMap<Node, EqListN*, NodeHashFunction> EqListsN;
   typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap;
 
-  std::hash_set<TypeNode, TypeNodeHashFunction> d_addedDatatypes;
-
-  //context::CDList<Node> d_currAsserts;
-  //context::CDList<Node> d_currEqualities;
-
-  //TODO: the following 4 maps can be eliminated
-  /** a list of types with the list of constructors for that type */
-  std::map<TypeNode, std::vector<Node> > d_cons;
-  /** a list of types with the list of constructors for that type */
-  std::map<TypeNode, std::vector<Node> > d_testers;
-  /** a list of constructors with the list of selectors */
-  std::map<Node, std::vector<Node> > d_sels;
-  /** map from selectors to the constructors they are for */
-  std::map<Node, Node > d_sel_cons;
+  /** for debugging */
+  context::CDList<Node> d_currAsserts;
+  context::CDList<Node> d_currEqualities;
 
   /** map from equalties and the equalities they are derived from */
   context::CDMap< Node, Node, NodeHashFunction > d_drv_map;
@@ -75,8 +64,12 @@ private:
   BoolMap d_inst_map;
   /** transitive closure to record equivalence/subterm relation.  */
   TransitiveClosureNode d_cycle_check;
-  /** check whether constructor is finite */
-  bool isConstructorFinite( Node cons );
+  /** has seen cycle */
+  context::CDO< bool > d_hasSeenCycle;
+  /** get the constructor for the node */
+  const Datatype::Constructor& getConstructor( Node cons );
+  /** get the constructor for the selector */
+  Node getConstructorForSelector( Node sel );
 
   /**
    * map from terms to testers asserted for that term
@@ -140,15 +133,11 @@ private:
    */
   bool d_noMerge;
   std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending;
+  bool d_inCheck;
 public:
   TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation);
   ~TheoryDatatypes();
-  void preRegisterTerm(TNode n) {
-    TypeNode type = n.getType();
-    if(type.getKind() == kind::DATATYPE_TYPE) {
-      addDatatypeDefinitions(type);
-    }
-  }
+  void preRegisterTerm(TNode n);
   void presolve();
 
   void addSharedTerm(TNode t);
@@ -158,30 +147,26 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryDatatypes"); }
 
-  void addDatatypeDefinitions(TypeNode dttn);
-
 private:
   /* Helper methods */
   void checkTester( Node assertion, bool doAdd = true );
-  static bool checkTrivialTester(Node assertion);
+  bool checkTrivialTester(Node assertion);
   void checkInstantiate( Node t );
   Node getPossibleCons( Node t, bool checkInst = false );
   Node collapseSelector( TNode t, bool useContext = false );
   void updateSelectors( Node a );
-  void collectTerms( TNode t );
   void addTermToLabels( Node t );
   void initializeEqClass( Node t );
+  void collectTerms( Node n );
 
   /* from uf_morgan */
   void merge(TNode a, TNode b);
   inline TNode find(TNode a);
   inline TNode debugFind(TNode a) const;
   void appendToDiseqList(TNode of, TNode eq);
-  void appendToEqList(TNode of, TNode eq);
   void addDisequality(TNode eq);
   void addDerivedEquality(TNode eq, TNode jeq);
   void addEquality(TNode eq);
-  void registerEqualityForPropagation(TNode eq);
 
   void convertDerived(Node n, NodeBuilder<>& nb);
   void throwConflict();
@@ -189,8 +174,6 @@ private:
   bool searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        NodeBuilder<>& explanation );
-  bool checkClash( Node n1, Node n2, NodeBuilder<>& explanation );
-  friend class DatatypesRewriter;// for access to checkTrivialTester();
 };/* class TheoryDatatypes */
 
 inline TNode TheoryDatatypes::find(TNode a) {
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 20d63995f..2a3f69fd6 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -399,6 +399,10 @@ void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
   d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self));
   d_name.resize(d_name.find('\0'));
   d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self));
+  //associate constructor with all selectors
+  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    (*i).d_constructor = d_constructor;
+  }
 }
 
 Datatype::Constructor::Constructor(std::string name, std::string tester) :
@@ -605,6 +609,12 @@ Expr Datatype::Constructor::Arg::getSelector() const {
   return d_selector;
 }
 
+Expr Datatype::Constructor::Arg::getConstructor() const {
+  CheckArgument(isResolved(), this, 
+                "cannot get a associated constructor for argument of an unresolved datatype constructor");
+  return d_constructor;
+}
+
 bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() {
   return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index df7dd1814..75da1405f 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -147,6 +147,8 @@ public:
 
       std::string d_name;
       Expr d_selector;
+      /** the constructor associated with this selector */
+      Expr d_constructor;
       bool d_resolved;
 
       explicit Arg(std::string name, Expr selector);
@@ -166,6 +168,12 @@ public:
        */
       Expr getSelector() const;
 
+      /**
+       * Get the associated constructor for this constructor argument; this call is
+       * only permitted after resolution.
+       */
+      Expr getConstructor() const;
+
       /**
        * Get the name of the type of this constructor argument
        * (Datatype field).  Can be used for not-yet-resolved Datatypes
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index a31dc3378..43c8735ad 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -74,6 +74,14 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j)
   return false;
 }
 
+bool TransitiveClosure::isConnected(unsigned i, unsigned j)
+{
+  if( i>=adjMatrix.size() || j>adjMatrix.size() ){
+    return false;
+  }else{
+    return adjMatrix[i] != NULL && adjMatrix[i]->read(j);
+  }
+}
 
 void TransitiveClosure::debugPrintMatrix()
 {
@@ -89,16 +97,24 @@ void TransitiveClosure::debugPrintMatrix()
   }      
 }
 
-unsigned TransitiveClosureNode::d_counter = 0;
-
 unsigned TransitiveClosureNode::getId( Node i ){
-  std::map< Node, unsigned >::iterator it = nodeMap.find( i );
+  context::CDMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i );
   if( it==nodeMap.end() ){
-    nodeMap[i] = d_counter;
-    d_counter++;
-    return d_counter-1;
+    unsigned c = d_counter.get();
+    nodeMap[i] = c;
+    d_counter.set( c + 1 );
+    return c;
+  }
+  return (*it).second;
+}
+
+void TransitiveClosureNode::debugPrint(){
+  for( int i=0; i<(int)currEdges.size(); i++ ){
+    cout << "currEdges[ " << i << " ] = " 
+         << currEdges[i].first << " -> " << currEdges[i].second;
+         //<< "(" << getId( currEdges[i].first ) << " -> " << getId( currEdges[i].second ) << ")";
+    cout << std::endl;
   }
-  return it->second;
 }
 
 
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index 4d811d0c9..af16d2e13 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -23,6 +23,10 @@
 #include "expr/node.h"
 #include <map>
 
+#include "context/cdlist.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
+
 namespace CVC4 {
 
 /*
@@ -65,14 +69,14 @@ public:
   }
 
   bool read(unsigned index) {
-    if (index < 64) return (d_data & (unsigned(1) << index)) != 0;
+    if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
     else if (d_next == NULL) return false;
     else return d_next->read(index - 64);
   }
 
   void write(unsigned index) {
     if (index < 64) {
-      unsigned mask = unsigned(1) << index;
+      unsigned mask = uint64_t(1) << index;
       if ((d_data & mask) != 0) return;
       makeCurrent();
       d_data = d_data | mask;
@@ -111,6 +115,8 @@ public:
 
   /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
   bool addEdge(unsigned i, unsigned j);
+  /** whether node i is connected to node j */
+  bool isConnected(unsigned i, unsigned j);
   void debugPrintMatrix();
 };
 
@@ -119,17 +125,26 @@ public:
  *
  */
 class TransitiveClosureNode : public TransitiveClosure{
-  static unsigned d_counter;
-  std::map< Node, unsigned > nodeMap;
+  context::CDO< unsigned > d_counter;
+  context::CDMap< Node, unsigned, NodeHashFunction > nodeMap;
   unsigned getId( Node i );
+  //for debugging
+  context::CDList< std::pair< Node, Node > > currEdges;
 public:
-  TransitiveClosureNode(context::Context* context) : TransitiveClosure(context) {}
+  TransitiveClosureNode(context::Context* context) : 
+    TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
   ~TransitiveClosureNode(){}
 
   /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
   bool addEdgeNode(Node i, Node j) {
+    currEdges.push_back( std::pair< Node, Node >( i, j ) );
     return addEdge( getId( i ), getId( j ) );
   }
+  /** whether node i is connected to node j */
+  bool isConnectedNode(Node i, Node j) {
+    return isConnected( getId( i ), getId( j ) );
+  }
+  void debugPrint();
 };
 
 }/* CVC4 namespace */