From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 4 Jun 2016 00:07:05 +0000 (-0500)
Subject: Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.
X-Git-Tag: cvc5-1.0.0~6049^2~8^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4498f55969576927c290b0fd26e0f94726068d03;p=cvc5.git

Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.
---

diff --git a/src/options/datatypes_options b/src/options/datatypes_options
index e9578f8d7..bb92b4e05 100644
--- a/src/options/datatypes_options
+++ b/src/options/datatypes_options
@@ -27,5 +27,7 @@ option dtInferAsLemmas --dt-infer-as-lemmas bool :default false
  always send lemmas out instead of making internal inferences
 #option dtRExplainLemmas --dt-rexplain-lemmas bool :default true
 # regression explanations for datatype lemmas
+option dtBlastSplits --dt-blast-splits bool :default false
+ when applicable, blast splitting lemmas for all variables at once
  
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7994351ee..a2f995935 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -94,9 +94,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak
   if( !hasEqcInfo( n ) ){
     if( doMake ){
       //add to labels
-      NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                             ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_labels.insertDataFromContextMemory( n, lbl );
+      d_labels[ n ] = 0;
 
       std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
       EqcInfo* ei;
@@ -109,10 +107,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak
       if( n.getKind()==APPLY_CONSTRUCTOR ){
         ei->d_constructor = n;
       }
+      
       //add to selectors
-      NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                               ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_selector_apps.insertDataFromContextMemory( n, sel );
+      d_selector_apps[n] = 0;
+      
       return ei;
     }else{
       return NULL;
@@ -181,6 +179,7 @@ void TheoryDatatypes::check(Effort e) {
     Trace("datatypes-debug") << "Check for splits " << e << endl;
     do {
       d_addedFact = false;
+      bool added_split = false;
       std::map< TypeNode, Node > rec_singletons;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
@@ -314,7 +313,10 @@ void TheoryDatatypes::check(Effort e) {
                     //doSendLemma( lemma );
                     d_out->lemma( lemma, false, false, true );
                   }
-                  return;
+                  added_split = true;
+                  if( !options::dtBlastSplits() ){
+                    return;
+                  }
                 }
               }else{
                 Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
@@ -326,6 +328,9 @@ void TheoryDatatypes::check(Effort e) {
         }
         ++eqcs_i;
       }
+      if( added_split ){
+        return;
+      }
       Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
       flushPendingFacts();
       /*
@@ -873,33 +878,36 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
 
 
       //merge labels
-      NodeListMap::iterator lbl_i = d_labels.find( t2 );
+      NodeIntMap::iterator lbl_i = d_labels.find( t2 );
       if( lbl_i != d_labels.end() ){
         Trace("datatypes-debug") << "  merge labels from " << eqc2 << " " << t2 << std::endl;
-        NodeList* lbl = (*lbl_i).second;
-        for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
-          Node tt = (*j).getKind()==kind::NOT ? (*j)[0] : (*j);
+        int n_label = (*lbl_i).second;
+        for( int i=0; i<n_label; i++ ){
+          Assert( i<(int)d_labels_data[ t2 ].size() );
+          Node t = d_labels_data[ t2 ][i];
+          Node tt = t.getKind()==kind::NOT ? t[0] : t;
           Node t_arg;
           int tindex = DatatypesRewriter::isTester( tt, t_arg );
           Assert( tindex!=-1 );
-          addTester( tindex, *j, eqc1, t1, t_arg );
+          addTester( tindex, t, eqc1, t1, t_arg );
           if( d_conflict ){
             Trace("datatypes-debug") << "  conflict!" << std::endl;
             return;
           }
         }
+
       }
       //merge selectors
       if( !eqc1->d_selectors && eqc2->d_selectors ){
         eqc1->d_selectors = true;
         checkInst = true;
       }
-      NodeListMap::iterator sel_i = d_selector_apps.find( t2 );
+      NodeIntMap::iterator sel_i = d_selector_apps.find( t2 );
       if( sel_i != d_selector_apps.end() ){
         Trace("datatypes-debug") << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
-        NodeList* sel = (*sel_i).second;
-        for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
-          addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() );
+        int n_sel = (*sel_i).second;
+        for( int j=0; j<n_sel; j++ ){
+          addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() );
         }
       }
       if( checkInst ){
@@ -930,11 +938,11 @@ bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
 }
 
 Node TheoryDatatypes::getLabel( Node n ) {
-  NodeListMap::iterator lbl_i = d_labels.find( n );
+  NodeIntMap::iterator lbl_i = d_labels.find( n );
   if( lbl_i != d_labels.end() ){
-    NodeList* lbl = (*lbl_i).second;
-    if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()!=kind::NOT ){
-      return (*lbl)[ (*lbl).size() - 1 ];
+    unsigned n_lbl = (*lbl_i).second;
+    if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){
+      return d_labels_data[n][ n_lbl-1 ];
     }
   }
   return Node::null();
@@ -957,9 +965,9 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
 }
 
 bool TheoryDatatypes::hasTester( Node n ) {
-  NodeListMap::iterator lbl_i = d_labels.find( n );
+  NodeIntMap::iterator lbl_i = d_labels.find( n );
   if( lbl_i != d_labels.end() ){
-    return !(*(*lbl_i).second).empty();
+    return (*lbl_i).second>0;
   }else{
     return false;
   }
@@ -972,13 +980,14 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   if( lindex!=-1 ){
     pcons[ lindex ] = true;
   }else{
-    NodeListMap::iterator lbl_i = d_labels.find( n );
+    NodeIntMap::iterator lbl_i = d_labels.find( n );
     if( lbl_i != d_labels.end() ){
-      NodeList* lbl = (*lbl_i).second;
-      for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-        Assert( (*i).getKind()==NOT );
-        //pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false;
-        int tindex = DatatypesRewriter::isTester( (*i)[0] );
+      int n_lbl = (*lbl_i).second;
+      for( int i=0; i<n_lbl; i++ ){
+        Node t = d_labels_data[n][i];
+        Assert( t.getKind()==NOT );
+        //pcons[ Datatype::indexOf( t[0].getOperator().toExpr() ) ] = false;
+        int tindex = DatatypesRewriter::isTester( t[0] );
         Assert( tindex!=-1 );
         pcons[ tindex ] = false;
       }
@@ -987,11 +996,11 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
 }
 
 void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) {
-  NodeListMap::iterator sel_i = d_selector_apps.find( r );
+  NodeIntMap::iterator sel_i = d_selector_apps.find( r );
   if( sel_i != d_selector_apps.end() ){
-    NodeList* sel = (*sel_i).second;
-    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
-      int sindex = Datatype::indexOf( (*j).getOperator().toExpr() );
+    int n_sel = (*sel_i).second;
+    for( int j=0; j<n_sel; j++ ){
+      int sindex = Datatype::indexOf( d_selector_apps_data[r][j].getOperator().toExpr() );
       sels[sindex] = true;
     }
   }
@@ -1058,12 +1067,13 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
     }
   }else{
     //otherwise, scan list of labels
-    NodeListMap::iterator lbl_i = d_labels.find( n );
+    NodeIntMap::iterator lbl_i = d_labels.find( n );
     Assert( lbl_i != d_labels.end() );
-    NodeList* lbl = (*lbl_i).second;
-    for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-      Assert( (*i).getKind()==NOT );
-      j = *i;
+    int n_lbl = (*lbl_i).second;
+    for( int i=0; i<n_lbl; i++ ){
+      Node ti = d_labels_data[n][i];
+      Assert( ti.getKind()==NOT );
+      j = ti;
       jt = j[0];
       //int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
       int jtindex = DatatypesRewriter::isTester( jt );
@@ -1079,16 +1089,24 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
     }
     if( !makeConflict ){
       Debug("datatypes-labels") << "Add to labels " << t << std::endl;
-      lbl->push_back( t );
+      //lbl->push_back( t );
+      d_labels[n] = n_lbl + 1;
+      if( n_lbl<(int)d_labels_data[n].size() ){
+        d_labels_data[n][n_lbl] = t;
+      }else{
+        d_labels_data[n].push_back( t );
+      }
+      n_lbl++;
+      
       const Datatype& dt = ((DatatypeType)(t_arg.getType()).toType()).getDatatype();
-      Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
+      Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
       if( tpolarity ){
         instantiate( eqc, n );
       }else{
         //check if we have reached the maximum number of testers
         // in this case, add the positive tester
         //this should not be done for sygus, since cases may be limited
-        if( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){
+        if( n_lbl==(int)dt.getNumConstructors()-1 && !dt.isSygus() ){
           std::vector< bool > pcons;
           getPossibleCons( eqc, n, pcons );
           int testerIndex = -1;
@@ -1102,11 +1120,14 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
           //we must explain why each term in the set of testers for this equivalence class is equal
           std::vector< Node > eq_terms;
           NodeBuilder<> nb(kind::AND);
-          for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-            nb << (*i);
-            Assert( (*i).getKind()==NOT );
+          //for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+          
+          for( int i=0; i<n_lbl; i++ ){
+            Node ti = d_labels_data[n][i];
+            nb << ti;
+            Assert( ti.getKind()==NOT );
             Node t_arg2;
-            DatatypesRewriter::isTester( (*i)[0], t_arg2 );
+            DatatypesRewriter::isTester( ti[0], t_arg2 );
             //Assert( tindex!=-1 );
             if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
               eq_terms.push_back( t_arg2 );
@@ -1143,19 +1164,26 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
 void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
   Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
   //check to see if it is redundant
-  NodeListMap::iterator sel_i = d_selector_apps.find( n );
+  NodeIntMap::iterator sel_i = d_selector_apps.find( n );
   Assert( sel_i != d_selector_apps.end() );
   if( sel_i != d_selector_apps.end() ){
-    NodeList* sel = (*sel_i).second;
-    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
-      Node ss = *j;
+    int n_sel = (*sel_i).second;
+    for( int j=0; j<n_sel; j++ ){
+      Node ss = d_selector_apps_data[n][j];
       if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
         Trace("dt-collapse-sel") << "...redundant." << std::endl;
         return;
       }
     }
     //add it to the vector
-    sel->push_back( s );
+    //sel->push_back( s );
+    d_selector_apps[n] = n_sel + 1;
+    if( n_sel<(int)d_selector_apps_data[n].size() ){
+      d_selector_apps_data[n][n_sel] = s;
+    }else{
+      d_selector_apps_data[n].push_back( s );
+    }
+  
     eqc->d_selectors = true;
   }
   if( assertFacts && !eqc->d_constructor.get().isNull() ){
@@ -1168,19 +1196,19 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
   Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
   Assert( eqc->d_constructor.get().isNull() );
   //check labels
-  NodeListMap::iterator lbl_i = d_labels.find( n );
+  NodeIntMap::iterator lbl_i = d_labels.find( n );
   if( lbl_i != d_labels.end() ){
     size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
-    NodeList* lbl = (*lbl_i).second;
-    for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-      if( (*i).getKind()==NOT ){
-        int tindex = DatatypesRewriter::isTester( (*i)[0] );
+    int n_lbl = (*lbl_i).second;
+    for( int i=0; i<n_lbl; i++ ){
+      Node t = d_labels_data[n][i];
+      if( t.getKind()==NOT ){
+        int tindex = DatatypesRewriter::isTester( t[0] );
         Assert( tindex!=-1 );
         if( tindex==(int)constructorIndex ){
-          Node n = *i;
           std::vector< TNode > assumptions;
-          explain( *i, assumptions );
-          explainEquality( c, (*i)[0][0], true, assumptions );
+          explain( t, assumptions );
+          explainEquality( c, t[0][0], true, assumptions );
           d_conflictNode = mkAnd( assumptions );
           Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
           d_out->conflict( d_conflictNode );
@@ -1191,12 +1219,13 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
     }
   }
   //check selectors
-  NodeListMap::iterator sel_i = d_selector_apps.find( n );
+  NodeIntMap::iterator sel_i = d_selector_apps.find( n );
   if( sel_i != d_selector_apps.end() ){
-    NodeList* sel = (*sel_i).second;
-    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
+    int n_sel = (*sel_i).second;
+    for( int j=0; j<n_sel; j++ ){
+      Node s = d_selector_apps_data[n][j];
       //collapse the selector
-      collapseSelector( *j, c );
+      collapseSelector( s, c );
     }
   }
   eqc->d_constructor.set( c );
@@ -2098,21 +2127,19 @@ void TheoryDatatypes::printModelDebug( const char* c ){
           if( hasLabel( ei, eqc ) ){
             Trace( c ) << getLabel( eqc );
           }else{
-            NodeListMap::iterator lbl_i = d_labels.find( eqc );
+            NodeIntMap::iterator lbl_i = d_labels.find( eqc );
             if( lbl_i != d_labels.end() ){
-              NodeList* lbl = (*lbl_i).second;
-              for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
-                Trace( c ) << *j << " ";
+              for( int j=0; j<(*lbl_i).second; j++ ){
+                Trace( c ) << d_labels_data[eqc][j] << " ";
               }
             }
           }
           Trace( c ) << std::endl;
           Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
-          NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
+          NodeIntMap::iterator sel_i = d_selector_apps.find( eqc );
           if( sel_i != d_selector_apps.end() ){
-            NodeList* sel = (*sel_i).second;
-            for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
-              Trace( c ) << *j << " ";
+            for( int j=0; j<(*sel_i).second; j++ ){
+              Trace( c ) << d_selector_apps_data[eqc][j] << " ";
             }
           }
           Trace( c ) << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index a1882d171..5722e7822 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -42,7 +42,7 @@ namespace datatypes {
 class TheoryDatatypes : public Theory {
 private:
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
 
@@ -162,9 +162,11 @@ private:
    *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t )  followed by
    *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
   */
-  NodeListMap d_labels;
+  NodeIntMap d_labels;
+  std::map< Node, std::vector< Node > > d_labels_data;
   /** selector apps for eqch equivalence class */
-  NodeListMap d_selector_apps;
+  NodeIntMap d_selector_apps;
+  std::map< Node, std::vector< Node > > d_selector_apps_data;
   /** constructor terms */
   //BoolMap d_consEqc;
   /** Are we in conflict */
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index c3064116f..5190025ee 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -53,10 +53,10 @@ void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) {
 }
 
 void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
   if( re_i!=d_rep_exp.end() ){
-    for( unsigned i=0; i<(*re_i).second->size(); i++ ){
-      addToExplanation( exp, (*(*re_i).second)[i] );
+    for( int i=0; i<(*re_i).second; i++ ){
+      addToExplanation( exp, d_rep_exp_data[eqc][i] );
     }
   }
   //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){
@@ -65,16 +65,19 @@ void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc
 }
 
 void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) {
-  NodeListMap::iterator re_i = d_rep_exp.find( eqc );
-  NodeList* re;
+  NodeIntMap::iterator re_i = d_rep_exp.find( eqc );
+  int n_re = 0;
   if( re_i != d_rep_exp.end() ){
-    re = (*re_i).second;
-  }else{
-    re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_rep_exp.insertDataFromContextMemory( eqc, re );
+    n_re = (*re_i).second;
   }
+  d_rep_exp[eqc] = n_re + exp_to_add.size();
   for( unsigned i=0; i<exp_to_add.size(); i++ ){
-    re->push_back( exp_to_add[i] );
+    if( n_re<(int)d_rep_exp_data[eqc].size() ){
+      d_rep_exp_data[eqc][n_re] = exp_to_add[i];
+    }else{
+      d_rep_exp_data[eqc].push_back( exp_to_add[i] );
+    }
+    n_re++;
   }
   //for( unsigned i=0; i<exp_to_add.size(); i++ ){
   //  eqci->d_rep_exp.push_back( exp_to_add[i] );
@@ -204,16 +207,18 @@ void EqualityInference::eqNotifyNewClass(TNode t) {
 
 void EqualityInference::addToUseList( Node used, Node eqc ) {
 #if 1
-  NodeListMap::iterator ul_i = d_uselist.find( used );
-  NodeList* ul;
+  NodeIntMap::iterator ul_i = d_uselist.find( used );
+  int n_ul = 0;
   if( ul_i != d_uselist.end() ){
-    ul = (*ul_i).second;
-  }else{
-    ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
-    d_uselist.insertDataFromContextMemory( used, ul );
+    n_ul = (*ul_i).second;
   }
+  d_uselist[ used ] = n_ul + 1;
   Trace("eq-infer-debug") << "      add to use list : " << used << " -> " << eqc << std::endl;
-  (*ul).push_back( eqc );  
+  if( n_ul<(int)d_uselist_data[used].size() ){
+    d_uselist_data[used][n_ul] = eqc;
+  }else{
+    d_uselist_data[used].push_back( eqc );  
+  }
 #else
   std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used );
   EqcInfo * eqci_used;
@@ -356,12 +361,12 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
               //go through all equivalence classes that may refer to v_solve
               std::map< Node, bool > processed;
               processed[v_solve] = true;
-              NodeListMap::iterator ul_i = d_uselist.find( v_solve );
+              NodeIntMap::iterator ul_i = d_uselist.find( v_solve );
               if( ul_i != d_uselist.end() ){
-                NodeList* ul = (*ul_i).second;
-                Trace("eq-infer-debug") << "      use list size = " << ul->size() << std::endl;
-                for( unsigned j=0; j<ul->size(); j++ ){
-                  Node r = (*ul)[j];
+                int n_ul = (*ul_i).second;
+                Trace("eq-infer-debug") << "      use list size = " << n_ul << std::endl;
+                for( int j=0; j<n_ul; j++ ){
+                  Node r = d_uselist_data[v_solve][j];
                 //Trace("eq-infer-debug") << "      use list size = " << eqci_solved->d_uselist.size() << std::endl;
                 //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){
                 //  Node r = eqci_solved->d_uselist[j];
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 93c7bd080..80d6ef98b 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -39,7 +39,7 @@ class EqualityInference
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap;
+  typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
 private:
   context::Context * d_c;
   Node d_one;
@@ -67,11 +67,13 @@ private:
   BoolMap d_elim_vars;
   std::map< Node, EqcInfo * > d_eqci;
   NodeMap d_rep_to_eqc;
-  NodeListMap d_rep_exp;
+  NodeIntMap d_rep_exp;
+  std::map< Node, std::vector< Node > > d_rep_exp_data;
   /** set eqc rep */
   void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci );
   /** use list */
-  NodeListMap d_uselist;
+  NodeIntMap d_uselist;
+  std::map< Node, std::vector< Node > > d_uselist_data;
   void addToUseList( Node used, Node eqc );
   /** pending merges */
   NodeList d_pending_merges;
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 38fea4f45..e682955e7 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -42,9 +42,7 @@ class SubsortSymmetryBreaker {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  //typedef context::CDChunkList<int> IntList;
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
 private:
   /** quantifiers engine */
   QuantifiersEngine* d_qe;