Merge branch 'master' of https://github.com/CVC4/CVC4

19 files changed, 448 insertions, 583 deletions

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/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 63afb0b72..d5874c52f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -552,10 +552,10 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   unsigned d_simplifyAssertionsDepth;
 
-  /** whether certain preprocess steps are necessary */
-  bool d_needsExpandDefs;
-  bool d_needsRewriteBoolTerms;
-  bool d_needsConstrainSubTypes;
+  /** TODO: whether certain preprocess steps are necessary */
+  //bool d_needsExpandDefs;
+  //bool d_needsRewriteBoolTerms;
+  //bool d_needsConstrainSubTypes;
 
 public:
   /**
@@ -684,9 +684,9 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
-    d_needsExpandDefs(true),
-    d_needsRewriteBoolTerms(true),
-    d_needsConstrainSubTypes(true), //TODO
+    //d_needsExpandDefs(true),
+    //d_needsRewriteBoolTerms(true),
+    //d_needsConstrainSubTypes(true), //TODO
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 95d704a0e..a2f995935 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -82,6 +82,8 @@ TheoryDatatypes::~TheoryDatatypes() {
     Assert(current != NULL);
     delete current;
   }
+  delete d_sygus_split;
+  delete d_sygus_sym_break;
 }
 
 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -92,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;
@@ -107,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;
@@ -179,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() ){
@@ -312,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;
@@ -324,6 +328,9 @@ void TheoryDatatypes::check(Effort e) {
         }
         ++eqcs_i;
       }
+      if( added_split ){
+        return;
+      }
       Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
       flushPendingFacts();
       /*
@@ -871,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 ){
@@ -928,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();
@@ -955,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;
   }
@@ -970,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;
       }
@@ -985,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;
     }
   }
@@ -1056,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 );
@@ -1077,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;
@@ -1100,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 );
@@ -1141,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() ){
@@ -1166,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 );
@@ -1189,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 );
@@ -2096,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/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index bd5100a2e..2d3bf76f6 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -32,6 +32,7 @@ namespace theory {
 namespace inst {
 
 InstMatchGenerator::InstMatchGenerator( Node pat ){
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
@@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
 }
 
 InstMatchGenerator::InstMatchGenerator() {
+  d_cg = NULL;
   d_needsReset = true;
   d_active_add = false;
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
 }
 
+InstMatchGenerator::~InstMatchGenerator() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  delete d_cg;
+}
+
 void InstMatchGenerator::setActiveAdd(bool val){
   d_active_add = val;
   if( d_next!=NULL ){
@@ -249,7 +258,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
       Trace("matching-debug2") << "Reset children..." << std::endl;
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
-      for( int i=0; i<(int)d_children.size(); i++ ){
+      for( unsigned i=0; i<d_children.size(); i++ ){
         d_children[i]->reset( t[ d_children_index[i] ], qe );
       }
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
@@ -484,7 +493,7 @@ d_f( q ){
     }
     Debug("smart-multi-trigger") << std::endl;
   }
-  for( int i=0; i<(int)pats.size(); i++ ){
+  for( unsigned i=0; i<pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
     d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
@@ -492,7 +501,7 @@ d_f( q ){
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
     int numSharedVars = 0;
-    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+    for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
         Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
         unique_vars.push_back( d_var_contains[n][j] );
@@ -503,7 +512,7 @@ d_f( q ){
     }
     //we use the latest shared variables, then unique variables
     std::vector< int > vars;
-    int index = i==0 ? (int)(pats.size()-1) : (i-1);
+    unsigned index = i==0 ? pats.size()-1 : (i-1);
     while( numSharedVars>0 && index!=i ){
       for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
         if( it->second ){
@@ -519,16 +528,24 @@ d_f( q ){
     }
     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
     Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
-    for( int i=0; i<(int)vars.size(); i++ ){
-      Debug("smart-multi-trigger") << vars[i] << " ";
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Debug("smart-multi-trigger") << vars[j] << " ";
     }
     Debug("smart-multi-trigger") << std::endl;
     //make ordered inst match trie
-    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
-    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
-    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
+    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
+    d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
+    d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
   }
+}
 
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    delete d_children[i];
+  }
+  for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
+    delete it->second;
+  }
 }
 
 /** reset instantiation round (call this whenever equivalence classes have changed) */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 49e3c1ec5..096774c51 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -91,7 +91,7 @@ public:
   InstMatchGenerator( Node pat );
   InstMatchGenerator();
   /** destructor */
-  ~InstMatchGenerator() throw() {}
+  virtual ~InstMatchGenerator() throw();
   /** The pattern we are producing matches for.
       If null, this is a multi trigger that is merging matches from d_children.
   */
@@ -125,7 +125,7 @@ public:
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
-  ~VarMatchGeneratorBooleanTerm() throw() {}
+  virtual ~VarMatchGeneratorBooleanTerm() throw() {}
   Node d_comp;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -142,7 +142,7 @@ public:
 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
-  ~VarMatchGeneratorTermSubs() throw() {}
+  virtual ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
   TypeNode d_var_type;
   Node d_subs;
@@ -183,6 +183,8 @@ private:
   int d_matchPolicy;
   /** children generators */
   std::vector< InstMatchGenerator* > d_children;
