Refactor strings, remove old cycle checks in normalize eqc.

2 files changed, 1121 insertions, 1201 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 607552188..9899a7a48 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -799,8 +799,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
       }
     }
     Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
-    Trace("strings-pending-debug") << atom << std::endl;
-    Trace("strings-pending-debug") << Rewriter::rewrite( atom ) << std::endl;
     d_equalityEngine.assertEquality( atom, polarity, exp );
     Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
   } else {
@@ -874,118 +872,911 @@ void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
   }
 }
 
-bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
-  std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
+void TheoryStrings::checkInit() {
+  //build term index
+  d_eqc_to_const.clear();
+  d_eqc_to_const_base.clear();
+  d_eqc_to_const_exp.clear();
+  d_eqc_to_len_term.clear();
+  d_term_index.clear();
+  d_strings_eqc.clear();
+
+  std::map< Kind, unsigned > ncongruent;
+  std::map< Kind, unsigned > congruent;
+  d_emptyString_r = getRepresentative( d_emptyString );
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    TypeNode tn = eqc.getType();
+    if( !tn.isRegExp() ){
+      if( tn.isString() ){
+        d_strings_eqc.push_back( eqc );
+      }
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+      while( !eqc_i.isFinished() ) {
+        Node n = *eqc_i;
+        if( tn.isInteger() ){
+          if( n.getKind()==kind::STRING_LENGTH ){
+            Node nr = getRepresentative( n[0] );
+            d_eqc_to_len_term[nr] = n[0];
+          }
+        }else if( n.isConst() ){
+          d_eqc_to_const[eqc] = n;
+          d_eqc_to_const_base[eqc] = n;
+          d_eqc_to_const_exp[eqc] = Node::null();
+        }else if( n.getNumChildren()>0 ){
+          Kind k = n.getKind();
+          if( k!=kind::EQUAL ){
+            if( d_congruent.find( n )==d_congruent.end() ){
+              std::vector< Node > c;
+              Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c );
+              if( nc!=n ){
+                //check if we have inferred a new equality by removal of empty components
+                if( n.getKind()==kind::STRING_CONCAT && !areEqual( nc, n ) ){
+                  std::vector< Node > exp;
+                  unsigned count[2] = { 0, 0 };
+                  while( count[0]<nc.getNumChildren() || count[1]<n.getNumChildren() ){
+                    //explain empty prefixes
+                    for( unsigned t=0; t<2; t++ ){
+                      Node nn = t==0 ? nc : n;
+                      while( count[t]<nn.getNumChildren() &&
+                            ( nn[count[t]]==d_emptyString || areEqual( nn[count[t]], d_emptyString ) ) ){
+                        if( nn[count[t]]!=d_emptyString ){
+                          exp.push_back( nn[count[t]].eqNode( d_emptyString ) );
+                        }
+                        count[t]++;
+                      }
+                    }
+                    //explain equal components
+                    if( count[0]<nc.getNumChildren() ){
+                      Assert( count[1]<n.getNumChildren() );
+                      if( nc[count[0]]!=n[count[1]] ){
+                        exp.push_back( nc[count[0]].eqNode( n[count[1]] ) );
+                      }
+                      count[0]++;
+                      count[1]++;
+                    }
+                  }
+                  //infer the equality
+                  sendInfer( mkAnd( exp ), n.eqNode( nc ), "I_Norm" );
+                }else{
+                  //update the extf map : only process if neither has been reduced
+                  NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
+                  if( it!=d_ext_func_terms.end() ){
+                    if( d_ext_func_terms.find( nc )==d_ext_func_terms.end() ){
+                      d_ext_func_terms[nc] = (*it).second;
+                    }else{
+                      d_ext_func_terms[nc] = d_ext_func_terms[nc] && (*it).second;
+                    }
+                    d_ext_func_terms[n] = false;
+                  }
+                }
+                //this node is congruent to another one, we can ignore it
+                Trace("strings-process-debug") << "  congruent term : " << n << std::endl;
+                d_congruent.insert( n );
+                congruent[k]++;
+              }else if( k==kind::STRING_CONCAT && c.size()==1 ){
+                Trace("strings-process-debug") << "  congruent term by singular : " << n << " " << c[0] << std::endl;
+                //singular case
+                if( !areEqual( c[0], n ) ){
+                  std::vector< Node > exp;
+                  //explain empty components
+                  bool foundNEmpty = false;
+                  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+                    if( areEqual( n[i], d_emptyString ) ){
+                      if( n[i]!=d_emptyString ){
+                        exp.push_back( n[i].eqNode( d_emptyString ) );
+                      }
+                    }else{
+                      Assert( !foundNEmpty );
+                      if( n[i]!=c[0] ){
+                        exp.push_back( n[i].eqNode( c[0] ) );
+                      }
+                      foundNEmpty = true;
+                    }
+                  }
+                  AlwaysAssert( foundNEmpty );
+                  //infer the equality
+                  sendInfer( mkAnd( exp ), n.eqNode( c[0] ), "I_Norm_S" );
+                }
+                d_congruent.insert( n );
+                congruent[k]++;
+              }else{
+                ncongruent[k]++;
+              }
+            }else{
+              congruent[k]++;
+            }
+          }
+        }
+        ++eqc_i;
+      }
+    }
+    ++eqcs_i;
+  }
+  if( Trace.isOn("strings-process") ){
+    for( std::map< Kind, TermIndex >::iterator it = d_term_index.begin(); it != d_term_index.end(); ++it ){
+      Trace("strings-process") << "  Terms[" << it->first << "] = " << ncongruent[it->first] << "/" << (congruent[it->first]+ncongruent[it->first]) << std::endl;
+    }
+  }
+  Trace("strings-process") << "Done check init, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+  //now, infer constants for equivalence classes
+  if( !hasProcessed() ){
+    //do fixed point
+    unsigned prevSize;
+    do{
+      Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl;
+      prevSize = d_eqc_to_const.size();
+      std::vector< Node > vecc;
+      checkConstantEquivalenceClasses( &d_term_index[kind::STRING_CONCAT], vecc );
+    }while( !hasProcessed() && d_eqc_to_const.size()>prevSize );
+    Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+  }
+}
+
+void TheoryStrings::checkExtendedFuncsEval( int effort ) {
+  Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
+  if( effort==0 ){
+    d_extf_vars.clear();
+  }
+  d_extf_pol.clear();
+  d_extf_exp.clear();
+  d_extf_info.clear();
+  Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
+  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+    if( (*it).second ){
+      Node n = (*it).first;
+      d_extf_pol[n] = 0;
+      if( n.getType().isBoolean() ){
+        if( areEqual( n, d_true ) ){
+          d_extf_pol[n] = 1;
+        }else if( areEqual( n, d_false ) ){
+          d_extf_pol[n] = -1;
+        }
+      }
+      Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << d_extf_pol[n] << "..." << std::endl;
+      if( effort==0 ){
+        std::map< Node, bool > visited;
+        collectVars( n, d_extf_vars[n], visited );
+      }
+      //build up a best current substitution for the variables in the term, exp is explanation for substitution
+      std::vector< Node > var;
+      std::vector< Node > sub;
+      for( std::map< Node, std::vector< Node > >::iterator itv = d_extf_vars[n].begin(); itv != d_extf_vars[n].end(); ++itv ){
+        Node nr = itv->first;
+        std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
+        Node s;
+        Node b;
+        Node e;
+        if( itc!=d_eqc_to_const.end() ){
+          b = d_eqc_to_const_base[nr];
+          s = itc->second;
+          e = d_eqc_to_const_exp[nr];
+        }else if( effort>0 ){
+          b = d_normal_forms_base[nr];
+          std::vector< Node > expt;
+          s = getNormalString( b, expt );
+          e = mkAnd( expt );
+        }
+        if( !s.isNull() ){
+          bool added = false;
+          for( unsigned i=0; i<itv->second.size(); i++ ){
+            if( itv->second[i]!=s ){
+              var.push_back( itv->second[i] );
+              sub.push_back( s );
+              addToExplanation( itv->second[i], b, d_extf_exp[n] );
+              Trace("strings-extf-debug") << "  " << itv->second[i] << " --> " << s << std::endl;
+              added = true;
+            }
+          }
+          if( added ){
+            addToExplanation( e, d_extf_exp[n] );
+          }
+        }
+      }
+      Node to_reduce;
+      if( !var.empty() ){
+        Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() );
+        Node nrc = Rewriter::rewrite( nr );
+        if( nrc.isConst() ){
+          //mark as reduced
+          d_ext_func_terms[n] = false;
+          Trace("strings-extf-debug") << "  resolvable by evaluation..." << std::endl;
+          std::vector< Node > exps;
+          Trace("strings-extf-debug") << "  get symbolic definition..." << std::endl;
+          Node nrs = getSymbolicDefinition( nr, exps );
+          if( !nrs.isNull() ){
+            Trace("strings-extf-debug") << "  rewrite " << nrs << "..." << std::endl;
+            nrs = Rewriter::rewrite( nrs );
+            //ensure the symbolic form is non-trivial
+            if( nrs.isConst() ){
+              Trace("strings-extf-debug") << "  symbolic definition is trivial..." << std::endl;
+              nrs = Node::null();
+            }
+          }else{
+            Trace("strings-extf-debug") << "  could not infer symbolic definition." << std::endl;
+          }
+          Node conc;
+          if( !nrs.isNull() ){
+            Trace("strings-extf-debug") << "  symbolic def : " << nrs << std::endl;
+            if( !areEqual( nrs, nrc ) ){
+              //infer symbolic unit
+              if( n.getType().isBoolean() ){
+                conc = nrc==d_true ? nrs : nrs.negate();
+              }else{
+                conc = nrs.eqNode( nrc );
+              }
+              d_extf_exp[n].clear();
+            }
+          }else{
+            if( !areEqual( n, nrc ) ){
+              if( n.getType().isBoolean() ){
+                d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n );
+                conc = d_false;
+              }else{
+                conc = n.eqNode( nrc );
+              }
+            }
+          }
+          if( !conc.isNull() ){
+            Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << std::endl;
+            if( n.getType().isInteger() || d_extf_exp[n].empty() ){
+              sendLemma( mkExplain( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" );
+            }else{
+              sendInfer( mkAnd( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" );
+            }
+            if( d_conflict ){
+              Trace("strings-extf-debug") << "  conflict, return." << std::endl;
+              return;
+            }
+          }
+        }else if( ( nrc.getKind()==kind::OR && d_extf_pol[n]==-1 ) || ( nrc.getKind()==kind::AND && d_extf_pol[n]==1 ) ){
+          //infer the consequence of each
+          d_ext_func_terms[n] = false;
+          d_extf_exp[n].push_back( d_extf_pol[n]==-1 ? n.negate() : n );
+          Trace("strings-extf-debug") << "  decomposable..." << std::endl;
+          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl;
+          for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
+            sendInfer( mkAnd( d_extf_exp[n] ), d_extf_pol[n]==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+          }
+        }else{
+          to_reduce = nrc;
+        }
+      }else{
+        to_reduce = n;
+      }
+      if( !to_reduce.isNull() ){
+        if( effort==1 ){
+          Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
+        }
+        checkExtfInference( n, to_reduce, effort );
+        if( Trace.isOn("strings-extf-list") ){
+          Trace("strings-extf-list") << "  * " << to_reduce;
+          if( d_extf_pol[n]!=0 ){
+            Trace("strings-extf-list") << ", pol = " << d_extf_pol[n];
+          }
+          if( n!=to_reduce ){
+            Trace("strings-extf-list") << ", from " << n;
+          }
+          Trace("strings-extf-list") << std::endl;
+        }
+      }
+    }else{
+      Trace("strings-extf-debug")  << "  already reduced " << (*it).first << std::endl;
+    }
+  }
+}
+
+void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
+  int n_pol = d_extf_pol[n];
+  if( n_pol!=0 ){
+    //add original to explanation
+    d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() );
+    if( nr.getKind()==kind::STRING_STRCTN ){
+      if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
+        if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
+          d_extf_infer_cache.insert( nr );
+          //one argument does (not) contain each of the components of the other argument
+          int index = n_pol==1 ? 1 : 0;
+          std::vector< Node > children;
+          children.push_back( nr[0] );
+          children.push_back( nr[1] );
+          Node exp_n = mkAnd( d_extf_exp[n] );
+          for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){
+            children[index] = nr[index][i];
+            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children );
+            //can mark as reduced, since model for n => model for conc
+            d_ext_func_terms[conc] = false;
+            sendInfer( exp_n, n_pol==1 ? conc : conc.negate(), "CTN_Decompose" );
+          }
+        }
+      }else{
+        //store this (reduced) assertion
+        //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
+        bool pol = n_pol==1;
+        if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
+          Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
+          d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] );
+          d_extf_info[nr[0]].d_ctn_from[pol].push_back( n );
+          //transitive closure for contains
+          bool opol = !pol;
+          for( unsigned i=0; i<d_extf_info[nr[0]].d_ctn[opol].size(); i++ ){
+            Node onr = d_extf_info[nr[0]].d_ctn[opol][i];
+            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ).negate();
+            std::vector< Node > exp;
+            exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
+            Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
+            Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
+            exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
+            sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
+          }
+        }else{
+          Trace("strings-extf-debug") << "  redundant." << std::endl;
+          d_ext_func_terms[n] = false;
+        }
+      }
+    }
+  }
+}
+
+void TheoryStrings::collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ) {
+  if( !n.isConst() ){
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      if( n.getNumChildren()>0 ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          collectVars( n[i], vars, visited );
+        }
+      }else{
+        Node nr = getRepresentative( n );
+        vars[nr].push_back( n );
+      }
+    }
+  }
+}
+
+Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) {
+  if( n.getNumChildren()==0 ){
+    NodeNodeMap::const_iterator it = d_proxy_var.find( n );
+    if( it==d_proxy_var.end() ){
+      return Node::null();
+    }else{
+      Node eq = n.eqNode( (*it).second );
+      eq = Rewriter::rewrite( eq );
+      if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
+        exp.push_back( eq );
+      }
+      return (*it).second;
+    }
+  }else{
+    std::vector< Node > children;
+    if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      children.push_back( n.getOperator() );
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n.getKind()==kind::STRING_IN_REGEXP && i==1 ){
+        children.push_back( n[i] );
+      }else{
+        Node ns = getSymbolicDefinition( n[i], exp );
+        if( ns.isNull() ){
+          return Node::null();
+        }else{
+          children.push_back( ns );
+        }
+      }
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }
+}
+
+
+void TheoryStrings::debugPrintFlatForms( const char * tc ){
+  for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
+    Node eqc = d_strings_eqc[k];
+    if( d_eqc[eqc].size()>1 ){
+      Trace( tc ) << "EQC [" << eqc << "]" << std::endl;
+    }else{
+      Trace( tc ) << "eqc [" << eqc << "]";
+    }
+    std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
+    if( itc!=d_eqc_to_const.end() ){
+      Trace( tc ) << "  C: " << itc->second;
+      if( d_eqc[eqc].size()>1 ){
+        Trace( tc ) << std::endl;
+      }
+    }
+    if( d_eqc[eqc].size()>1 ){
+      for( unsigned i=0; i<d_eqc[eqc].size(); i++ ){
+        Node n = d_eqc[eqc][i];
+        Trace( tc ) << "    ";
+        for( unsigned j=0; j<d_flat_form[n].size(); j++ ){
+          Node fc = d_flat_form[n][j];
+          itc = d_eqc_to_const.find( fc );
+          Trace( tc ) << " ";
+          if( itc!=d_eqc_to_const.end() ){
+            Trace( tc ) << itc->second;
+          }else{
+            Trace( tc ) << fc;
+          }
+        }
+        if( n!=eqc ){
+          Trace( tc ) << ", from " << n;
+        }
+        Trace( tc ) << std::endl;
+      }
+    }else{
+      Trace( tc ) << std::endl;
+    }
+  }
+  Trace( tc ) << std::endl;
+}
+
+void TheoryStrings::checkFlatForms() {
+  //first check for cycles, while building ordering of equivalence classes
+  d_eqc.clear();
+  d_flat_form.clear();
+  d_flat_form_index.clear();
+  Trace("strings-process") << "Check equivalence classes cycles...." << std::endl;
+  //rebuild strings eqc based on acyclic ordering
+  std::vector< Node > eqc;
+  eqc.insert( eqc.end(), d_strings_eqc.begin(), d_strings_eqc.end() );
+  d_strings_eqc.clear();
+  for( unsigned i=0; i<eqc.size(); i++ ){
+    std::vector< Node > curr;
+    std::vector< Node > exp;
+    checkCycles( eqc[i], curr, exp );
+    if( hasProcessed() ){
+      return;
+    }
+  }
+  Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << std::endl;
+  if( !hasProcessed() ){
+    //debug print flat forms
+    if( Trace.isOn("strings-ff") ){
+      Trace("strings-ff") << "Flat forms : " << std::endl;
+      debugPrintFlatForms( "strings-ff" );
+    }
+    //inferences without recursively expanding flat forms
+    for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
+      Node eqc = d_strings_eqc[k];
+      Node c;
+      std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
+      if( itc!=d_eqc_to_const.end() ){
+        c = itc->second;   //use?
+      }
+      std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc );
+      if( it!=d_eqc.end() && it->second.size()>1 ){
+        //iterate over start index
+        for( unsigned start=0; start<it->second.size()-1; start++ ){
+          for( unsigned r=0; r<2; r++ ){
+            unsigned count = 0;
+            std::vector< Node > inelig;
+            for( unsigned i=0; i<=start; i++ ){
+              inelig.push_back( it->second[start] );
+            }
+            Node a = it->second[start];
+            Node b;
+            do{
+              std::vector< Node > exp;
+              //std::vector< Node > exp_n;
+              Node conc;
+              int inf_type = -1;
+              if( count==d_flat_form[a].size() ){
+                for( unsigned i=start+1; i<it->second.size(); i++ ){
+                  b = it->second[i];
+                  if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
+                    if( count<d_flat_form[b].size() ){
+                      //endpoint
+                      std::vector< Node > conc_c;
+                      for( unsigned j=count; j<d_flat_form[b].size(); j++ ){
+                        conc_c.push_back( b[d_flat_form_index[b][j]].eqNode( d_emptyString ) );
+                      }
+                      Assert( !conc_c.empty() );
+                      conc = mkAnd( conc_c );
+                      inf_type = 2;
+                      Assert( count>0 );
+                      //swap, will enforce is empty past current
+                      a = it->second[i]; b = it->second[start];
+                      count--;
+                      break;
+                    }
+                    inelig.push_back( it->second[i] );
+                  }
+                }
+              }else{
+                Node curr = d_flat_form[a][count];
+                Node curr_c = d_eqc_to_const[curr];
+                std::vector< Node > lexp;
+                Node lcurr = getLength( curr, lexp );
+                for( unsigned i=1; i<it->second.size(); i++ ){
+                  b = it->second[i];
+                  if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
+                    if( count==d_flat_form[b].size() ){
+                      inelig.push_back( b );
+                      //endpoint
+                      std::vector< Node > conc_c;
+                      for( unsigned j=count; j<d_flat_form[a].size(); j++ ){
+                        conc_c.push_back( a[d_flat_form_index[a][j]].eqNode( d_emptyString ) );
+                      }
+                      Assert( !conc_c.empty() );
+                      conc = mkAnd( conc_c );
+                      inf_type = 2;
+                      Assert( count>0 );
+                      count--;
+                      break;
+                    }else{
+                      Node cc = d_flat_form[b][count];
+                      if( cc!=curr ){
+                        Node ac = a[d_flat_form_index[a][count]];
+                        Node bc = b[d_flat_form_index[b][count]];
+                        inelig.push_back( b );
+                        Assert( !areEqual( curr, cc ) );
+                        Node cc_c = d_eqc_to_const[cc];
+                        if( !curr_c.isNull() && !cc_c.isNull() ){
+                          //check for constant conflict
+                          int index;
+                          Node s = TheoryStringsRewriter::splitConstant( cc_c, curr_c, index, r==1 );
+                          if( s.isNull() ){
+                            addToExplanation( ac, d_eqc_to_const_base[curr], exp );
+                            addToExplanation( d_eqc_to_const_exp[curr], exp );
+                            addToExplanation( bc, d_eqc_to_const_base[cc], exp );
+                            addToExplanation( d_eqc_to_const_exp[cc], exp );
+                            conc = d_false;
+                            inf_type = 0;
+                            break;
+                          }
+                        }else if( (d_flat_form[a].size()-1)==count && (d_flat_form[b].size()-1)==count ){
+                          conc = ac.eqNode( bc );
+                          inf_type = 3;
+                          break;
+                        }else{
+                          //if lengths are the same, apply LengthEq
+                          Node lcc = getLength( cc, lexp );
+                          if( areEqual( lcurr, lcc ) ){
+                            Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
+                            //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
+                            exp.insert( exp.end(), lexp.begin(), lexp.end() );
+                            addToExplanation( lcurr, lcc, exp );
+                            conc = ac.eqNode( bc );
+                            inf_type = 1;
+                            break;
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+              if( !conc.isNull() ){
+                Trace("strings-ff-debug") << "Found inference : " << conc << " based on equality " << a << " == " << b << " " << r << " " << inf_type << std::endl;
+                addToExplanation( a, b, exp );
+                //explain why prefixes up to now were the same
+                for( unsigned j=0; j<count; j++ ){
+                  Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " " << d_flat_form_index[b][j] << std::endl;
+                  addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp );
+                }
+                //explain why other components up to now are empty
+                for( unsigned t=0; t<2; t++ ){
+                  Node c = t==0 ? a : b;
+                  int jj = t==0 ? d_flat_form_index[a][count] : ( inf_type==2 ? ( r==0 ? c.getNumChildren() : -1 ) : d_flat_form_index[b][count] );
+                  if( r==0 ){
+                    for( int j=0; j<jj; j++ ){
+                      if( areEqual( c[j], d_emptyString ) ){
+                        addToExplanation( c[j], d_emptyString, exp );
+                      }
+                    }
+                  }else{
+                    for( int j=(c.getNumChildren()-1); j>jj; --j ){
+                      if( areEqual( c[j], d_emptyString ) ){
+                        addToExplanation( c[j], d_emptyString, exp );
+                      }
+                    }
+                  }
+                }
+                //if( exp_n.empty() ){
+                sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
+                //}else{
+                //}
+                if( d_conflict ){
+                  return;
+                }else{
+                  break;
+                }
+              }
+              count++;
+            }while( inelig.size()<it->second.size() );
+
+            for( unsigned i=0; i<it->second.size(); i++ ){
+              std::reverse( d_flat_form[it->second[i]].begin(), d_flat_form[it->second[i]].end() );
+              std::reverse( d_flat_form_index[it->second[i]].begin(), d_flat_form_index[it->second[i]].end() );
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
+  if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
+    // a loop
+    return eqc;
+  }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){
+    curr.push_back( eqc );
+    //look at all terms in this equivalence class
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ) {
+      Node n = (*eqc_i);
+      if( d_congruent.find( n )==d_congruent.end() ){
+        Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
+        if( n.getKind() == kind::STRING_CONCAT ) {
+          if( eqc!=d_emptyString_r ){
+            d_eqc[eqc].push_back( n );
+          }
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            Node nr = getRepresentative( n[i] );
+            if( eqc==d_emptyString_r ){
+              //for empty eqc, ensure all components are empty
+              if( nr!=d_emptyString_r ){
+                sendInfer( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "I_CYCLE_E" );
+                return Node::null();
+              }
+            }else{
+              if( nr!=d_emptyString_r ){
+                d_flat_form[n].push_back( nr );
+                d_flat_form_index[n].push_back( i );
+              }
+              //for non-empty eqc, recurse and see if we find a loop
+              Node ncy = checkCycles( nr, curr, exp );
+              if( !ncy.isNull() ){
+                Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
+                addToExplanation( n, eqc, exp );
+                addToExplanation( nr, n[i], exp );
+                if( ncy==eqc ){
+                  //can infer all other components must be empty
+                  for( unsigned j=0; j<n.getNumChildren(); j++ ){
+                    //take first non-empty
+                    if( j!=i && !areEqual( n[j], d_emptyString ) ){
+                      sendInfer( mkAnd( exp ), n[j].eqNode( d_emptyString ), "I_CYCLE" );
+                      return Node::null();
+                    }
+                  }
+                  Trace("strings-error") << "Looping term should be congruent : " << n << " " << eqc << " " << ncy << std::endl;
+                  //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
+                  Assert( false );
+                }else{
+                  return ncy;
+                }
+              }else{
+                if( hasProcessed() ){
+                  return Node::null();
+                }
+              }
+            }
+          }
+        }
+      }
+      ++eqc_i;
+    }
+    curr.pop_back();
+    //now we can add it to the list of equivalence classes
+    d_strings_eqc.push_back( eqc );
+  }else{
+    //already processed
+  }
+  return Node::null();
+}
+
+
+void TheoryStrings::checkNormalForms(){
+  // simple extended func reduction
+  Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl;
+  checkExtfReduction( 1 );
+  Trace("strings-process") << "Done check extended function reduction" << std::endl;
+  if( !hasProcessed() ){
+    Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
+    //calculate normal forms for each equivalence class, possibly adding splitting lemmas
+    d_normal_forms.clear();
+    d_normal_forms_exp.clear();
+    std::map< Node, Node > nf_to_eqc;
+    std::map< Node, Node > eqc_to_exp;
+    for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
+      Node eqc = d_strings_eqc[i];
+      Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
+      std::vector< Node > nf;
+      std::vector< Node > nf_exp;
+      normalizeEquivalenceClass( eqc, nf, nf_exp );
+      Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
+      if( hasProcessed() ){
+        return;
+      }else{
+        Node nf_term = mkConcat( nf );
+        if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
+          //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
+          //two equivalence classes have same normal form, merge
+          nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
+          Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
+          sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
+        } else {
+          nf_to_eqc[nf_term] = eqc;
+          eqc_to_exp[eqc] = mkAnd( nf_exp );
+        }
+      }
+      Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
+    }
+
+    if(Trace.isOn("strings-nf")) {
+      Trace("strings-nf") << "**** Normal forms are : " << std::endl;
+      for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
+        Trace("strings-nf") << "  N[" << it->second << "] = " << it->first << std::endl;
+      }
+      Trace("strings-nf") << std::endl;
+    }
+    if( !hasProcessed() ){
+      checkExtendedFuncsEval( 1 );
+      Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+      if( !hasProcessed() ){
+        if( !options::stringEagerLen() ){
+          checkLengthsEqc();
+          if( hasProcessed() ){
+            return;
+          }
+        }
+        //process disequalities between equivalence classes
+        checkDeqNF();
+        Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+      }
+    }
+  }
+  Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
+}
+
+//nf_exp is conjunction
+bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
+  Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
+  if( areEqual( eqc, d_emptyString ) ) {
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ) {
+      Node n = (*eqc_i);
+      if( d_congruent.find( n )==d_congruent.end() ){
+        if( n.getKind()==kind::STRING_CONCAT ){
+          //std::vector< Node > exp;
+          //exp.push_back( n.eqNode( d_emptyString ) );
+          //Node ant = mkExplain( exp );
+          Node ant = n.eqNode( d_emptyString );
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            if( !areEqual( n[i], d_emptyString ) ){
+              //sendLemma( ant, n[i].eqNode( d_emptyString ), "CYCLE" );
+              sendInfer( ant, n[i].eqNode( d_emptyString ), "CYCLE" );
+            }
+          }
+        }
+      }
+      ++eqc_i;
+    }
+    //do nothing
+    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+    d_normal_forms_base[eqc] = d_emptyString;
+    d_normal_forms[eqc].clear();
+    d_normal_forms_exp[eqc].clear();
+    return true;
+  } else {
+    bool result;
+    if( d_normal_forms.find(eqc)==d_normal_forms.end() ){
+      //phi => t = s1 * ... * sn
+      // normal form for each non-variable term in this eqc (s1...sn)
+      std::vector< std::vector< Node > > normal_forms;
+      // explanation for each normal form (phi)
+      std::vector< std::vector< Node > > normal_forms_exp;
+      // record terms for each normal form (t)
+      std::vector< Node > normal_form_src;
+      //Get Normal Forms
+      result = getNormalForms(eqc, nf, normal_forms, normal_forms_exp, normal_form_src);
+      if( hasProcessed() ){
+          return true;
+      }else if( result ){
+        if( processNEqc(normal_forms, normal_forms_exp, normal_form_src) ){
+          return true;
+        }
+      }
+      //construct the normal form
+      if( normal_forms.empty() ){
+        Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
+        getConcatVec( eqc, nf );
+      }else{
+        Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
+        //just take the first normal form
+        nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
+        nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
+        if( eqc!=normal_form_src[0] ){
+          nf_exp.push_back( eqc.eqNode( normal_form_src[0] ) );
+        }
+        Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+      }
+
+      d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
+      d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
+      d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
+      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
+    }else{
+      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
+      nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
+      nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
+      result = true;
+    }
+    return result;
+  }
+}
+
+bool TheoryStrings::getNormalForms( Node &eqc, std::vector< Node > & nf,
+                                    std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, 
+                                    std::vector< Node > &normal_form_src) {
   Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
-  // EqcItr
   eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-  while( !eqc_i.isFinished() ) {
+  while( !eqc_i.isFinished() ){
     Node n = (*eqc_i);
     if( d_congruent.find( n )==d_congruent.end() ){
-      if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
+      if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ){
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
         std::vector<Node> nf_n;
         std::vector<Node> nf_exp_n;
-        bool result = true;
-        if( n.getKind() == kind::CONST_STRING  ) {
+        if( n.getKind()==kind::CONST_STRING ){
           if( n!=d_emptyString ) {
             nf_n.push_back( n );
           }
-        } else if( n.getKind() == kind::STRING_CONCAT ){
+        }else if( n.getKind()==kind::STRING_CONCAT ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ) {
             Node nr = d_equalityEngine.getRepresentative( n[i] );
             std::vector< Node > nf_temp;
             std::vector< Node > nf_exp_temp;
             Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
-            bool nresult = false;
-            if( nr==eqc ) {
-              nf_temp.push_back( nr );
-            } else {
-              nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
-              if( hasProcessed() ) {
-                return true;
-              }
-            }
-            //successfully computed normal form
-            if( nf.size()!=1 || nf[0]!=d_emptyString ) {
-              if( Trace.isOn("strings-error") ) {
-                for( unsigned r=0; r<nf_temp.size(); r++ ) {
-                  if( nresult && nf_temp[r].getKind()==kind::STRING_CONCAT ) {
+            Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
+            nf_temp.insert( nf_temp.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
+            nf_exp_temp.insert( nf_exp_temp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
+            //if not the empty string, add to current normal form
+            if( nf.size()!=1 || nf[0]!=d_emptyString ){
+              for( unsigned r=0; r<nf_temp.size(); r++ ) {
+                if( Trace.isOn("strings-error") ) {
+                  if( nf_temp[r].getKind()==kind::STRING_CONCAT ){
                     Trace("strings-error") << "Strings::Error: From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
                     for( unsigned rr=0; rr<nf_temp.size(); rr++ ) {
                       Trace("strings-error") << nf_temp[rr] << " ";
                     }
                     Trace("strings-error") << std::endl;
                   }
-                  Assert( !nresult || nf_temp[r].getKind()!=kind::STRING_CONCAT );
                 }
+                Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
               }
               nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() );
             }
             nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() );
-            if( nr!=n[i] ) {
+            if( nr!=n[i] ){
               nf_exp_n.push_back( n[i].eqNode( nr ) );
             }
-            if( !nresult ) {
-              //Trace("strings-process-debug") << "....Caused already asserted
-              for( unsigned j=i+1; j<n.getNumChildren(); j++ ) {
-                if( !areEqual( n[j], d_emptyString ) ) {
-                  nf_n.push_back( n[j] );
-                }
-              }
-              if( nf_n.size()>1 ) {
-                result = false;
-                break;
-              }
-            }
           }
         }
         //if not equal to self
         //if( nf_n.size()!=1 || (nf_n.size()>1 && nf_n[0]!=eqc ) ){
-        if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) {
+        if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
           if( nf_n.size()>1 ) {
-            Trace("strings-process-debug") << "Check for cycle lemma for normal form ";
-            printConcat(nf_n,"strings-process-debug");
-            Trace("strings-process-debug") << "..." << std::endl;
-            for( unsigned i=0; i<nf_n.size(); i++ ) {
-              //if a component is equal to whole,
-              if( areEqual( nf_n[i], n ) ){
-                //all others must be empty
-                std::vector< Node > ant;
-                if( nf_n[i]!=n ){
-                  ant.push_back( nf_n[i].eqNode( n ) );
-                }
-                ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
-                std::vector< Node > cc;
-                for( unsigned j=0; j<nf_n.size(); j++ ){
-                  if( i!=j ){
-                    cc.push_back( nf_n[j].eqNode( d_emptyString ) );
-                  }
-                }
-                std::vector< Node > empty_vec;
-                Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
-                conc = Rewriter::rewrite( conc );
-                sendInfer( mkAnd( ant ), conc, "CYCLE" );
-                return true;
+            for( unsigned i=0; i<nf_n.size(); i++ ){
+              if( Trace.isOn("strings-error") ){
+                Trace("strings-error") << "Cycle for normal form ";
+                printConcat(nf_n,"strings-error");
+                Trace("strings-error") << "..." << nf_n[i] << std::endl;
               }
+              Assert( !areEqual( nf_n[i], n ) );
             }
           }
-          if( !result ) {
-            Trace("strings-process-debug") << "Will have cycle lemma at higher level!" << std::endl;
-            //we have a normal form that will cause a component lemma at a higher level
-            normal_forms.clear();
-            normal_forms_exp.clear();
-            normal_form_src.clear();
-          }
           normal_forms.push_back(nf_n);
           normal_forms_exp.push_back(nf_exp_n);
           normal_form_src.push_back(n);
-          if( !result ) {
-            return false;
-          }
-        } else {
+        }else{
+          //this was redundant: combination of eqc + empty string(s)
           Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
+          Assert( areEqual( nn, eqc ) );
           //Assert( areEqual( nf_n[0], eqc ) );
+          /*
           if( !areEqual( nn, eqc ) ){
             std::vector< Node > ant;
             ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
@@ -994,6 +1785,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
             sendInfer( mkAnd( ant ), conc, "CYCLE-T" );
             return true;
           }
+          */
         }
         //}
       }
@@ -1001,13 +1793,11 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
     ++eqc_i;
   }
 
-  // Test the result
   if(Trace.isOn("strings-solve")) {
     if( !normal_forms.empty() ) {
       Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
       for( unsigned i=0; i<normal_forms.size(); i++ ) {
         Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
-        //mergeCstVec(normal_forms[i]);
         for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
           if(j>0) {
             Trace("strings-solve") << ", ";
@@ -1041,236 +1831,9 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
   return true;
 }
 
-void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
-  std::vector< Node >::iterator itr = vec_strings.begin();
-  while(itr != vec_strings.end()) {
-    if(itr->isConst()) {
-      std::vector< Node >::iterator itr2 = itr + 1;
-      if(itr2 == vec_strings.end()) {
-        break;
-      } else if(itr2->isConst()) {
-        CVC4::String s1 = itr->getConst<String>();
-        CVC4::String s2 = itr2->getConst<String>();
-        *itr = NodeManager::currentNM()->mkConst(s1.concat(s2));
-        vec_strings.erase(itr2);
-      } else {
-        ++itr;
-      }
-    } else {
-      ++itr;
-    }
-  }
-}
-
-bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
-  int i, int j, int index_i, int index_j,
-  int &loop_in_i, int &loop_in_j) {
-  int has_loop[2] = { -1, -1 };
-  if( options::stringLB() != 2 ) {
-    for( unsigned r=0; r<2; r++ ) {
-      int index = (r==0 ? index_i : index_j);
-      int other_index = (r==0 ? index_j : index_i );
-      int n_index = (r==0 ? i : j);
-      int other_n_index = (r==0 ? j : i);
-      if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
-        for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
-          if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
-            has_loop[r] = lp;
-            break;
-          }
-        }
-      }
-    }
-  }
-  if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
-    loop_in_i = has_loop[0];
-    loop_in_j = has_loop[1];
-    return true;
-  } else {
-    return false;
-  }
-}
-//xs(zy)=t(yz)xr
-bool TheoryStrings::processLoop(std::vector< Node > &antec,
-  std::vector< std::vector< Node > > &normal_forms,
-  std::vector< Node > &normal_form_src,
-  int i, int j, int loop_n_index, int other_n_index,
-  int loop_index, int index, int other_index) {
-  Node conc;
-  Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
-  Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
-
-  Trace("strings-loop") << " ... T(Y.Z)= ";
-  std::vector< Node > vec_t;
-  for(int lp=index; lp<loop_index; ++lp) {
-    if(lp != index) Trace("strings-loop") << " ++ ";
-    Trace("strings-loop") << normal_forms[loop_n_index][lp];
-    vec_t.push_back( normal_forms[loop_n_index][lp] );
-  }
-  Node t_yz = mkConcat( vec_t );
-  Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
-  Trace("strings-loop") << " ... S(Z.Y)= ";
-  std::vector< Node > vec_s;
-  for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
-    if(lp != other_index+1) Trace("strings-loop") << " ++ ";
-    Trace("strings-loop") << normal_forms[other_n_index][lp];
-    vec_s.push_back( normal_forms[other_n_index][lp] );
-  }
-  Node s_zy = mkConcat( vec_s );
-  Trace("strings-loop") << " (" << s_zy << ")" << std::endl;
-  Trace("strings-loop") << " ... R= ";
-  std::vector< Node > vec_r;
-  for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
-    if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
-    Trace("strings-loop") << normal_forms[loop_n_index][lp];
-    vec_r.push_back( normal_forms[loop_n_index][lp] );
-  }
-  Node r = mkConcat( vec_r );
-  Trace("strings-loop") << " (" << r << ")" << std::endl;
-
-  //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
-  //TODO: can be more general
-  if( s_zy.isConst() && r.isConst() && r != d_emptyString) {
-    int c;
-    bool flag = true;
-    if(s_zy.getConst<String>().tailcmp( r.getConst<String>(), c ) ) {
-      if(c >= 0) {
-        s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, c) );
-        r = d_emptyString;
-        vec_r.clear();
-        Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl;
-        flag = false;
-      }
-    }
-    if(flag) {
-      Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl;
-      sendLemma( mkExplain( antec ), conc, "Loop Conflict" );
-      return true;
-    }
-  }
-
-  //require that x is non-empty
-  if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
-    //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
-    sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Len-Split(Loop-X)" );
-  } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING  ) {
-    //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
-    sendSplit( t_yz, d_emptyString, "Len-Split(Loop-YZ)" );
-  } else {
-    //need to break
-    antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
-    if( t_yz.getKind()!=kind::CONST_STRING ) {
-      antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
-    }
-    Node ant = mkExplain( antec );
-    if(d_loop_antec.find(ant) == d_loop_antec.end()) {
-      d_loop_antec.insert(ant);
-
-      Node str_in_re;
-      if( s_zy == t_yz &&
-        r == d_emptyString &&
-        s_zy.isConst() &&
-        s_zy.getConst<String>().isRepeated()
-        ) {
-        Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
-        Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
-        Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
-        //special case
-        str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
-                NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
-                NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
-        conc = str_in_re;
-      } else if(t_yz.isConst()) {
-        Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl;
-        CVC4::String s = t_yz.getConst< CVC4::String >();
-        unsigned size = s.size();
-        std::vector< Node > vconc;
-        for(unsigned len=1; len<=size; len++) {
-          Node y = NodeManager::currentNM()->mkConst(s.substr(0, len));
-          Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len));
-          Node restr = s_zy;
-          Node cc;
-          if(r != d_emptyString) {
-            std::vector< Node > v2(vec_r);
-            v2.insert(v2.begin(), y);
-            v2.insert(v2.begin(), z);
-            restr = mkConcat( z, y );
-            cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) ));
-          } else {
-            cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( z, y) ));
-          }
-          if(cc == d_false) {
-            continue;
-          }
-          Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
-                  NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-                    NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
-                    NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
-                      NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr))));
-          cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 );
-          d_regexp_ant[conc2] = ant;
-          vconc.push_back(cc);
-        }
-        conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc);
-      } else {
-        Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl;
-        //right
-        Node sk_w= mkSkolemS( "w_loop" );
-        Node sk_y= mkSkolemS( "y_loop", 1 );
-        Node sk_z= mkSkolemS( "z_loop" );
-        //t1 * ... * tn = y * z
-        Node conc1 = t_yz.eqNode( mkConcat( sk_y, sk_z ) );
-        // s1 * ... * sk = z * y * r
-        vec_r.insert(vec_r.begin(), sk_y);
-        vec_r.insert(vec_r.begin(), sk_z);
-        Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
-        Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
-        Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
-        str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
-                NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
-                  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, restr ) ) );
-
-        std::vector< Node > vec_conc;
-        vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3);
-        vec_conc.push_back(str_in_re);
-        //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
-        conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
-      } // normal case
-
-      //set its antecedant to ant, to say when it is relevant
-      if(!str_in_re.isNull()) {
-        d_regexp_ant[str_in_re] = ant;
-      }
-
-      sendLemma( ant, conc, "F-LOOP" );
-      ++(d_statistics.d_loop_lemmas);
 