+  /** order */
+  std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
   /** inst match tries for each child */
   std::vector< InstMatchTrieOrdered > d_children_trie;
   /** calculate matches */
@@ -191,7 +193,7 @@ public:
   /** constructors */
   InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
-  ~InstMatchGeneratorMulti() throw() {}
+  virtual ~InstMatchGeneratorMulti() throw();
   /** reset instantiation round (call this whenever equivalence classes have changed) */
   void resetInstantiationRound( QuantifiersEngine* qe );
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 511337b40..68f824c57 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -48,7 +48,7 @@ bool QuantifiersRewriter::isClause( Node n ){
 bool QuantifiersRewriter::isLiteral( Node n ){
   switch( n.getKind() ){
   case NOT:
-    return isLiteral( n[0] );
+    return n[0].getKind()!=NOT && isLiteral( n[0] );
     break;
   case OR:
   case AND:
@@ -59,7 +59,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){
     return false;
     break;
   case EQUAL:
-    return n[0].getType()!=NodeManager::currentNM()->booleanType();
+    //for boolean terms
+    return !n[0].getType().isBoolean();
     break;
   default:
     break;
@@ -259,121 +260,98 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   return RewriteResponse( status, ret );
 }
 
-Node QuantifiersRewriter::computeElimSymbols( Node body ) {
-  if( isLiteral( body ) ){
-    return body;
-  }else{
-    bool childrenChanged = false;
-    Kind k = body.getKind();
-    if( body.getKind()==IMPLIES ){
-      k = OR;
-      childrenChanged = true;
-    }else if( body.getKind()==XOR ){
-      k = IFF;
+bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){
+  if( ( k==OR || k==AND ) && options::elimTautQuant() ){
+    Node lit = c.getKind()==NOT ? c[0] : c;
+    bool pol = c.getKind()!=NOT;
+    std::map< Node, bool >::iterator it = lit_pol.find( lit );
+    if( it==lit_pol.end() ){
+      lit_pol[lit] = pol;
+      children.push_back( c );
+    }else{
       childrenChanged = true;
-    }
-    std::vector< Node > children;
-    std::map< Node, bool > lit_pol;
-    for( unsigned i=0; i<body.getNumChildren(); i++ ){
-      Node c = computeElimSymbols( body[i] );
-      if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){
-        c = c.negate();
-      }
-      if( ( k==OR || k==AND ) && options::elimTautQuant() ){
-        Node lit = c.getKind()==NOT ? c[0] : c;
-        bool pol = c.getKind()!=NOT;
-        std::map< Node, bool >::iterator it = lit_pol.find( lit );
-        if( it==lit_pol.end() ){
-          lit_pol[lit] = pol;
-          children.push_back( c );
-        }else{
-          childrenChanged = true;
-          if( it->second!=pol ){
-            return NodeManager::currentNM()->mkConst( k==OR );
-          }
-        }
-      }else{
-        children.push_back( c );
+      if( it->second!=pol ){
+        return false;
       }
-      childrenChanged = childrenChanged || c!=body[i];
-    }
-    //if( body.getKind()==ITE && isLiteral( body[0] ) ){
-    //  ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), 
-    //                                               NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) );
-    //}
-    if( childrenChanged ){
-      return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
-    }else{
-      return body;
     }
+  }else{
+    children.push_back( c );
   }
+  return true;
 }
 
-Node QuantifiersRewriter::computeNNF( Node body ){
-  if( body.getKind()==NOT ){
+// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF
+Node QuantifiersRewriter::computeElimSymbols( Node body ) {
+  Kind ok = body.getKind();
+  Kind k = ok;
+  bool negAllCh = false;
+  bool negCh1 = false;
+  if( ok==IMPLIES ){
+    k = OR;
+    negCh1 = true;
+  }else if( ok==XOR ){
+    k = IFF;
+    negCh1 = true;
+  }else if( ok==NOT ){
     if( body[0].getKind()==NOT ){
-      return computeNNF( body[0][0] );
-    }else if( isLiteral( body[0] ) ){
-      return body;
+      return computeElimSymbols( body[0][0] );
+    }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){
+      k = AND;   
+      negAllCh = true;
+      negCh1 = body[0].getKind()==IMPLIES;
+      body = body[0];
+    }else if( body[0].getKind()==AND ){
+      k = OR;
+      negAllCh = true;
+      body = body[0];
+    }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){
+      k = IFF;
+      negCh1 = ( body[0].getKind()==IFF );
+      body = body[0];
+    }else if( body[0].getKind()==ITE ){
+      k = body[0].getKind();
+      negAllCh = true;
+      negCh1 = true;
+      body = body[0];
     }else{
-      std::vector< Node > children; 
-      Kind k = body[0].getKind();
-
-      if( body[0].getKind()==OR || body[0].getKind()==AND ){
-        k = body[0].getKind()==AND ? OR : AND;
-        for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          Node nc = computeNNF( body[0][i].notNode() );
-          if( nc.getKind()==k ){
-            for( unsigned j=0; j<nc.getNumChildren(); j++ ){
-              children.push_back( nc[j] );
-            }
-          }else{
-            children.push_back( nc );
-          }
-        }
-      }else if( body[0].getKind()==IFF ){
-        for( int i=0; i<2; i++ ){
-          Node nn = i==0 ? body[0][i] : body[0][i].notNode();
-          children.push_back( computeNNF( nn ) );
-        }
-      }else if( body[0].getKind()==ITE ){
-        for( int i=0; i<3; i++ ){
-          Node nn = i==0 ? body[0][i] : body[0][i].notNode();
-          children.push_back( computeNNF( nn ) );
-        }
-      }else{
-        Notice() << "Unhandled Quantifiers NNF: " << body << std::endl;
-        return body;
-      }
-      return NodeManager::currentNM()->mkNode( k, children );
+      return body;
     }
-  }else if( isLiteral( body ) ){
+  }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){
+    //a literal
     return body;
-  }else{
-    std::vector< Node > children;
-    bool childrenChanged = false;
-    bool isAssoc = body.getKind()==AND || body.getKind()==OR;
-    for( int i=0; i<(int)body.getNumChildren(); i++ ){
-      Node nc = computeNNF( body[i] );
-      if( isAssoc && nc.getKind()==body.getKind() ){
-        for( unsigned j=0; j<nc.getNumChildren(); j++ ){
-          children.push_back( nc[j] );
+  }
+  bool childrenChanged = false;
+  std::vector< Node > children;
+  std::map< Node, bool > lit_pol;
+  for( unsigned i=0; i<body.getNumChildren(); i++ ){
+    Node c = computeElimSymbols( ( i==0 && negCh1 )!=negAllCh ? body[i].negate() : body[i] );
+    bool success = true;
+    if( c.getKind()==k && ( k==OR || k==AND ) ){
+      //flatten
+      childrenChanged = true;
+      for( unsigned j=0; j<c.getNumChildren(); j++ ){
+        if( !addCheckElimChild( children, c[j], k, lit_pol, childrenChanged ) ){
+          success = false;
+          break;
         }
-        childrenChanged = true;
-      }else{
-        children.push_back( nc );
-        childrenChanged = childrenChanged || nc!=body[i];
       }
-    }
-    if( childrenChanged ){
-      return NodeManager::currentNM()->mkNode( body.getKind(), children );
     }else{
-      return body;
+      success = addCheckElimChild( children, c, k, lit_pol, childrenChanged );
+    }
+    if( !success ){
+      // tautology
+      Assert( k==OR || k==AND );
+      return NodeManager::currentNM()->mkConst( k==OR );
     }
+    childrenChanged = childrenChanged || c!=body[i];
+  }
+  if( childrenChanged || k!=ok ){
+    return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
+  }else{
+    return body;
   }
 }
 
-
 void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
                                                    std::vector< Node >& conj ){
   if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
@@ -1036,144 +1014,6 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computeClause( Node n ){
-  Assert( isClause( n ) );
-  if( isLiteral( n ) ){
-    return n;
-  }else{
-    NodeBuilder<> t(OR);
-    if( n.getKind()==NOT ){
-      if( n[0].getKind()==NOT ){
-        return computeClause( n[0][0] );
-      }else{
-        //De-Morgan's law
-        Assert( n[0].getKind()==AND );
-        for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
-          Node nn = computeClause( n[0][i].notNode() );
-          addNodeToOrBuilder( nn, t );
-        }
-      }
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        Node nn = computeClause( n[i] );
-        addNodeToOrBuilder( nn, t );
-      }
-    }
-    return t.constructNode();
-  }
-}
-
-Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
-  if( isLiteral( n ) ){
-    return n;
-  }else if( !forcePred && isClause( n ) ){
-    return computeClause( n );
-  }else{
-    Kind k = n.getKind();
-    NodeBuilder<> t(k);
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node nc = n[i];
-      Node ncnf = computeCNF( nc, args, defs, k!=OR );
-      if( k==OR ){
-        addNodeToOrBuilder( ncnf, t );
-      }else{
-        t << ncnf;
-      }
-    }
-    if( !forcePred && k==OR ){
-      return t.constructNode();
-    }else{
-      //compute the free variables
-      Node nt = t;
-      std::vector< Node > activeArgs;
-      computeArgVec( args, activeArgs, nt );
-      std::vector< TypeNode > argTypes;
-      for( int i=0; i<(int)activeArgs.size(); i++ ){
-        argTypes.push_back( activeArgs[i].getType() );
-      }
-      //create the predicate
-      Assert( argTypes.size()>0 );
-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
-      std::stringstream ss;
-      ss << "cnf_" << n.getKind() << "_" << n.getId();
-      Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" );
-      std::vector< Node > predArgs;
-      predArgs.push_back( op );
-      predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
-      Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs );
-      Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
-      //create the bound var list
-      Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs );
-      //now, look at the structure of nt
-      if( nt.getKind()==NOT ){
-        //case for NOT
-        for( int i=0; i<2; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( i==0 ? nt[0].notNode() : nt[0] );
-          tt << ( i==0 ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else if( nt.getKind()==OR ){
-        //case for OR
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          NodeBuilder<> tt(OR);
-          tt << nt[i].notNode() << pred;
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-        NodeBuilder<> tt(OR);
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          tt << nt[i];
-        }
-        tt << pred.notNode();
-        defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-      }else if( nt.getKind()==AND ){
-        //case for AND
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          NodeBuilder<> tt(OR);
-          tt << nt[i] << pred.notNode();
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-        NodeBuilder<> tt(OR);
-        for( int i=0; i<(int)nt.getNumChildren(); i++ ){
-          tt << nt[i].notNode();
-        }
-        tt << pred;
-        defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-      }else if( nt.getKind()==IFF ){
-        //case for IFF
-        for( int i=0; i<4; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] );
-          tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] );
-          tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else if( nt.getKind()==ITE ){
-        //case for ITE
-        for( int j=1; j<=2; j++ ){
-          for( int i=0; i<2; i++ ){
-            NodeBuilder<> tt(OR);
-            tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] );
-            tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] );
-            tt << ( ( i==0 ) ? pred.notNode() : pred );
-            defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-          }
-        }
-        for( int i=0; i<2; i++ ){
-          NodeBuilder<> tt(OR);
-          tt << ( i==0 ? nt[1].notNode() : nt[1] );
-          tt << ( i==0 ? nt[2].notNode() : nt[2] );
-          tt << ( i==1 ? pred.notNode() : pred );
-          defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
-        }
-      }else{
-        Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl;
-      }
-      return pred;
-    }
-  }
-}
-
 Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
   if( body.getKind()==FORALL ){
     if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
@@ -1181,15 +1021,13 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
       //must rename each variable that already exists
-      for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-        //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
+      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
         terms.push_back( body[0][i] );
         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
       args.insert( args.end(), subs.begin(), subs.end() );
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-      Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl;
       return newBody;
     }else{
       return body;
@@ -1198,7 +1036,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
-    for( int i=0; i<(int)body.getNumChildren(); i++ ){
+    for( unsigned i=0; i<body.getNumChildren(); i++ ){
       bool newHasPol;
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
@@ -1224,7 +1062,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
   }
 }
 
-Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node body ) {
+Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
   Assert( body.getKind()==OR );
   size_t var_found_count = 0;
   size_t eqc_count = 0;
@@ -1240,8 +1078,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
     Node n = body[i];
     std::vector< Node > lit_args;
     computeArgVec( args, lit_args, n );
-    if (lit_args.empty()) {
-      lits.push_back(n);
+    if( lit_args.empty() ){
+      lits.push_back( n );
     }else {
       //collect the equivalence classes this literal belongs to, and the new variables it contributes
       std::vector< int > eqcs;
@@ -1293,8 +1131,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
       eqc_to_lit[eqcz].push_back(n);
     }
   }
-  if ( eqc_active>1 || !lits.empty() ){
-    Trace("clause-split-debug") << "Split clause " << f << std::endl;
+  if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){
+    Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl;
     Trace("clause-split-debug") << "   Ground literals: " << std::endl;
     for( size_t i=0; i<lits.size(); i++) {
       Trace("clause-split-debug") << "      " << lits[i] << std::endl;
@@ -1317,27 +1155,21 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
       Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
       lits.push_back(fa);
     }
-    Assert( lits.size()>1 );
-    Node nf = NodeManager::currentNM()->mkNode(OR,lits);
+    Assert( !lits.empty() );
+    Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits);
     Trace("clause-split-debug") << "Made node : " << nf << std::endl;
     return nf;
+  }else{
+    return mkForAll( args, body, qa );
   }
-  return f;
 }
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){
-  std::vector< Node > activeArgs;
-  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
-  if( options::ceGuidedInst() && qa.d_sygus ){
-    activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
-  }else{
-    computeArgVec2( args, activeArgs, body, qa.d_ipl );
-  }
-  if( activeArgs.empty() ){
+  if( args.empty() ){
     return body;
   }else{
     std::vector< Node > children;
-    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
+    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
     children.push_back( body );
     if( !qa.d_ipl.isNull() ){
       children.push_back( qa.d_ipl );
@@ -1346,82 +1178,59 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri
   }
 }
 
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){
+//computes miniscoping, also eliminates variables that do not occur free in body
+Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
   if( body.getKind()==FORALL ){
-    //combine arguments
+    //combine prenex
     std::vector< Node > newArgs;
-    for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+    newArgs.insert( newArgs.end(), args.begin(), args.end() );
+    for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
       newArgs.push_back( body[0][i] );
     }
-    newArgs.insert( newArgs.end(), args.begin(), args.end() );
-    return mkForAll( newArgs, body[ 1 ], qa );
-  }else{
-    if( body.getKind()==NOT ){
-      //push not downwards
-      if( body[0].getKind()==NOT ){
-        return computeMiniscoping( f, args, body[0][0], qa );
-      }else if( body[0].getKind()==AND ){
-        if( options::miniscopeQuantFreeVar() ){
-          NodeBuilder<> t(kind::OR);
-          for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-            t <<  ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
-          }
-          return computeMiniscoping( f, args, t.constructNode(), qa );
-        }
-      }else if( body[0].getKind()==OR ){
-        if( options::miniscopeQuant() ){
-          NodeBuilder<> t(kind::AND);
-          for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-            Node trm = body[0][i].negate();
-            t << computeMiniscoping( f, args, trm, qa );
-          }
-          return t.constructNode();
+    return mkForAll( newArgs, body[1], qa );
+  }else if( body.getKind()==AND ){
+    if( options::miniscopeQuant() ){
+      //break apart
+      NodeBuilder<> t(kind::AND);
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        t << computeMiniscoping( args, body[i], qa );
+      }
+      Node retVal = t;
+      return retVal;
+    }
+  }else if( body.getKind()==OR ){
+    if( options::quantSplit() ){
+      //splitting subsumes free variable miniscoping, apply it with higher priority
+      return computeSplit( args, body, qa );
+    }else if( options::miniscopeQuantFreeVar() ){
+      Node newBody = body;
+      NodeBuilder<> body_split(kind::OR);
+      NodeBuilder<> tb(kind::OR);
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        Node trm = body[i];
+        if( TermDb::containsTerms( body[i], args ) ){
+          tb << trm;
+        }else{
+          body_split << trm;
         }
       }
-    }else if( body.getKind()==AND ){
-      if( options::miniscopeQuant() ){
-        //break apart
-        NodeBuilder<> t(kind::AND);
-        for( unsigned i=0; i<body.getNumChildren(); i++ ){
-          t << computeMiniscoping( f, args, body[i], qa );
-        }
-        Node retVal = t;
-        return retVal;
-      }
-    }else if( body.getKind()==OR ){
-      if( options::quantSplit() ){
-        //splitting subsumes free variable miniscoping, apply it with higher priority
-        Node nf = computeSplit( f, args, body );
-        if( nf!=f ){
-          return nf;
-        }
-      }else if( options::miniscopeQuantFreeVar() ){
-        Node newBody = body;
-        NodeBuilder<> body_split(kind::OR);
-        NodeBuilder<> tb(kind::OR);
-        for( unsigned i=0; i<body.getNumChildren(); i++ ){
-          Node trm = body[i];
-          if( TermDb::containsTerms( body[i], args ) ){
-            tb << trm;
-          }else{
-            body_split << trm;
-          }
-        }
-        if( tb.getNumChildren()==0 ){
-          return body_split;
-        }else if( body_split.getNumChildren()>0 ){
-          newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
-          body_split << mkForAll( args, newBody, qa );
-          return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
-        }
+      if( tb.getNumChildren()==0 ){
+        return body_split;
+      }else if( body_split.getNumChildren()>0 ){
+        newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
+        std::vector< Node > activeArgs;
+        computeArgVec2( args, activeArgs, newBody, qa.d_ipl );
+        body_split << mkForAll( activeArgs, newBody, qa );
+        return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
       }
     }
+  }else if( body.getKind()==NOT ){
+    Assert( isLiteral( body[0] ) );
   }
-  //if( body==f[1] ){
-  //  return f;
-  //}else{
-  return mkForAll( args, body, qa );
-  //}
+  //remove variables that don't occur
+  std::vector< Node > activeArgs;
+  computeArgVec2( args, activeArgs, body, qa.d_ipl );
+  return mkForAll( activeArgs, body, qa );
 }
 
 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