-      //we will be done
-      addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-    } else {
-      Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant << " has already added." << std::endl;
-      addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-      return false;
-    }
-  }
-  return true;
-}
-Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit ){
-  //return mkSkolemS( c, isLenSplit );
-  std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( id );
-  if( it==d_skolem_cache[a][b].end() ){
-    Node sk = mkSkolemS( c, isLenSplit );
-    d_skolem_cache[a][b][id] = sk;
-    return sk;
-  }else{
-    return it->second;
-  }
-
-}
-
-bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms,
-  std::vector< std::vector< Node > > &normal_forms_exp,
-  std::vector< Node > &normal_form_src) {
+bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp,
+                                 std::vector< Node > &normal_form_src) {
   bool flag_lb = false;
   std::vector< Node > c_lb_exp;
   int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
@@ -1451,8 +2014,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
   return false;
 }
 
-bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms,
-  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
+bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, 
+                                       std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
   //reverse normal form of i, j
   std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
   std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
@@ -1470,9 +2033,8 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
   return ret;
 }
 
-bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
-  std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
-  unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
+bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
+                                      unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
   bool success;
   do {
     success = false;
@@ -1593,89 +2155,195 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
   return false;
 }
 
-
-//nf_exp is conjunction
-bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
-  Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
-  if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
-    getConcatVec( eqc, nf );
-    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
-    return false;
-  } else if( areEqual( eqc, d_emptyString ) ) {
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ) {
-      Node n = (*eqc_i);
-      if( d_congruent.find( n )==d_congruent.end() ){
-        if( n.getKind()==kind::STRING_CONCAT ){
-          //std::vector< Node > exp;
-          //exp.push_back( n.eqNode( d_emptyString ) );
-          //Node ant = mkExplain( exp );
-          Node ant = n.eqNode( d_emptyString );
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            if( !areEqual( n[i], d_emptyString ) ){
-              //sendLemma( ant, n[i].eqNode( d_emptyString ), "CYCLE" );
-              sendInfer( ant, n[i].eqNode( d_emptyString ), "CYCLE" );
-            }
+bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, 
+                                int index_i, int index_j, int &loop_in_i, int &loop_in_j) {
+  int has_loop[2] = { -1, -1 };
+  if( options::stringLB() != 2 ) {
+    for( unsigned r=0; r<2; r++ ) {
+      int index = (r==0 ? index_i : index_j);
+      int other_index = (r==0 ? index_j : index_i );
+      int n_index = (r==0 ? i : j);
+      int other_n_index = (r==0 ? j : i);
+      if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
+        for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
+          if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
+            has_loop[r] = lp;
+            break;
           }
         }
       }
-      ++eqc_i;
     }
-    //do nothing
-    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
-    d_normal_forms_base[eqc] = d_emptyString;
-    d_normal_forms[eqc].clear();
-    d_normal_forms_exp[eqc].clear();
+  }
+  if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
+    loop_in_i = has_loop[0];
+    loop_in_j = has_loop[1];
     return true;
   } else {
-    visited.push_back( eqc );
-    bool result;
-    if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
-      //phi => t = s1 * ... * sn
-      // normal form for each non-variable term in this eqc (s1...sn)
-      std::vector< std::vector< Node > > normal_forms;
-      // explanation for each normal form (phi)
-      std::vector< std::vector< Node > > normal_forms_exp;
-      // record terms for each normal form (t)
-      std::vector< Node > normal_form_src;
-      //Get Normal Forms
-      result = getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src);
-      if( hasProcessed() ) {
-          return true;
-      } else if( result ) {
-        if(processNEqc(normal_forms, normal_forms_exp, normal_form_src)) {
-          return true;
-        }
+    return false;
+  }
+}
+
+//xs(zy)=t(yz)xr
+bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+                                 int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, int other_index) {
+  Node conc;
+  Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
+  Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
+
+  Trace("strings-loop") << " ... T(Y.Z)= ";
+  std::vector< Node > vec_t;
+  for(int lp=index; lp<loop_index; ++lp) {
+    if(lp != index) Trace("strings-loop") << " ++ ";
+    Trace("strings-loop") << normal_forms[loop_n_index][lp];
+    vec_t.push_back( normal_forms[loop_n_index][lp] );
+  }
+  Node t_yz = mkConcat( vec_t );
+  Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
+  Trace("strings-loop") << " ... S(Z.Y)= ";
+  std::vector< Node > vec_s;
+  for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
+    if(lp != other_index+1) Trace("strings-loop") << " ++ ";
+    Trace("strings-loop") << normal_forms[other_n_index][lp];
+    vec_s.push_back( normal_forms[other_n_index][lp] );
+  }
+  Node s_zy = mkConcat( vec_s );
+  Trace("strings-loop") << " (" << s_zy << ")" << std::endl;
+  Trace("strings-loop") << " ... R= ";
+  std::vector< Node > vec_r;
+  for(int lp=loop_index+1; lp<(int)normal_forms[loop_n_index].size(); ++lp) {
+    if(lp != loop_index+1) Trace("strings-loop") << " ++ ";
+    Trace("strings-loop") << normal_forms[loop_n_index][lp];
+    vec_r.push_back( normal_forms[loop_n_index][lp] );
+  }
+  Node r = mkConcat( vec_r );
+  Trace("strings-loop") << " (" << r << ")" << std::endl;
+
+  //Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl;
+  //TODO: can be more general
+  if( s_zy.isConst() && r.isConst() && r != d_emptyString) {
+    int c;
+    bool flag = true;
+    if(s_zy.getConst<String>().tailcmp( r.getConst<String>(), c ) ) {
+      if(c >= 0) {
+        s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, c) );
+        r = d_emptyString;
+        vec_r.clear();
+        Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl;
+        flag = false;
       }