@@ -1539,8 +1348,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
     return is_std;
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant() && is_std;
-  }else if( computeOption==COMPUTE_NNF ){
-    return true;
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return options::condRewriteQuant();
   }else if( computeOption==COMPUTE_COND_SPLIT ){
@@ -1549,8 +1356,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
-  //}else if( computeOption==COMPUTE_CNF ){
-  //  return options::cnfQuant();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
     return options::purifyQuant() && is_std;
   }else{
@@ -1570,11 +1375,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
     //return directly
-    return computeMiniscoping( f, args, n, qa );
+    return computeMiniscoping( args, n, qa );
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return computeAggressiveMiniscoping( args, n );
-  }else if( computeOption==COMPUTE_NNF ){
-    n = computeNNF( n );
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     std::vector< Node > new_conds;
     n = computeProcessTerms( n, args, new_conds, f, qa );
@@ -1588,9 +1391,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     n = computePrenex( n, args, true );
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
-  //}else if( computeOption==COMPUTE_CNF ){
-    //n = computeCNF( n, args, defs, false );
-    //ipl = Node::null();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
     std::vector< Node > conj;
     computePurifyExpand( n, conj, args, qa );
@@ -1724,15 +1524,15 @@ struct ContainsQuantAttributeId {};
 typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
 
 // check if the given node contains a universal quantifier
-bool QuantifiersRewriter::containsQuantifiers(Node n) {
+bool QuantifiersRewriter::containsQuantifiers( Node n ){
   if( n.hasAttribute(ContainsQuantAttribute()) ){
     return n.getAttribute(ContainsQuantAttribute())==1;
-  } else if(n.getKind() == kind::FORALL) {
+  }else if( n.getKind() == kind::FORALL ){
     return true;
-  } else {
+  }else{
     bool cq = false;
     for( unsigned i = 0; i < n.getNumChildren(); ++i ){
-      if( containsQuantifiers(n[i]) ){
+      if( containsQuantifiers( n[i] ) ){
         cq = true;
         break;
       }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 2071d1793..776517109 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -38,6 +38,7 @@ public:
   static int getPurifyId( Node n );
   static int getPurifyIdLit( Node n );
 private:
+  static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
@@ -46,7 +47,6 @@ private:
   static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds );
-  static Node computeClause( Node n );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
   static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
@@ -57,15 +57,13 @@ private:
   static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent );
 private:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa );
+  static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
-  static Node computeNNF( Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
-  static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
-  static Node computeSplit( Node f, std::vector< Node >& args, Node body );
+  static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
   static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
   static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa );
@@ -74,7 +72,6 @@ private:
     COMPUTE_ELIM_SYMBOLS = 0,
     COMPUTE_MINISCOPING,
     COMPUTE_AGGRESSIVE_MINISCOPING,
-    COMPUTE_NNF,
     COMPUTE_PROCESS_TERMS,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
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;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5645c3401..c34d86497 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) {
     if( it!=d_op_map.end() ){
       eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
       Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+      unsigned congruentCount = 0;
+      unsigned nonCongruentCount = 0;
+      unsigned alreadyCongruentCount = 0;
+      unsigned relevantCount = 0;
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node n = it->second[i];
         //to be added to term index, term must be relevant, and exist in EE
         if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+          relevantCount++;
           if( isTermActive( n ) ){
             computeArgReps( n );
 
@@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) {
             if( at!=n && ee->areEqual( at, n ) ){
               setTermInactive( n );
               Trace("term-db-debug") << n << " is redundant." << std::endl;
-              //congruentCount++;
+              congruentCount++;
             }else{
               if( at!=n && ee->areDisequal( at, n, false ) ){
                 std::vector< Node > lits;
@@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) {
                 d_consistent_ee = false;
                 return;
               }
-              //nonCongruentCount++;
+              nonCongruentCount++;
               d_op_nonred_count[ f ]++;
             }
           }else{
             Trace("term-db-debug") << n << " is already redundant." << std::endl;
-            //congruentCount++;
-            //alreadyCongruentCount++;
+            alreadyCongruentCount++;
           }
         }else{
           Trace("term-db-debug") << n << " is not relevant." << std::endl;
-          //nonRelevantCount++;
         }
       }
-      
-      /*
-      if( Trace.isOn("term-db-index") ){
-        Trace("term-db-index") << "Term index for " << f << " : " << std::endl;
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]);
-        Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = ";
-        Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; 
+      if( Trace.isOn("tdb") ){
+        Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / ";
+        Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / ";
+        Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
       }
-      */
     }
   }
 }