+    }
+    if(flag) {
+      Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl;
+      sendLemma( mkExplain( antec ), conc, "Loop Conflict" );
+      return true;
+    }
+  }
 
-      //construct the normal form
-      if( normal_forms.empty() ){
-        Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
-        getConcatVec( eqc, nf );
-      } else {
-        Trace("strings-solve-debug2") << "just take the first normal form" << std::endl;
-        //just take the first normal form
-        nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() );
-        nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() );
-        if( eqc!=normal_form_src[0] ){
-          nf_exp.push_back( eqc.eqNode( normal_form_src[0] ) );
+  //require that x is non-empty
+  if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
+    //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
+    sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Len-Split(Loop-X)" );
+  } else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING  ) {
+    //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
+    sendSplit( t_yz, d_emptyString, "Len-Split(Loop-YZ)" );
+  } else {
+    //need to break
+    antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
+    if( t_yz.getKind()!=kind::CONST_STRING ) {
+      antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+    }
+    Node ant = mkExplain( antec );
+    if(d_loop_antec.find(ant) == d_loop_antec.end()) {
+      d_loop_antec.insert(ant);
+
+      Node str_in_re;
+      if( s_zy == t_yz &&
+        r == d_emptyString &&
+        s_zy.isConst() &&
+        s_zy.getConst<String>().isRepeated()
+        ) {
+        Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
+        Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
+        Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
+        //special case
+        str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+                NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
+                NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
+        conc = str_in_re;
+      } else if(t_yz.isConst()) {
+        Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl;
+        CVC4::String s = t_yz.getConst< CVC4::String >();
+        unsigned size = s.size();
+        std::vector< Node > vconc;
+        for(unsigned len=1; len<=size; len++) {
+          Node y = NodeManager::currentNM()->mkConst(s.substr(0, len));
+          Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len));
+          Node restr = s_zy;
+          Node cc;
+          if(r != d_emptyString) {
+            std::vector< Node > v2(vec_r);
+            v2.insert(v2.begin(), y);
+            v2.insert(v2.begin(), z);
+            restr = mkConcat( z, y );
+            cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) ));
+          } else {
+            cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( z, y) ));
+          }
+          if(cc == d_false) {
+            continue;
+          }
+          Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+                  NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+                    NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
+                    NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
+                      NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr))));
+          cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 );
+          d_regexp_ant[conc2] = ant;
+          vconc.push_back(cc);
         }
-        Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+        conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc);
+      } else {
+        Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl;
+        //right
+        Node sk_w= mkSkolemS( "w_loop" );
+        Node sk_y= mkSkolemS( "y_loop", 1 );
+        Node sk_z= mkSkolemS( "z_loop" );
+        //t1 * ... * tn = y * z
+        Node conc1 = t_yz.eqNode( mkConcat( sk_y, sk_z ) );
+        // s1 * ... * sk = z * y * r
+        vec_r.insert(vec_r.begin(), sk_y);
+        vec_r.insert(vec_r.begin(), sk_z);
+        Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
+        Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
+        Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
+        str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
+                NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
+                  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, restr ) ) );
+
+        std::vector< Node > vec_conc;
+        vec_conc.push_back(conc1); vec_conc.push_back(conc2); vec_conc.push_back(conc3);
+        vec_conc.push_back(str_in_re);
+        //vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
+        conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
+      } // normal case
+
+      //set its antecedant to ant, to say when it is relevant
+      if(!str_in_re.isNull()) {
+        d_regexp_ant[str_in_re] = ant;
       }
 
-      d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
-      d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
-      d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
-      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
+      sendLemma( ant, conc, "F-LOOP" );
+      ++(d_statistics.d_loop_lemmas);
+
+      //we will be done
+      addNormalFormPair( normal_form_src[i], normal_form_src[j] );
     } else {
-      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
-      nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
-      nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
-      result = true;
+      Trace("strings-loop") << "Strings::Loop: loop lemma for " << ant << " has already added." << std::endl;
+      addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+      return false;
     }