@@ -676,10 +674,6 @@ void TermDb::presolve() {
 }
 
 bool TermDb::reset( Theory::Effort effort ){
-  //int nonCongruentCount = 0;
-  //int congruentCount = 0;
-  //int alreadyCongruentCount = 0;
-  //int nonRelevantCount = 0;
   d_op_nonred_count.clear();
   d_arg_reps.clear();
   d_func_map_trie.clear();
@@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
 */  
-  /*
-  Trace("term-db-stats") << "TermDb: Reset" << std::endl;
-  Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
-  Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
-  if( Trace.isOn("term-db-index") ){
-    Trace("term-db-index") << "functions : " << std::endl;
-    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-      if( it->second.size()>0 ){
-        Trace("term-db-index") << "- " << it->first << std::endl;
-        d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
-      }
-    }
-  }
-  */
   return true;
 }
 
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 214a4d055..802acc089 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
 }
 
 Trigger::~Trigger() {
-  if(d_mg != NULL) { delete d_mg; }
+  delete d_mg;
 }
 
 void Trigger::resetInstantiationRound(){
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 53344dd6c..a665a02c1 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -39,6 +39,10 @@ RegExpOpr::RegExpOpr()
   d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
 }
 
+RegExpOpr::~RegExpOpr(){ 
+
+}
+
 int RegExpOpr::gcd ( int a, int b ) {
   int c;
   while ( a != 0 ) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index c537553f2..075391370 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -99,6 +99,7 @@ private:
 
 public:
   RegExpOpr();
+  ~RegExpOpr();
 
   bool checkConstRegExp( Node r );
   void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 497ce5f8c..57344236e 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2726,23 +2726,17 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
 
 void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){
   if( !isNormalFormPair( n1, n2 ) ){
-    //Assert( !isNormalFormPair( n1, n2 ) );
-    NodeList* lst;
-    NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-    if( nf_i == d_nf_pairs.end() ){
-      if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
-        addNormalFormPair( n2, n1 );
-        return;
-      }
-      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                           ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_nf_pairs.insertDataFromContextMemory( n1, lst );
-      Trace("strings-nf") << "Create cache for " << n1 << std::endl;
-    } else {
-      lst = (*nf_i).second;
-    }
-    Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
-    lst->push_back( n2 );
+    int index = 0;
+    NodeIntMap::const_iterator it = d_nf_pairs.find( n1 );
+    if( it!=d_nf_pairs.end() ){
+      index = (*it).second;
+    }
+    d_nf_pairs[n1] = index + 1;
+    if( index<(int)d_nf_pairs_data[n1].size() ){
+      d_nf_pairs_data[n1][index] = n2;
+    }else{
+      d_nf_pairs_data[n1].push_back( n2 );
+    } 
     Assert( isNormalFormPair( n1, n2 ) );
   } else {
     Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
@@ -2755,15 +2749,14 @@ bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
 }
 
 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