-    visited.pop_back();
-    return result;
   }
+  return true;
 }
 
 //return true for lemma, false if we succeed
@@ -1854,7 +2522,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
   return 0;
 }
 
-void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
+void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){
   if( !isNormalFormPair( n1, n2 ) ){
     //Assert( !isNormalFormPair( n1, n2 ) );
     NodeList* lst;
@@ -1878,10 +2546,12 @@ void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
     Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
   }
 }
+
 bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
   //TODO: modulo equality?
   return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
 }
+
 bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
     //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
   NodeList* lst;
@@ -2114,6 +2784,18 @@ Node TheoryStrings::mkLength( Node t ) {
   return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
 }
 
+Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit ){
+  //return mkSkolemS( c, isLenSplit );
+  std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( id );
+  if( it==d_skolem_cache[a][b].end() ){
+    Node sk = mkSkolemS( c, isLenSplit );
+    d_skolem_cache[a][b][id] = sk;
+    return sk;
+  }else{
+    return it->second;
+  }
+}
+
 //isLenSplit: 0-yes, 1-no, 2-ignore
 Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) {
   Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" );
@@ -2214,371 +2896,9 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
         c.push_back( n[i] );
       }
     }
-  } else {
-    c.push_back( n );
-  }
-}
-
-void TheoryStrings::debugPrintFlatForms( const char * tc ){
-  for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
-    Node eqc = d_strings_eqc[k];
-    if( d_eqc[eqc].size()>1 ){
-      Trace( tc ) << "EQC [" << eqc << "]" << std::endl;
-    }else{
-      Trace( tc ) << "eqc [" << eqc << "]";
-    }
-    std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
-    if( itc!=d_eqc_to_const.end() ){
-      Trace( tc ) << "  C: " << itc->second;
-      if( d_eqc[eqc].size()>1 ){
-        Trace( tc ) << std::endl;
-      }
-    }
-    if( d_eqc[eqc].size()>1 ){
-      for( unsigned i=0; i<d_eqc[eqc].size(); i++ ){
-        Node n = d_eqc[eqc][i];
-        Trace( tc ) << "    ";
-        for( unsigned j=0; j<d_flat_form[n].size(); j++ ){
-          Node fc = d_flat_form[n][j];
-          itc = d_eqc_to_const.find( fc );
-          Trace( tc ) << " ";
-          if( itc!=d_eqc_to_const.end() ){
-            Trace( tc ) << itc->second;
-          }else{
-            Trace( tc ) << fc;
-          }
-        }
-        if( n!=eqc ){
-          Trace( tc ) << ", from " << n;
-        }
-        Trace( tc ) << std::endl;
-      }
-    }else{
-      Trace( tc ) << std::endl;
-    }
-  }
-  Trace( tc ) << std::endl;
-}
-
-void TheoryStrings::checkFlatForms() {
-  //first check for cycles, while building ordering of equivalence classes
-  d_eqc.clear();
-  d_flat_form.clear();
-  d_flat_form_index.clear();
-  Trace("strings-process") << "Check equivalence classes cycles...." << std::endl;
-  //rebuild strings eqc based on acyclic ordering
-  std::vector< Node > eqc;
-  eqc.insert( eqc.end(), d_strings_eqc.begin(), d_strings_eqc.end() );
-  d_strings_eqc.clear();
-  for( unsigned i=0; i<eqc.size(); i++ ){
-    std::vector< Node > curr;
-    std::vector< Node > exp;
-    checkCycles( eqc[i], curr, exp );
-    if( hasProcessed() ){
-      return;
-    }
-  }
-  Trace("strings-process-debug") << "Done check cycles, lemmas = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << std::endl;
-  if( !hasProcessed() ){
-    //debug print flat forms
-    if( Trace.isOn("strings-ff") ){
-      Trace("strings-ff") << "Flat forms : " << std::endl;
-      debugPrintFlatForms( "strings-ff" );
-    }
-    //inferences without recursively expanding flat forms
-    for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
-      Node eqc = d_strings_eqc[k];
-      Node c;
-      std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
-      if( itc!=d_eqc_to_const.end() ){
-        c = itc->second;   //use?
-      }
-      std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc );
-      if( it!=d_eqc.end() && it->second.size()>1 ){
-        //iterate over start index
-        for( unsigned start=0; start<it->second.size()-1; start++ ){
-          for( unsigned r=0; r<2; r++ ){
-            unsigned count = 0;
-            std::vector< Node > inelig;
-            for( unsigned i=0; i<=start; i++ ){
-              inelig.push_back( it->second[start] );
-            }
-            Node a = it->second[start];
-            Node b;
-            do{
-              std::vector< Node > exp;
-              //std::vector< Node > exp_n;
-              Node conc;
-              int inf_type = -1;
-              if( count==d_flat_form[a].size() ){
-                for( unsigned i=start+1; i<it->second.size(); i++ ){
-                  b = it->second[i];
-                  if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
-                    if( count<d_flat_form[b].size() ){
-                      //endpoint
-                      std::vector< Node > conc_c;
-                      for( unsigned j=count; j<d_flat_form[b].size(); j++ ){
-                        conc_c.push_back( b[d_flat_form_index[b][j]].eqNode( d_emptyString ) );
-                      }
-                      Assert( !conc_c.empty() );
-                      conc = mkAnd( conc_c );
-                      inf_type = 2;
-                      Assert( count>0 );
-                      //swap, will enforce is empty past current
-                      a = it->second[i]; b = it->second[start];
-                      count--;
-                      break;
-                    }
-                    inelig.push_back( it->second[i] );
-                  }
-                }
-              }else{
-                Node curr = d_flat_form[a][count];
-                Node curr_c = d_eqc_to_const[curr];
-                std::vector< Node > lexp;
-                Node lcurr = getLength( curr, lexp );
-                for( unsigned i=1; i<it->second.size(); i++ ){
-                  b = it->second[i];
-                  if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
-                    if( count==d_flat_form[b].size() ){
-                      inelig.push_back( b );
-                      //endpoint
-                      std::vector< Node > conc_c;
-                      for( unsigned j=count; j<d_flat_form[a].size(); j++ ){
-                        conc_c.push_back( a[d_flat_form_index[a][j]].eqNode( d_emptyString ) );
-                      }
-                      Assert( !conc_c.empty() );
-                      conc = mkAnd( conc_c );
-                      inf_type = 2;
-                      Assert( count>0 );
-                      count--;
-                      break;
-                    }else{
-                      Node cc = d_flat_form[b][count];
-                      if( cc!=curr ){
-                        Node ac = a[d_flat_form_index[a][count]];
-                        Node bc = b[d_flat_form_index[b][count]];
-                        inelig.push_back( b );
-                        Assert( !areEqual( curr, cc ) );
-                        Node cc_c = d_eqc_to_const[cc];
-                        if( !curr_c.isNull() && !cc_c.isNull() ){
-                          //check for constant conflict
-                          int index;
-                          Node s = TheoryStringsRewriter::splitConstant( cc_c, curr_c, index, r==1 );
-                          if( s.isNull() ){
-                            addToExplanation( ac, d_eqc_to_const_base[curr], exp );
-                            addToExplanation( d_eqc_to_const_exp[curr], exp );
-                            addToExplanation( bc, d_eqc_to_const_base[cc], exp );
-                            addToExplanation( d_eqc_to_const_exp[cc], exp );
-                            conc = d_false;
-                            inf_type = 0;
-                            break;
-                          }
-                        }else if( (d_flat_form[a].size()-1)==count && (d_flat_form[b].size()-1)==count ){
-                          conc = ac.eqNode( bc );
-                          inf_type = 3;
-                          break;
-                        }else{
-                          //if lengths are the same, apply LengthEq
-                          Node lcc = getLength( cc, lexp );
-                          if( areEqual( lcurr, lcc ) ){
-                            Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
-                            //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
-                            exp.insert( exp.end(), lexp.begin(), lexp.end() );
-                            addToExplanation( lcurr, lcc, exp );
-                            conc = ac.eqNode( bc );
-                            inf_type = 1;
-                            break;
-                          }
-                        }
-                      }
-                    }
-                  }
-                }
-              }
-              if( !conc.isNull() ){
-                Trace("strings-ff-debug") << "Found inference : " << conc << " based on equality " << a << " == " << b << " " << r << " " << inf_type << std::endl;
-                addToExplanation( a, b, exp );
-                //explain why prefixes up to now were the same
-                for( unsigned j=0; j<count; j++ ){
-                  Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " " << d_flat_form_index[b][j] << std::endl;
-                  addToExplanation( a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp );
-                }
-                //explain why other components up to now are empty
-                for( unsigned t=0; t<2; t++ ){
-                  Node c = t==0 ? a : b;
-                  int jj = t==0 ? d_flat_form_index[a][count] : ( inf_type==2 ? ( r==0 ? c.getNumChildren() : -1 ) : d_flat_form_index[b][count] );
-                  if( r==0 ){
-                    for( int j=0; j<jj; j++ ){
-                      if( areEqual( c[j], d_emptyString ) ){
-                        addToExplanation( c[j], d_emptyString, exp );
-                      }
-                    }
-                  }else{
-                    for( int j=(c.getNumChildren()-1); j>jj; --j ){
-                      if( areEqual( c[j], d_emptyString ) ){
-                        addToExplanation( c[j], d_emptyString, exp );
-                      }
-                    }
-                  }
-                }
-                //if( exp_n.empty() ){
-                sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
-                //}else{
-                //}
-                if( d_conflict ){
-                  return;
-                }else{
-                  break;
-                }
-              }
-              count++;
-            }while( inelig.size()<it->second.size() );
-
-            for( unsigned i=0; i<it->second.size(); i++ ){
-              std::reverse( d_flat_form[it->second[i]].begin(), d_flat_form[it->second[i]].end() );
-              std::reverse( d_flat_form_index[it->second[i]].begin(), d_flat_form_index[it->second[i]].end() );
-            }
-          }
-        }
-      }
-    }
-  }
-}
-
-Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
-  if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
-    // a loop
-    return eqc;
-  }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){
-    curr.push_back( eqc );
-    //look at all terms in this equivalence class
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ) {
-      Node n = (*eqc_i);
-      if( d_congruent.find( n )==d_congruent.end() ){
-        Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
-        if( n.getKind() == kind::STRING_CONCAT ) {
-          if( eqc!=d_emptyString_r ){
-            d_eqc[eqc].push_back( n );
-          }
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            Node nr = getRepresentative( n[i] );
-            if( eqc==d_emptyString_r ){
-              //for empty eqc, ensure all components are empty
-              if( nr!=d_emptyString_r ){
-                sendInfer( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "I_CYCLE_E" );
-                return Node::null();
-              }
-            }else{
-              if( nr!=d_emptyString_r ){
-                d_flat_form[n].push_back( nr );
-                d_flat_form_index[n].push_back( i );
-              }
-              //for non-empty eqc, recurse and see if we find a loop
-              Node ncy = checkCycles( nr, curr, exp );
-              if( !ncy.isNull() ){
-                Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
-                addToExplanation( n, eqc, exp );
-                addToExplanation( nr, n[i], exp );
-                if( ncy==eqc ){
-                  //can infer all other components must be empty
-                  for( unsigned j=0; j<n.getNumChildren(); j++ ){
-                    //take first non-empty
-                    if( j!=i && !areEqual( n[j], d_emptyString ) ){
-                      sendInfer( mkAnd( exp ), n[j].eqNode( d_emptyString ), "I_CYCLE" );
-                      return Node::null();
-                    }
-                  }
-                  Trace("strings-error") << "Looping term should be congruent : " << n << " " << eqc << " " << ncy << std::endl;
-                  //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
-                  Assert( false );
-                }else{
-                  return ncy;
-                }
-              }else{
-                if( hasProcessed() ){
-                  return Node::null();
-                }
-              }
-            }
-          }
-        }
-      }
-      ++eqc_i;
-    }
-    curr.pop_back();
-    //now we can add it to the list of equivalence classes
-    d_strings_eqc.push_back( eqc );
   }else{
-    //already processed
-  }
-  return Node::null();
-}
-
-
-void TheoryStrings::checkNormalForms() {
-  // simple extended func reduction
-  Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl;
-  checkExtfReduction( 1 );
-  Trace("strings-process") << "Done check extended function reduction" << std::endl;
-  if( !hasProcessed() ){
-    Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
-    //calculate normal forms for each equivalence class, possibly adding splitting lemmas
-    d_normal_forms.clear();
-    d_normal_forms_exp.clear();
-    std::map< Node, Node > nf_to_eqc;
-    std::map< Node, Node > eqc_to_exp;
-    for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
-      Node eqc = d_strings_eqc[i];
-      Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
-      std::vector< Node > visited;
-      std::vector< Node > nf;
-      std::vector< Node > nf_exp;
-      normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
-      Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
-      if( d_conflict ) {
-        return;
-      } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
-        Node nf_term = mkConcat( nf );
-        if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
-          //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
-          //two equivalence classes have same normal form, merge
-          nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
-          Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
-          sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
-        } else {
-          nf_to_eqc[nf_term] = eqc;
-          eqc_to_exp[eqc] = mkAnd( nf_exp );
-        }
-      }
-      Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
-    }
-
-    if(Trace.isOn("strings-nf")) {
-      Trace("strings-nf") << "**** Normal forms are : " << std::endl;
-      for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
-        Trace("strings-nf") << "  N[" << it->second << "] = " << it->first << std::endl;
-      }
-      Trace("strings-nf") << std::endl;
-    }
-    if( !hasProcessed() ){
-      checkExtendedFuncsEval( 1 );
-      Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-      if( !hasProcessed() ){
-        if( !options::stringEagerLen() ){
-          checkLengthsEqc();
-          if( hasProcessed() ){
-            return;
-          }
-        }
-        //process disequalities between equivalence classes
-        checkDeqNF();
-        Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-      }
-    }
+    c.push_back( n );
   }
-  Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
 }
 
 void TheoryStrings::checkDeqNF() {
@@ -2619,43 +2939,43 @@ void TheoryStrings::checkLengthsEqc() {
   if( options::stringLenNorm() ){
     for( unsigned i=0; i<d_strings_eqc.size(); i++ ){
       //if( d_normal_forms[nodes[i]].size()>1 ) {
-        Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl;
-        //check if there is a length term for this equivalence class
-        EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false );
-        Node lt = ei ? ei->d_length_term : Node::null();
-        if( !lt.isNull() ) {
-          Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
-          //now, check if length normalization has occurred
-          if( ei->d_normalized_length.get().isNull() ) {
-            //if not, add the lemma
-            std::vector< Node > ant;
-            ant.insert( ant.end(), d_normal_forms_exp[d_strings_eqc[i]].begin(), d_normal_forms_exp[d_strings_eqc[i]].end() );
-            ant.push_back( d_normal_forms_base[d_strings_eqc[i]].eqNode( lt ) );
-            Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[d_strings_eqc[i]] ) );
-            lc = Rewriter::rewrite( lc );
-            Node eq = llt.eqNode( lc );
-            if( llt!=lc ){
-              ei->d_normalized_length.set( eq );
-              sendLemma( mkExplain( ant ), eq, "LEN-NORM" );
-            }
+      Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl;
+      //check if there is a length term for this equivalence class
+      EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false );
+      Node lt = ei ? ei->d_length_term : Node::null();
+      if( !lt.isNull() ) {
+        Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt );
+        //now, check if length normalization has occurred
+        if( ei->d_normalized_length.get().isNull() ) {
+          //if not, add the lemma
+          std::vector< Node > ant;
+          ant.insert( ant.end(), d_normal_forms_exp[d_strings_eqc[i]].begin(), d_normal_forms_exp[d_strings_eqc[i]].end() );
+          ant.push_back( d_normal_forms_base[d_strings_eqc[i]].eqNode( lt ) );
+          Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[d_strings_eqc[i]] ) );
+          lc = Rewriter::rewrite( lc );
+          Node eq = llt.eqNode( lc );
+          if( llt!=lc ){
+            ei->d_normalized_length.set( eq );
+            sendLemma( mkExplain( ant ), eq, "LEN-NORM" );
           }
-        }else{
-          Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
-          if( !options::stringEagerLen() ){
-            Node c = mkConcat( d_normal_forms[d_strings_eqc[i]] );
-            registerTerm( c );
-            if( !c.isConst() ){
-              NodeNodeMap::const_iterator it = d_proxy_var.find( c );
-              if( it!=d_proxy_var.end() ){
-                Node pv = (*it).second;
-                Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
-                Node pvl = d_proxy_var_to_length[pv];
-                Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
-                sendLemma( d_true, ceq, "LEN-NORM-I" );
-              }
+        }
+      }else{
+        Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl;
+        if( !options::stringEagerLen() ){
+          Node c = mkConcat( d_normal_forms[d_strings_eqc[i]] );
+          registerTerm( c );
+          if( !c.isConst() ){
+            NodeNodeMap::const_iterator it = d_proxy_var.find( c );
+            if( it!=d_proxy_var.end() ){
+              Node pv = (*it).second;
+              Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
+              Node pvl = d_proxy_var_to_length[pv];
+              Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
+              sendLemma( d_true, ceq, "LEN-NORM-I" );
             }
           }
         }
+      }
       //} else {
       //  Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
       //}
@@ -3550,148 +3870,6 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
   return true;
 }
 