-    //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
-  NodeList* lst;
-  NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-  if( nf_i != d_nf_pairs.end() ) {
-    lst = (*nf_i).second;
-    for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
-      Node n = *i;
-      if( n==n2 ) {
-          return true;
+  //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
+  NodeIntMap::const_iterator it = d_nf_pairs.find( n1 );
+  if( it!=d_nf_pairs.end() ){
+    Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() );
+    for( int i=0; i<(*it).second; i++ ){
+      Assert( i<(int)d_nf_pairs_data[n1].size() );
+      if( d_nf_pairs_data[n1][i]==n2 ){
+        return true;
       }
     }
   }
@@ -3428,6 +3421,26 @@ void TheoryStrings::updateMpl( Node n, int b ) {
 }
 */
 
+
+unsigned TheoryStrings::getNumMemberships( Node n, bool isPos ) {
+  if( isPos ){
+    NodeIntMap::const_iterator it = d_pos_memberships.find( n );
+    if( it!=d_pos_memberships.end() ){
+      return (*it).second;
+    }
+  }else{
+    NodeIntMap::const_iterator it = d_neg_memberships.find( n );
+    if( it!=d_neg_memberships.end() ){
+      return (*it).second;
+    }
+  }
+  return 0;
+}
+
+Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) {
+  return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i];
+}
+
 //// Regular Expressions
 Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
   if(d_regexp_ant.find(atom) == d_regexp_ant.end()) {
@@ -3505,10 +3518,8 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node >
 
   Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl;
 
-  for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin();
-    itr_xr != d_pos_memberships.end(); ++itr_xr ) {
+  for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){
     Node x = (*itr_xr).first;
-    NodeList* lst = (*itr_xr).second;
     Node nf_x = x;
     std::vector< Node > nf_x_exp;
     if(d_normal_forms.find( x ) != d_normal_forms.end()) {
@@ -3522,10 +3533,11 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node >
 
     std::vector< Node > vec_x;
     std::vector< Node > vec_r;
-    for(NodeList::const_iterator itr_lst = lst->begin();
-        itr_lst != lst->end(); ++itr_lst) {
-      Node r = *itr_lst;
-      Node nf_r = normalizeRegexp((*lst)[0]);
+    unsigned n_pmem = (*itr_xr).second;
+    Assert( getNumMemberships( x, true )==n_pmem );
+    for( unsigned k=0; k<n_pmem; k++ ){
+      Node r = getMembership( x, true, k );
+      Node nf_r = normalizeRegexp( r );  //AJR: fixed (was normalizing mem #0 always)
       Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r);
       if(d_processed_memberships.find(memb) == d_processed_memberships.end()) {
         if(d_regexp_opr.checkConstRegExp(nf_r)) {
@@ -3755,46 +3767,43 @@ void TheoryStrings::checkMemberships() {
   Trace("regexp-debug") << "Checking Memberships ... " << std::endl;
   //if(options::stringEIT()) {
     //TODO: Opt for normal forms
-    for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin();
-      itr_xr != d_pos_memberships.end(); ++itr_xr ) {
+    for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){
       bool spflag = false;
       Node x = (*itr_xr).first;
-      NodeList* lst = (*itr_xr).second;
       Trace("regexp-debug") << "Checking Memberships for " << x << std::endl;
       if(d_inter_index.find(x) == d_inter_index.end()) {
         d_inter_index[x] = 0;
       }
       int cur_inter_idx = d_inter_index[x];
-      if(cur_inter_idx != (int)lst->size()) {
-        if(lst->size() == 1) {
-          d_inter_cache[x] = (*lst)[0];
+      unsigned n_pmem = (*itr_xr).second;
+      Assert( getNumMemberships( x, true )==n_pmem );
+      if( cur_inter_idx != (int)n_pmem ) {
+        if( n_pmem == 1) {
+          d_inter_cache[x] = getMembership( x, true, 0 );
           d_inter_index[x] = 1;
           Trace("regexp-debug") << "... only one choice " << std::endl;
-        } else if(lst->size() > 1) {
+        } else if(n_pmem > 1) {
           Node r;
           if(d_inter_cache.find(x) != d_inter_cache.end()) {
             r = d_inter_cache[x];
           }
           if(r.isNull()) {
-            r = (*lst)[0];
+            r = getMembership( x, true, 0 );
             cur_inter_idx = 1;
           }
-          NodeList::const_iterator itr_lst = lst->begin();
-          for(int i=0; i<cur_inter_idx; i++) {
-            ++itr_lst;
-          }
-          Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << lst->size() << std::endl;
-          for(;itr_lst != lst->end(); ++itr_lst) {
-            Node r2 = *itr_lst;
+
+          unsigned k_start = cur_inter_idx;
+          Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << n_pmem << std::endl;
+          for(unsigned k = k_start; k<n_pmem; k++) {
+            Node r2 = getMembership( x, true, k );
             r = d_regexp_opr.intersect(r, r2, spflag);
             if(spflag) {
               break;
             } else if(r == d_emptyRegexp) {
               std::vector< Node > vec_nodes;
-              ++itr_lst;
-              for(NodeList::const_iterator itr2 = lst->begin();
-                itr2 != itr_lst; ++itr2) {
-                Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
+              for( unsigned kk=0; kk<=k; kk++ ){
+                Node rr = getMembership( x, true, kk );
+                Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, rr);
                 vec_nodes.push_back( n );
               }
               Node conc;
@@ -3809,7 +3818,7 @@ void TheoryStrings::checkMemberships() {
           //updates
           if(!d_conflict && !spflag) {
             d_inter_cache[x] = r;
-            d_inter_index[x] = (int)lst->size();
+            d_inter_index[x] = (int)n_pmem;
           }
         }
       }
@@ -4432,44 +4441,52 @@ void TheoryStrings::addMembership(Node assertion) {
   Node x = atom[0];
   Node r = atom[1];
   if(polarity) {
-    NodeList* lst;
-    NodeListMap::iterator itr_xr = d_pos_memberships.find( x );
-    if( itr_xr == d_pos_memberships.end() ){
-      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_pos_memberships.insertDataFromContextMemory( x, lst );
-    } else {
-      lst = (*itr_xr).second;
-    }
-    //check
-    for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) {
-      if( r == *itr ) {
-        return;
+    int index = 0;
+    NodeIntMap::const_iterator it = d_pos_memberships.find( x );
+    if( it!=d_nf_pairs.end() ){
+      index = (*it).second;
+      for( int k=0; k<index; k++ ){
+        if( k<(int)d_pos_memberships_data[x].size() ){
+          if( d_pos_memberships_data[x][k]==r ){
+            return;
+          }
+        }else{
+          break;
+        }
       }
     }
-    lst->push_back( r );
+    d_pos_memberships[x] = index + 1;
+    if( index<(int)d_pos_memberships_data[x].size() ){
+      d_pos_memberships_data[x][index] = r;
+    }else{
+      d_pos_memberships_data[x].push_back( r );
+    }
   } else if(!options::stringIgnNegMembership()) {
     /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
       int rt;
       Node r2 = d_regexp_opr.complement(r, rt);
       Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
     }*/
-    NodeList* lst;
-    NodeListMap::iterator itr_xr = d_neg_memberships.find( x );
-    if( itr_xr == d_neg_memberships.end() ){
-      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_neg_memberships.insertDataFromContextMemory( x, lst );
-    } else {
-      lst = (*itr_xr).second;
-    }
-    //check
-    for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) {
-      if( r == *itr ) {
-        return;
+    int index = 0;
+    NodeIntMap::const_iterator it = d_neg_memberships.find( x );
+    if( it!=d_nf_pairs.end() ){
+      index = (*it).second;
+      for( int k=0; k<index; k++ ){
+        if( k<(int)d_neg_memberships_data[x].size() ){
+          if( d_neg_memberships_data[x][k]==r ){
+            return;
+          }
+        }else{
+          break;
+        }
       }
     }
-    lst->push_back( r );
+    d_neg_memberships[x] = index + 1;
+    if( index<(int)d_neg_memberships_data[x].size() ){
+      d_neg_memberships_data[x][index] = r;
+    }else{
+      d_neg_memberships_data[x].push_back( r );
+    }
   }
   // old
   if(polarity || !options::stringIgnNegMembership()) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index c9e0a29bf..2deb09654 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -50,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri
 
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
@@ -165,7 +164,8 @@ private:
   std::map< Node, std::vector< Node > > d_normal_forms_exp;
   std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
   //map of pairs of terms that have the same normal form
-  NodeListMap d_nf_pairs;
+  NodeIntMap d_nf_pairs;
+  std::map< Node, std::vector< Node > > d_nf_pairs_data;
   void addNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair( Node n1, Node n2 );
   bool isNormalFormPair2( Node n1, Node n2 );
@@ -421,8 +421,12 @@ private:
   NodeSet d_regexp_ucached;
   NodeSet d_regexp_ccached;
   // stored assertions
-  NodeListMap d_pos_memberships;
-  NodeListMap d_neg_memberships;
+  NodeIntMap d_pos_memberships;
+  std::map< Node, std::vector< Node > > d_pos_memberships_data;
+  NodeIntMap d_neg_memberships;
+  std::map< Node, std::vector< Node > > d_neg_memberships_data;
+  unsigned getNumMemberships( Node n, bool isPos );
+  Node getMembership( Node n, bool isPos, unsigned i );
   // semi normal forms for symbolic expression
   std::map< Node, Node > d_nf_regexps;
   std::map< Node, std::vector< Node > > d_nf_regexps_exp;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a4f42bddd..ba811644a 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -33,6 +33,10 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){
   d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 }
 
+StringsPreprocess::~StringsPreprocess(){
+
+}
+
 /*
 int StringsPreprocess::checkFixLenVar( Node t ) {
   int ret = 2;
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 5bc9667ea..abc7b5a91 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -40,6 +40,7 @@ private:
   Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
   StringsPreprocess( context::UserContext* u );
+  ~StringsPreprocess();
 
   Node decompose( Node t, std::vector< Node > &new_nodes );
   void simplify(std::vector< Node > &vec_node);