-void TheoryStrings::checkInit() {
-  //build term index
-  d_eqc_to_const.clear();
-  d_eqc_to_const_base.clear();
-  d_eqc_to_const_exp.clear();
-  d_eqc_to_len_term.clear();
-  d_term_index.clear();
-  d_strings_eqc.clear();
-
-  std::map< Kind, unsigned > ncongruent;
-  std::map< Kind, unsigned > congruent;
-  d_emptyString_r = getRepresentative( d_emptyString );
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    TypeNode tn = eqc.getType();
-    if( !tn.isRegExp() ){
-      if( tn.isString() ){
-        d_strings_eqc.push_back( eqc );
-      }
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-      while( !eqc_i.isFinished() ) {
-        Node n = *eqc_i;
-        if( tn.isInteger() ){
-          if( n.getKind()==kind::STRING_LENGTH ){
-            Node nr = getRepresentative( n[0] );
-            d_eqc_to_len_term[nr] = n[0];
-          }
-        }else if( n.isConst() ){
-          d_eqc_to_const[eqc] = n;
-          d_eqc_to_const_base[eqc] = n;
-          d_eqc_to_const_exp[eqc] = Node::null();
-        }else if( n.getNumChildren()>0 ){
-          Kind k = n.getKind();
-          if( k!=kind::EQUAL ){
-            if( d_congruent.find( n )==d_congruent.end() ){
-              std::vector< Node > c;
-              Node nc = d_term_index[k].add( n, 0, this, d_emptyString_r, c );
-              if( nc!=n ){
-                //check if we have inferred a new equality by removal of empty components
-                if( n.getKind()==kind::STRING_CONCAT && !areEqual( nc, n ) ){
-                  std::vector< Node > exp;
-                  unsigned count[2] = { 0, 0 };
-                  while( count[0]<nc.getNumChildren() || count[1]<n.getNumChildren() ){
-                    //explain empty prefixes
-                    for( unsigned t=0; t<2; t++ ){
-                      Node nn = t==0 ? nc : n;
-                      while( count[t]<nn.getNumChildren() &&
-                            ( nn[count[t]]==d_emptyString || areEqual( nn[count[t]], d_emptyString ) ) ){
-                        if( nn[count[t]]!=d_emptyString ){
-                          exp.push_back( nn[count[t]].eqNode( d_emptyString ) );
-                        }
-                        count[t]++;
-                      }
-                    }
-                    //explain equal components
-                    if( count[0]<nc.getNumChildren() ){
-                      Assert( count[1]<n.getNumChildren() );
-                      if( nc[count[0]]!=n[count[1]] ){
-                        exp.push_back( nc[count[0]].eqNode( n[count[1]] ) );
-                      }
-                      count[0]++;
-                      count[1]++;
-                    }
-                  }
-                  //infer the equality
-                  sendInfer( mkAnd( exp ), n.eqNode( nc ), "I_Norm" );
-                }else{
-                  //update the extf map : only process if neither has been reduced
-                  NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
-                  if( it!=d_ext_func_terms.end() ){
-                    if( d_ext_func_terms.find( nc )==d_ext_func_terms.end() ){
-                      d_ext_func_terms[nc] = (*it).second;
-                    }else{
-                      d_ext_func_terms[nc] = d_ext_func_terms[nc] && (*it).second;
-                    }
-                    d_ext_func_terms[n] = false;
-                  }
-                }
-                //this node is congruent to another one, we can ignore it
-                Trace("strings-process-debug") << "  congruent term : " << n << std::endl;
-                d_congruent.insert( n );
-                congruent[k]++;
-              }else if( k==kind::STRING_CONCAT && c.size()==1 ){
-                Trace("strings-process-debug") << "  congruent term by singular : " << n << " " << c[0] << std::endl;
-                //singular case
-                if( !areEqual( c[0], n ) ){
-                  std::vector< Node > exp;
-                  //explain empty components
-                  bool foundNEmpty = false;
-                  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                    if( areEqual( n[i], d_emptyString ) ){
-                      if( n[i]!=d_emptyString ){
-                        exp.push_back( n[i].eqNode( d_emptyString ) );
-                      }
-                    }else{
-                      Assert( !foundNEmpty );
-                      if( n[i]!=c[0] ){
-                        exp.push_back( n[i].eqNode( c[0] ) );
-                      }
-                      foundNEmpty = true;
-                    }
-                  }
-                  AlwaysAssert( foundNEmpty );
-                  //infer the equality
-                  sendInfer( mkAnd( exp ), n.eqNode( c[0] ), "I_Norm_S" );
-                }
-                d_congruent.insert( n );
-                congruent[k]++;
-              }else{
-                ncongruent[k]++;
-              }
-            }else{
-              congruent[k]++;
-            }
-          }
-        }
-        ++eqc_i;
-      }
-    }
-    ++eqcs_i;
-  }
-  if( Trace.isOn("strings-process") ){
-    for( std::map< Kind, TermIndex >::iterator it = d_term_index.begin(); it != d_term_index.end(); ++it ){
-      Trace("strings-process") << "  Terms[" << it->first << "] = " << ncongruent[it->first] << "/" << (congruent[it->first]+ncongruent[it->first]) << std::endl;
-    }
-  }
-  Trace("strings-process") << "Done check init, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-  //now, infer constants for equivalence classes
-  if( !hasProcessed() ){
-    //do fixed point
-    unsigned prevSize;
-    do{
-      Trace("strings-process-debug") << "Check constant equivalence classes..." << std::endl;
-      prevSize = d_eqc_to_const.size();
-      std::vector< Node > vecc;
-      checkConstantEquivalenceClasses( &d_term_index[kind::STRING_CONCAT], vecc );
-    }while( !hasProcessed() && d_eqc_to_const.size()>prevSize );
-    Trace("strings-process") << "Done check constant equivalence classes, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-  }
-}
-
 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
   Node n = ti->d_data;
   if( !n.isNull() ){
@@ -3771,261 +3949,6 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
   }
 }
 
-void TheoryStrings::checkExtendedFuncsEval( int effort ) {
-  Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
-  if( effort==0 ){
-    d_extf_vars.clear();
-  }
-  d_extf_pol.clear();
-  d_extf_exp.clear();
-  d_extf_info.clear();
-  Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
-  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-    if( (*it).second ){
-      Node n = (*it).first;
-      d_extf_pol[n] = 0;
-      if( n.getType().isBoolean() ){
-        if( areEqual( n, d_true ) ){
-          d_extf_pol[n] = 1;
-        }else if( areEqual( n, d_false ) ){
-          d_extf_pol[n] = -1;
-        }
-      }
-      Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << d_extf_pol[n] << "..." << std::endl;
-      if( effort==0 ){
-        std::map< Node, bool > visited;
-        collectVars( n, d_extf_vars[n], visited );
-      }
-      //build up a best current substitution for the variables in the term, exp is explanation for substitution
-      std::vector< Node > var;
-      std::vector< Node > sub;
-      for( std::map< Node, std::vector< Node > >::iterator itv = d_extf_vars[n].begin(); itv != d_extf_vars[n].end(); ++itv ){
-        Node nr = itv->first;
-        std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
-        Node s;
-        Node b;
-        Node e;
-        if( itc!=d_eqc_to_const.end() ){
-          b = d_eqc_to_const_base[nr];
-          s = itc->second;
-          e = d_eqc_to_const_exp[nr];
-        }else if( effort>0 ){
-          b = d_normal_forms_base[nr];
-          std::vector< Node > expt;
-          s = getNormalString( b, expt );
-          e = mkAnd( expt );
-        }
-        if( !s.isNull() ){
-          bool added = false;
-          for( unsigned i=0; i<itv->second.size(); i++ ){
-            if( itv->second[i]!=s ){
-              var.push_back( itv->second[i] );
-              sub.push_back( s );
-              addToExplanation( itv->second[i], b, d_extf_exp[n] );
-              Trace("strings-extf-debug") << "  " << itv->second[i] << " --> " << s << std::endl;
-              added = true;
-            }
-          }
-          if( added ){
-            addToExplanation( e, d_extf_exp[n] );
-          }
-        }
-      }
-      Node to_reduce;
-      if( !var.empty() ){
-        Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() );
-        Node nrc = Rewriter::rewrite( nr );
-        if( nrc.isConst() ){
-          //mark as reduced
-          d_ext_func_terms[n] = false;
-          Trace("strings-extf-debug") << "  resolvable by evaluation..." << std::endl;
-          std::vector< Node > exps;
-          Trace("strings-extf-debug") << "  get symbolic definition..." << std::endl;
-          Node nrs = getSymbolicDefinition( nr, exps );
-          if( !nrs.isNull() ){
-            Trace("strings-extf-debug") << "  rewrite " << nrs << "..." << std::endl;
-            nrs = Rewriter::rewrite( nrs );
-            //ensure the symbolic form is non-trivial
-            if( nrs.isConst() ){
-              Trace("strings-extf-debug") << "  symbolic definition is trivial..." << std::endl;
-              nrs = Node::null();
-            }
-          }else{
-            Trace("strings-extf-debug") << "  could not infer symbolic definition." << std::endl;
-          }
-          Node conc;
-          if( !nrs.isNull() ){
-            Trace("strings-extf-debug") << "  symbolic def : " << nrs << std::endl;
-            if( !areEqual( nrs, nrc ) ){
-              //infer symbolic unit
-              if( n.getType().isBoolean() ){
-                conc = nrc==d_true ? nrs : nrs.negate();
-              }else{
-                conc = nrs.eqNode( nrc );
-              }
-              d_extf_exp[n].clear();
-            }
-          }else{
-            if( !areEqual( n, nrc ) ){
-              if( n.getType().isBoolean() ){
-                d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n );
-                conc = d_false;
-              }else{
-                conc = n.eqNode( nrc );
-              }
-            }
-          }
-          if( !conc.isNull() ){
-            Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << std::endl;
-            if( n.getType().isInteger() || d_extf_exp[n].empty() ){
-              sendLemma( mkExplain( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" );
-            }else{
-              sendInfer( mkAnd( d_extf_exp[n] ), conc, effort==0 ? "EXTF" : "EXTF-N" );
-            }
-            if( d_conflict ){
-              Trace("strings-extf-debug") << "  conflict, return." << std::endl;
-              return;
-            }
-          }
-        }else if( ( nrc.getKind()==kind::OR && d_extf_pol[n]==-1 ) || ( nrc.getKind()==kind::AND && d_extf_pol[n]==1 ) ){
-          //infer the consequence of each
-          d_ext_func_terms[n] = false;
-          d_extf_exp[n].push_back( d_extf_pol[n]==-1 ? n.negate() : n );
-          Trace("strings-extf-debug") << "  decomposable..." << std::endl;
-          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl;
-          for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
-            sendInfer( mkAnd( d_extf_exp[n] ), d_extf_pol[n]==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
-          }
-        }else{
-          to_reduce = nrc;
-        }
-      }else{
-        to_reduce = n;
-      }
-      if( !to_reduce.isNull() ){
-        if( effort==1 ){
-          Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
-        }
-        checkExtfInference( n, to_reduce, effort );
-        if( Trace.isOn("strings-extf-list") ){
-          Trace("strings-extf-list") << "  * " << to_reduce;
-          if( d_extf_pol[n]!=0 ){
-            Trace("strings-extf-list") << ", pol = " << d_extf_pol[n];
-          }
-          if( n!=to_reduce ){
-            Trace("strings-extf-list") << ", from " << n;
-          }
-          Trace("strings-extf-list") << std::endl;
-        }
-      }
-    }else{
-      Trace("strings-extf-debug")  << "  already reduced " << (*it).first << std::endl;
-    }
-  }
-}
-
-void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
-  int n_pol = d_extf_pol[n];
-  if( n_pol!=0 ){
-    //add original to explanation
-    d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() );
-    if( nr.getKind()==kind::STRING_STRCTN ){
-      if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){
-        if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){
-          d_extf_infer_cache.insert( nr );
-          //one argument does (not) contain each of the components of the other argument
-          int index = n_pol==1 ? 1 : 0;
-          std::vector< Node > children;
-          children.push_back( nr[0] );
-          children.push_back( nr[1] );
-          Node exp_n = mkAnd( d_extf_exp[n] );
-          for( unsigned i=0; i<nr[index].getNumChildren(); i++ ){
-            children[index] = nr[index][i];
-            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children );
-            //can mark as reduced, since model for n => model for conc
-            d_ext_func_terms[conc] = false;
-            sendInfer( exp_n, n_pol==1 ? conc : conc.negate(), "CTN_Decompose" );
-          }
-        }
-      }else{
-        //store this (reduced) assertion
-        //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
-        bool pol = n_pol==1;
-        if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
-          Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
-          d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] );
-          d_extf_info[nr[0]].d_ctn_from[pol].push_back( n );
-          //transitive closure for contains
-          bool opol = !pol;
-          for( unsigned i=0; i<d_extf_info[nr[0]].d_ctn[opol].size(); i++ ){
-            Node onr = d_extf_info[nr[0]].d_ctn[opol][i];
-            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ).negate();
-            std::vector< Node > exp;
-            exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
-            Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
-            Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
-            exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
-            sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
-          }
-        }else{
-          Trace("strings-extf-debug") << "  redundant." << std::endl;
-          d_ext_func_terms[n] = false;
-        }
-      }
-    }
-  }
-}
-
-void TheoryStrings::collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ) {
-  if( !n.isConst() ){
-    if( visited.find( n )==visited.end() ){
-      visited[n] = true;
-      if( n.getNumChildren()>0 ){
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          collectVars( n[i], vars, visited );
-        }
-      }else{
-        Node nr = getRepresentative( n );
-        vars[nr].push_back( n );
-      }
-    }
-  }
-}
-
-Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) {
-  if( n.getNumChildren()==0 ){
-    NodeNodeMap::const_iterator it = d_proxy_var.find( n );
-    if( it==d_proxy_var.end() ){
-      return Node::null();
-    }else{
-      Node eq = n.eqNode( (*it).second );
-      eq = Rewriter::rewrite( eq );
-      if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
-        exp.push_back( eq );
-      }
-      return (*it).second;
-    }
-  }else{
-    std::vector< Node > children;
-    if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      children.push_back( n.getOperator() );
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n.getKind()==kind::STRING_IN_REGEXP && i==1 ){
-        children.push_back( n[i] );
-      }else{
-        Node ns = getSymbolicDefinition( n[i], exp );
-        if( ns.isNull() ){
-          return Node::null();
-        }else{
-          children.push_back( ns );
-        }
-      }
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }
-}
-
 void TheoryStrings::checkExtendedFuncs() {
   if( options::stringExp() ){
     checkExtfReduction( 2 );
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 721ba864e..125e1c1eb 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -250,11 +250,11 @@ private:
   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
   //normal forms check
   void checkNormalForms();
-  void mergeCstVec(std::vector< Node > &vec_strings);
-  bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
-        std::vector< std::vector< Node > > &normal_forms,
-        std::vector< std::vector< Node > > &normal_forms_exp,
-        std::vector< Node > &normal_form_src);
+  bool normalizeEquivalenceClass( Node n, std::vector< Node > & nf, std::vector< Node > & nf_exp );
+  bool getNormalForms( Node &eqc, std::vector< Node > & nf,
+                       std::vector< std::vector< Node > > &normal_forms,
+                       std::vector< std::vector< Node > > &normal_forms_exp,
+                       std::vector< Node > &normal_form_src);
   bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
         int i, int j, int index_i, int index_j,
         int &loop_in_i, int &loop_in_j);
@@ -271,7 +271,6 @@ private:
   bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
         unsigned& index_i, unsigned& index_j, bool isRev );
-  bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
   bool processDeq( Node n1, Node n2 );
   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
@@ -282,18 +281,17 @@ private:
   //check membership constraints
   Node mkRegExpAntec(Node atom, Node ant);
   Node normalizeRegexp(Node r);
-  bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps);
-  bool applyRConsume( CVC4::String &s, Node &r);
-  Node applyRSplit(Node s1, Node s2, Node r);
-  bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps);
-  bool checkMembershipsWithoutLength(
-    std::map< Node, std::vector< Node > > &memb_with_exps,
-    std::map< Node, std::vector< Node > > &XinR_with_exps);
+  bool normalizePosMemberships( std::map< Node, std::vector< Node > > &memb_with_exps );
+  bool applyRConsume( CVC4::String &s, Node &r );
+  Node applyRSplit( Node s1, Node s2, Node r );
+  bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
+  bool checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps, 
+                                      std::map< Node, std::vector< Node > > &XinR_with_exps);
   void checkMemberships();
   bool checkMemberships2();
-  bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
-    std::vector< Node > &processed, std::vector< Node > &cprocessed,
-    std::vector< Node > &nf_exp);
+  bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma,
+                         std::vector< Node > &processed, std::vector< Node > &cprocessed,
+                         std::vector< Node > &nf_exp);
   //check contains
   void checkPosContains( std::vector< Node >& posContains );
   void checkNegContains( std::vector< Node >& negContains );
@@ -346,6 +344,18 @@ protected:
   inline Node mkConcat( const std::vector< Node >& c );
   inline Node mkLength( Node n );
   //mkSkolem
+  enum {
+    sk_id_c_spt,
+    sk_id_vc_spt,
+    sk_id_v_spt,
+    sk_id_ctn_pre,
+    sk_id_ctn_post,
+    sk_id_deq_x,
+    sk_id_deq_y,
+    sk_id_deq_z,
+  };
+  std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
+  Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
   //inline Node mkSkolemI(const char * c);
   /** mkExplain **/
@@ -366,19 +376,6 @@ protected:
   void printConcat( std::vector< Node >& n, const char * c );
 
   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
-
-  enum {
-    sk_id_c_spt,
-    sk_id_vc_spt,
-    sk_id_v_spt,
-    sk_id_ctn_pre,
-    sk_id_ctn_post,
-    sk_id_deq_x,
-    sk_id_deq_y,
-    sk_id_deq_z,
-  };
-  std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
-  Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
 private:
 
   // Special String Functions