From cd119eedadb0431cfbcfc6c3ae037781ae849ee4 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Oct 2015 12:49:49 +0200
Subject: [PATCH] Refactor strings, remove old cycle checks in normalize eqc.

---
 src/theory/strings/theory_strings.cpp | 3701 ++++++++++++-------------
 src/theory/strings/theory_strings.h   |   55 +-
 2 files changed, 1838 insertions(+), 1918 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,734 +872,769 @@ 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) {
-  Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
-  // EqcItr
-  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::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!=d_emptyString ) {
-            nf_n.push_back( n );
+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.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 ) {
-                    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] << " ";
+        }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]++;
                     }
-                    Trace("strings-error") << std::endl;
                   }
-                  Assert( !nresult || 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] ) {
-              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 ) {
-            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 ) );
+                  //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;
+                  }
                 }
-                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 ) );
+                //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" );
                 }
-                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;
+                d_congruent.insert( n );
+                congruent[k]++;
+              }else{
+                ncongruent[k]++;
               }
+            }else{
+              congruent[k]++;
             }
           }
-          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 {
-          Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
-          //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() );
-            ant.push_back( n.eqNode( eqc ) );
-            Node conc = Rewriter::rewrite( nn.eqNode( eqc ) );
-            sendInfer( mkAnd( ant ), conc, "CYCLE-T" );
-            return true;
-          }
         }
-        //}
+        ++eqc_i;
       }
     }
-    ++eqc_i;
+    ++eqcs_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") << ", ";
-          }
-          Trace("strings-solve") << normal_forms[i][j];
-        }
-        Trace("strings-solve") << std::endl;
-        Trace("strings-solve") << "   Explanation is : ";
-        if(normal_forms_exp[i].size() == 0) {
-          Trace("strings-solve") << "NONE";
-        } else {
-          for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
-            if(j>0) {
-              Trace("strings-solve") << " AND ";
-            }
-            Trace("strings-solve") << normal_forms_exp[i][j];
-          }
-        }
-        Trace("strings-solve") << std::endl;
-      }
-    } else {
-      //std::vector< Node > nf;
-      //nf.push_back( eqc );
-      //normal_forms.push_back(nf);
-      //std::vector< Node > nf_exp_def;
-      //normal_forms_exp.push_back(nf_exp_def);
-      //normal_form_src.push_back(eqc);
-      Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+  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;
     }
   }
-  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;
-    }
+  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;
   }
 }
 
-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;
-          }
+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;
         }
       }
-    }
-  }
-  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;
+      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;
+    }
   }
 }
-//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] );
+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;
+        }
+      }
+    }
   }
-  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;
+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 );
       }
     }
-    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);
+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 );
         }
-        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 NodeManager::currentNM()->mkNode( n.getKind(), children );
   }
-  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 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;
-  for(unsigned i=0; i<normal_forms.size()-1; i++) {
-    //unify each normalform[j] with normal_forms[i]
-    for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
-      Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
-      if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
-        Trace("strings-solve") << "Strings: Already cached." << std::endl;
-      } else {
-        //the current explanation for why the prefix is equal
-        std::vector< Node > curr_exp;
-        curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
-        curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
-        if( normal_form_src[i]!=normal_form_src[j] ){
-          curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
+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;
+          }
         }
-
-        //process the reverse direction first (check for easy conflicts and inferences)
-        if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){
-          return true;
+        if( n!=eqc ){
+          Trace( tc ) << ", from " << n;
         }
+        Trace( tc ) << std::endl;
+      }
+    }else{
+      Trace( tc ) << std::endl;
+    }
+  }
+  Trace( tc ) << std::endl;
+}
 
-        //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
-        unsigned index_i = 0;
-        unsigned index_j = 0;
-        bool success;
-        do
-        {
-          //simple check
-          if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
-            //added a lemma, return
-            return true;
-          }
-
-          success = false;
-          //if we are at the end
-          if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
-            Assert( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() );
-            //we're done
-            //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-          } else {
-            std::vector< Node > lexp;
-            Node length_term_i = getLength( normal_forms[i][index_i], lexp );
-            Node length_term_j = getLength( normal_forms[j][index_j], lexp );
-            //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-            if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) &&
-                normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
-              //length terms are equal, merge equivalence classes if not already done so
-              Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
-              Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
-              //try to make the lengths equal via splitting on demand
-              sendSplit( length_term_i, length_term_j, "Len-Split(Diseq)" );
-              length_eq = Rewriter::rewrite( length_eq  );
-              d_pending_req_phase[ length_eq ] = true;
-              return true;
-            } else {
-              Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
-              int loop_in_i = -1;
-              int loop_in_j = -1;
-              if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
-                if( !flag_lb ){
-                  c_i = i;
-                  c_j = j;
-                  c_loop_n_index = loop_in_i!=-1 ? i : j;
-                  c_other_n_index = loop_in_i!=-1 ? j : i;
-                  c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
-                  c_index = loop_in_i!=-1 ? index_i : index_j;
-                  c_other_index = loop_in_i!=-1 ? index_j : index_i;
-
-                  c_lb_exp = curr_exp;
-
-                  if(options::stringLB() == 0) {
-                    flag_lb = true;
-                  } else {
-                    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
-                      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
-                      return true;
+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 conc;
-                std::vector< Node > antec;
-                Trace("strings-solve-debug") << "No loops detected." << std::endl;
-                if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
-                  unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
-                  unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
-                  unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
-                  unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
-                  Node const_str = normal_forms[const_k][const_index_k];
-                  Node other_str = normal_forms[nconst_k][nconst_index_k];
-                  Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
-                  Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
-                  if( !areDisequal(other_str, d_emptyString) ) {
-                    sendSplit( other_str, d_emptyString, "Len-Split(CST)" );
-                  } else {
-                    Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var");
-                    antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() );
-                    Node xnz = other_str.eqNode(d_emptyString).negate();
-                    antec.push_back( xnz );
-                    Node conc;
-                    if( normal_forms[nconst_k].size() > nconst_index_k + 1 && normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
-                      CVC4::String stra = const_str.getConst<String>();
-                      CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
-                      CVC4::String stra1 = stra.substr(1);
-                      size_t p = stra.size() - stra1.overlap(strb);
-                      size_t p2 = stra1.find(strb);
-                      p = p2==std::string::npos? p : ( p>p2+1? p2+1 : p );
-                      Node prea = p==stra.size()? const_str : NodeManager::currentNM()->mkConst(stra.substr(0, p));
-                      Node sk = mkSkolemCached( other_str, prea, sk_id_c_spt, "c_spt" );
-                      conc = other_str.eqNode( mkConcat(prea, sk) );
-                      Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << std::endl;
-                    } else {
-                      // normal v/c split
-                      Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-                        NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-                      Node sk = mkSkolemCached( other_str, firstChar, sk_id_vc_spt, "c_spt" );
-                      conc = other_str.eqNode( mkConcat(firstChar, sk) );
-                      Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (normal) " << std::endl;
+              }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 );
+                      }
                     }
-
-                    conc = Rewriter::rewrite( conc );
-                    sendLemma( mkExplain( antec ), conc, "S-Split(CST-P)" );
-                    //sendInfer(mkAnd( antec ), conc, "S-Split(CST-P)");
-                  }
-                  return true;
-                } else {
-                  std::vector< Node > antec_new_lits;
-                  antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-
-                  Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
-                  if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
-                    antec.push_back( ldeq );
                   }else{
-                    antec_new_lits.push_back(ldeq);
-                  }
-
-                  //x!=e /\ y!=e
-                  for(unsigned xory=0; xory<2; xory++) {
-                    Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j];
-                    Node xgtz = x.eqNode( d_emptyString ).negate();
-                    if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
-                      antec.push_back( xgtz );
-                    } else {
-                      antec_new_lits.push_back( xgtz );
+                    for( int j=(c.getNumChildren()-1); j>jj; --j ){
+                      if( areEqual( c[j], d_emptyString ) ){
+                        addToExplanation( c[j], d_emptyString, exp );
+                      }
                     }
                   }
-
-                  Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
-                  Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
-                  Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
-                  conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
-
-                  Node ant = mkExplain( antec, antec_new_lits );
-                  sendLemma( ant, conc, "S-Split(VAR)" );
-                  //sendInfer( ant, conc, "S-Split(VAR)" );
-                  //++(d_statistics.d_eq_splits);
-                  return true;
+                }
+                //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() );
             }
           }
-        } while(success);
+        }
       }
     }
-    if(!flag_lb) {
-      return false;
-    }
-  }
-  if(flag_lb) {
-    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
-      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
-      return true;
-    }
   }
-
-  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 ) {
-  //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() );
-
-  std::vector< Node > t_curr_exp;
-  t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
-  unsigned index_i = 0;
-  unsigned index_j = 0;
-  bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
-
-  //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() );
-
-  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 success;
-  do {
-    success = false;
-    //if we are at the end
-    if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
-      if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) {
-        //we're done
-      } else {
-        //the remainder must be empty
-        unsigned k = index_i==normal_forms[i].size() ? j : i;
-        unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
-        Node eq_exp = mkAnd( curr_exp );
-        while(!d_conflict && index_k<normal_forms[k].size()) {
-          //can infer that this string must be empty
-          Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
-          //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
-          Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
-          sendInfer( eq_exp, eq, "EQ_Endpoint" );
-          index_k++;
-        }
-        return true;
-      }
-    }else{
-      Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
-      if(areEqual(normal_forms[i][index_i], normal_forms[j][index_j])) {
-        Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
-        //terms are equal, continue
-        if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
-          Node eq = normal_forms[i][index_i].eqNode(normal_forms[j][index_j]);
-          Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
-          curr_exp.push_back(eq);
-        }
-        index_j++;
-        index_i++;
-        success = true;
-      } else {
-        std::vector< Node > temp_exp;
-        Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
-        Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
-        //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-        if( areEqual( length_term_i, length_term_j ) ){
-          Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
-          Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
-          //eq = Rewriter::rewrite( eq );
-          Node length_eq = length_term_i.eqNode( length_term_j );
-          temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
-          temp_exp.push_back(length_eq);
-          sendInfer( mkAnd( temp_exp ), eq, "LengthEq" );
-          return true;
-        }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) ||
-                  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
-          Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
-          Node conc;
-          std::vector< Node > antec;
-          antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-          std::vector< Node > eqn;
-          for( unsigned r=0; r<2; r++ ) {
-            int index_k = r==0 ? index_i : index_j;
-            int k = r==0 ? i : j;
-            std::vector< Node > eqnc;
-            for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
-              if(isRev) {
-                eqnc.insert(eqnc.begin(), normal_forms[k][index_l] );
-              } else {
-                eqnc.push_back( normal_forms[k][index_l] );
-              }
-            }
-            eqn.push_back( mkConcat( eqnc ) );
-          }
-          if( !areEqual( eqn[0], eqn[1] ) ) {
-            conc = eqn[0].eqNode( eqn[1] );
-            sendLemma( mkExplain( antec ), conc, "ENDPOINT" );
-            //sendInfer( mkAnd( antec ), conc, "ENDPOINT" );
-            return true;
-          }else{
-            index_i = normal_forms[i].size();
-            index_j = normal_forms[j].size();
+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 );
           }
-        } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
-          Node const_str = normal_forms[i][index_i];
-          Node other_str = normal_forms[j][index_j];
-          Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
-          unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
-          bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
-          if( isSameFix ) {
-            //same prefix/suffix
-            //k is the index of the string that is shorter
-            int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
-            int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
-            int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
-            int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
-            if(isRev) {
-              int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
-              Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
-              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
-              normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
-            } else {
-              Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index_l].getConst<String>().substr(len_short));
-              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
-              normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
-            }
-            normal_forms[l][index_l] = normal_forms[k][index_k];
-            index_i++;
-            index_j++;
-            success = true;
-          } else {
-            std::vector< Node > antec;
-            //curr_exp is conflict
-            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-            Node ant = mkExplain( antec );
-            sendLemma( ant, d_false, "Const Conflict" );
-            return true;
+          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;
     }
-  }while( success );
-  return false;
+    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 > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
+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( 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 ) ) {
+  if( areEqual( eqc, d_emptyString ) ) {
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
       Node n = (*eqc_i);
@@ -1628,9 +1661,8 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
     d_normal_forms_exp[eqc].clear();
     return true;
   } else {
-    visited.push_back( eqc );
     bool result;
-    if(d_normal_forms.find(eqc)==d_normal_forms.end() ) {
+    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;
@@ -1639,20 +1671,19 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
       // 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() ) {
+      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)) {
+      }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 {
+      }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() );
@@ -1667,918 +1698,1207 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
       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 {
+    }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;
     }
-    visited.pop_back();
     return result;
   }
 }
 
-//return true for lemma, false if we succeed
-bool TheoryStrings::processDeq( Node ni, Node nj ) {
-  //Assert( areDisequal( ni, nj ) );
-  if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
-    std::vector< Node > nfi;
-    nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
-    std::vector< Node > nfj;
-    nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
+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;
+  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::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;
+        if( n.getKind()==kind::CONST_STRING ){
+          if( n!=d_emptyString ) {
+            nf_n.push_back( n );
+          }
+        }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;
+            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( 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] ){
+              nf_exp_n.push_back( n[i].eqNode( nr ) );
+            }
+          }
+        }
+        //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 ) {
+            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 ) );
+            }
+          }
+          normal_forms.push_back(nf_n);
+          normal_forms_exp.push_back(nf_exp_n);
+          normal_form_src.push_back(n);
+        }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() );
+            ant.push_back( n.eqNode( eqc ) );
+            Node conc = Rewriter::rewrite( nn.eqNode( eqc ) );
+            sendInfer( mkAnd( ant ), conc, "CYCLE-T" );
+            return true;
+          }
+          */
+        }
+        //}
+      }
+    }
+    ++eqc_i;
+  }
+
+  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] << ") : ";
+        for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
+          if(j>0) {
+            Trace("strings-solve") << ", ";
+          }
+          Trace("strings-solve") << normal_forms[i][j];
+        }
+        Trace("strings-solve") << std::endl;
+        Trace("strings-solve") << "   Explanation is : ";
+        if(normal_forms_exp[i].size() == 0) {
+          Trace("strings-solve") << "NONE";
+        } else {
+          for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
+            if(j>0) {
+              Trace("strings-solve") << " AND ";
+            }
+            Trace("strings-solve") << normal_forms_exp[i][j];
+          }
+        }
+        Trace("strings-solve") << std::endl;
+      }
+    } else {
+      //std::vector< Node > nf;
+      //nf.push_back( eqc );
+      //normal_forms.push_back(nf);
+      //std::vector< Node > nf_exp_def;
+      //normal_forms_exp.push_back(nf_exp_def);
+      //normal_form_src.push_back(eqc);
+      Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
+    }
+  }
+  return true;
+}
+
+
+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;
+  for(unsigned i=0; i<normal_forms.size()-1; i++) {
+    //unify each normalform[j] with normal_forms[i]
+    for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
+      Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
+      if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
+        Trace("strings-solve") << "Strings: Already cached." << std::endl;
+      } else {
+        //the current explanation for why the prefix is equal
+        std::vector< Node > curr_exp;
+        curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() );
+        curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() );
+        if( normal_form_src[i]!=normal_form_src[j] ){
+          curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
+        }
+
+        //process the reverse direction first (check for easy conflicts and inferences)
+        if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){
+          return true;
+        }
+
+        //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
+        unsigned index_i = 0;
+        unsigned index_j = 0;
+        bool success;
+        do
+        {
+          //simple check
+          if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
+            //added a lemma, return
+            return true;
+          }
+
+          success = false;
+          //if we are at the end
+          if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
+            Assert( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() );
+            //we're done
+            //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+          } else {
+            std::vector< Node > lexp;
+            Node length_term_i = getLength( normal_forms[i][index_i], lexp );
+            Node length_term_j = getLength( normal_forms[j][index_j], lexp );
+            //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
+            if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) &&
+                normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+              //length terms are equal, merge equivalence classes if not already done so
+              Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
+              Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
+              //try to make the lengths equal via splitting on demand
+              sendSplit( length_term_i, length_term_j, "Len-Split(Diseq)" );
+              length_eq = Rewriter::rewrite( length_eq  );
+              d_pending_req_phase[ length_eq ] = true;
+              return true;
+            } else {
+              Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
+              int loop_in_i = -1;
+              int loop_in_j = -1;
+              if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
+                if( !flag_lb ){
+                  c_i = i;
+                  c_j = j;
+                  c_loop_n_index = loop_in_i!=-1 ? i : j;
+                  c_other_n_index = loop_in_i!=-1 ? j : i;
+                  c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
+                  c_index = loop_in_i!=-1 ? index_i : index_j;
+                  c_other_index = loop_in_i!=-1 ? index_j : index_i;
+
+                  c_lb_exp = curr_exp;
+
+                  if(options::stringLB() == 0) {
+                    flag_lb = true;
+                  } else {
+                    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
+                      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+                      return true;
+                    }
+                  }
+                }
+              } else {
+                Node conc;
+                std::vector< Node > antec;
+                Trace("strings-solve-debug") << "No loops detected." << std::endl;
+                if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
+                  unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
+                  unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
+                  unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
+                  unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
+                  Node const_str = normal_forms[const_k][const_index_k];
+                  Node other_str = normal_forms[nconst_k][nconst_index_k];
+                  Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
+                  Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
+                  if( !areDisequal(other_str, d_emptyString) ) {
+                    sendSplit( other_str, d_emptyString, "Len-Split(CST)" );
+                  } else {
+                    Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var");
+                    antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() );
+                    Node xnz = other_str.eqNode(d_emptyString).negate();
+                    antec.push_back( xnz );
+                    Node conc;
+                    if( normal_forms[nconst_k].size() > nconst_index_k + 1 && normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+                      CVC4::String stra = const_str.getConst<String>();
+                      CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+                      CVC4::String stra1 = stra.substr(1);
+                      size_t p = stra.size() - stra1.overlap(strb);
+                      size_t p2 = stra1.find(strb);
+                      p = p2==std::string::npos? p : ( p>p2+1? p2+1 : p );
+                      Node prea = p==stra.size()? const_str : NodeManager::currentNM()->mkConst(stra.substr(0, p));
+                      Node sk = mkSkolemCached( other_str, prea, sk_id_c_spt, "c_spt" );
+                      conc = other_str.eqNode( mkConcat(prea, sk) );
+                      Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << std::endl;
+                    } else {
+                      // normal v/c split
+                      Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+                        NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+                      Node sk = mkSkolemCached( other_str, firstChar, sk_id_vc_spt, "c_spt" );
+                      conc = other_str.eqNode( mkConcat(firstChar, sk) );
+                      Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (normal) " << std::endl;
+                    }
+
+                    conc = Rewriter::rewrite( conc );
+                    sendLemma( mkExplain( antec ), conc, "S-Split(CST-P)" );
+                    //sendInfer(mkAnd( antec ), conc, "S-Split(CST-P)");
+                  }
+                  return true;
+                } else {
+                  std::vector< Node > antec_new_lits;
+                  antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
 
-    int revRet = processReverseDeq( nfi, nfj, ni, nj );
-    if( revRet!=0 ){
-      return revRet==-1;
-    }
+                  Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
+                  if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
+                    antec.push_back( ldeq );
+                  }else{
+                    antec_new_lits.push_back(ldeq);
+                  }
 
-    nfi.clear();
-    nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
-    nfj.clear();
-    nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
+                  //x!=e /\ y!=e
+                  for(unsigned xory=0; xory<2; xory++) {
+                    Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j];
+                    Node xgtz = x.eqNode( d_emptyString ).negate();
+                    if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
+                      antec.push_back( xgtz );
+                    } else {
+                      antec_new_lits.push_back( xgtz );
+                    }
+                  }
 
-    unsigned index = 0;
-    while( index<nfi.size() || index<nfj.size() ){
-      int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
-      if( ret!=0 ) {
-        return ret==-1;
-      } else {
-        Assert( index<nfi.size() && index<nfj.size() );
-        Node i = nfi[index];
-        Node j = nfj[index];
-        Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
-        if( !areEqual( i, j ) ) {
-          Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
-          std::vector< Node > lexp;
-          Node li = getLength( i, lexp );
-          Node lj = getLength( j, lexp );
-          if( areDisequal(li, lj) ){
-            //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
+                  Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
+                  Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
+                  Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
+                  conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
 
-            Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
-            //must add lemma
-            std::vector< Node > antec;
-            std::vector< Node > antec_new_lits;
-            antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
-            antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
-            //check disequal
-            if( areDisequal( ni, nj ) ){
-              antec.push_back( ni.eqNode( nj ).negate() );
-            }else{
-              antec_new_lits.push_back( ni.eqNode( nj ).negate() );
+                  Node ant = mkExplain( antec, antec_new_lits );
+                  sendLemma( ant, conc, "S-Split(VAR)" );
+                  //sendInfer( ant, conc, "S-Split(VAR)" );
+                  //++(d_statistics.d_eq_splits);
+                  return true;
+                }
+              }
             }
-            antec_new_lits.push_back( li.eqNode( lj ).negate() );
-            std::vector< Node > conc;
-            Node sk1 = mkSkolemCached( i, j, sk_id_deq_x, "x_dsplit" );
-            Node sk2 = mkSkolemCached( i, j, sk_id_deq_y, "y_dsplit" );
-            Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 );
-            //Node nemp = sk3.eqNode(d_emptyString).negate();
-            //conc.push_back(nemp);
-            Node lsk1 = mkLength( sk1 );
-            conc.push_back( lsk1.eqNode( li ) );
-            Node lsk2 = mkLength( sk2 );
-            conc.push_back( lsk2.eqNode( lj ) );
-            conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
-            sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
-            ++(d_statistics.d_deq_splits);
-            return true;
-          }else if( areEqual( li, lj ) ){
-            Assert( !areDisequal( i, j ) );
-            //splitting on demand : try to make them disequal
-            Node eq = i.eqNode( j );
-            sendSplit( i, j, "S-Split(DEQL)" );
-            eq = Rewriter::rewrite( eq );
-            d_pending_req_phase[ eq ] = false;
-            return true;
-          }else{
-            //splitting on demand : try to make lengths equal
-            Node eq = li.eqNode( lj );
-            sendSplit( li, lj, "D-Split" );
-            eq = Rewriter::rewrite( eq );
-            d_pending_req_phase[ eq ] = true;
-            return true;
           }
-        }
-        index++;
+        } while(success);
       }
     }
-    Assert( false );
+    if(!flag_lb) {
+      return false;
+    }
+  }
+  if(flag_lb) {
+    if(processLoop(c_lb_exp, normal_forms, normal_form_src,
+      c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+      return true;
+    }
   }
+
   return false;
 }
 
-int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ) {
+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( nfi.begin(), nfi.end() );
-  std::reverse( nfj.begin(), nfj.end() );
+  std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
+  std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
 
-  unsigned index = 0;
-  int ret = processSimpleDeq( nfi, nfj, ni, nj, index, true );
+  std::vector< Node > t_curr_exp;
+  t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
+  unsigned index_i = 0;
+  unsigned index_j = 0;
+  bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
 
   //reverse normal form of i, j
-  std::reverse( nfi.begin(), nfi.end() );
-  std::reverse( nfj.begin(), nfj.end() );
+  std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
+  std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
 
   return ret;
 }
 
-int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) {
-  while( index<nfi.size() || index<nfj.size() ) {
-    if( index>=nfi.size() || index>=nfj.size() ) {
-      Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
-      std::vector< Node > ant;
-      //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
-      Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] );
-      Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] );
-      ant.push_back( lni.eqNode( lnj ) );
-      ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
-      ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
-      std::vector< Node > cc;
-      std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
-      for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
-        cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
+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;
+    //if we are at the end
+    if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
+      if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ) {
+        //we're done
+      } else {
+        //the remainder must be empty
+        unsigned k = index_i==normal_forms[i].size() ? j : i;
+        unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i;
+        Node eq_exp = mkAnd( curr_exp );
+        while(!d_conflict && index_k<normal_forms[k].size()) {
+          //can infer that this string must be empty
+          Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
+          //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
+          Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) );
+          sendInfer( eq_exp, eq, "EQ_Endpoint" );
+          index_k++;
+        }
+        return true;
       }
-      Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
-      conc = Rewriter::rewrite( conc );
-      sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty");
-      //sendInfer(mkAnd( ant ), conc, "Disequality Normalize Empty");
-      return -1;
-    } else {
-      Node i = nfi[index];
-      Node j = nfj[index];
-      Trace("strings-solve-debug")  << "...Processing(QED) " << i << " " << j << std::endl;
-      if( !areEqual( i, j ) ) {
-        if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
-          unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
-          bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
+    }else{
+      Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl;
+      if(areEqual(normal_forms[i][index_i], normal_forms[j][index_j])) {
+        Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
+        //terms are equal, continue
+        if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
+          Node eq = normal_forms[i][index_i].eqNode(normal_forms[j][index_j]);
+          Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
+          curr_exp.push_back(eq);
+        }
+        index_j++;
+        index_i++;
+        success = true;
+      } else {
+        std::vector< Node > temp_exp;
+        Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
+        Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
+        //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
+        if( areEqual( length_term_i, length_term_j ) ){
+          Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
+          Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
+          //eq = Rewriter::rewrite( eq );
+          Node length_eq = length_term_i.eqNode( length_term_j );
+          temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+          temp_exp.push_back(length_eq);
+          sendInfer( mkAnd( temp_exp ), eq, "LengthEq" );
+          return true;
+        }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) ||
+                  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
+          Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
+          Node conc;
+          std::vector< Node > antec;
+          antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+          std::vector< Node > eqn;
+          for( unsigned r=0; r<2; r++ ) {
+            int index_k = r==0 ? index_i : index_j;
+            int k = r==0 ? i : j;
+            std::vector< Node > eqnc;
+            for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
+              if(isRev) {
+                eqnc.insert(eqnc.begin(), normal_forms[k][index_l] );
+              } else {
+                eqnc.push_back( normal_forms[k][index_l] );
+              }
+            }
+            eqn.push_back( mkConcat( eqnc ) );
+          }
+          if( !areEqual( eqn[0], eqn[1] ) ) {
+            conc = eqn[0].eqNode( eqn[1] );
+            sendLemma( mkExplain( antec ), conc, "ENDPOINT" );
+            //sendInfer( mkAnd( antec ), conc, "ENDPOINT" );
+            return true;
+          }else{
+            index_i = normal_forms[i].size();
+            index_j = normal_forms[j].size();
+          }
+        } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
+          Node const_str = normal_forms[i][index_i];
+          Node other_str = normal_forms[j][index_j];
+          Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
+          unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
+          bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
           if( isSameFix ) {
             //same prefix/suffix
             //k is the index of the string that is shorter
-            Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j;
-            Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i;
-            Node remainderStr;
+            int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
+            int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
+            int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
+            int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
             if(isRev) {
-              int new_len = nl.getConst<String>().size() - len_short;
-              remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) );
-              Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
-            } else {
-              remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
-              Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
-            }
-            if( i.getConst<String>().size() < j.getConst<String>().size() ) {
-              nfj.insert( nfj.begin() + index + 1, remainderStr );
-              nfj[index] = nfi[index];
+              int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
+              Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
+              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+              normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
             } else {
-              nfi.insert( nfi.begin() + index + 1, remainderStr );
-              nfi[index] = nfj[index];
+              Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index_l].getConst<String>().substr(len_short));
+              Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+              normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
             }
+            normal_forms[l][index_l] = normal_forms[k][index_k];
+            index_i++;
+            index_j++;
+            success = true;
           } else {
-            return 1;
-          }
-        } else {
-          std::vector< Node > lexp;
-          Node li = getLength( i, lexp );
-          Node lj = getLength( j, lexp );
-          if( areEqual( li, lj ) && areDisequal( i, j ) ) {
-            Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
-            //we are done: D-Remove
-            return 1;
-          } else {
-            return 0;
+            std::vector< Node > antec;
+            //curr_exp is conflict
+            antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+            Node ant = mkExplain( antec );
+            sendLemma( ant, d_false, "Const Conflict" );
+            return true;
           }
         }
       }
-      index++;
     }
-  }
-  return 0;
+  }while( success );
+  return false;
 }
 
-void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) {
-  if( !isNormalFormPair( n1, n2 ) ){
-    //Assert( !isNormalFormPair( n1, n2 ) );
-    NodeList* lst;
-    NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-    if( nf_i == d_nf_pairs.end() ){
-      if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
-        addNormalFormPair( n2, n1 );
-        return;
+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;
+          }
+        }
       }
-      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
-                                                           ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_nf_pairs.insertDataFromContextMemory( n1, lst );
-      Trace("strings-nf") << "Create cache for " << n1 << std::endl;
-    } else {
-      lst = (*nf_i).second;
     }
-    Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
-    lst->push_back( n2 );
-    Assert( isNormalFormPair( n1, n2 ) );
+  }
+  if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
+    loop_in_i = has_loop[0];
+    loop_in_j = has_loop[1];
+    return true;
   } else {
-    Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
+    return false;
   }
 }
-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;
-  NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
-  if( nf_i != d_nf_pairs.end() ) {
-    lst = (*nf_i).second;
-    for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
-      Node n = *i;
-      if( n==n2 ) {
-          return true;
+
+//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;
+    }
   }
-  return false;
-}
 
-bool TheoryStrings::registerTerm( Node n ) {
-  if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) {
-    d_registered_terms_cache.insert(n);
-    Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl;
-    if(n.getType().isString()) {
-      //register length information:
-      //  for variables, split on empty vs positive length
-      //  for concat/const, introduce proxy var and state length relation
-      if( n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-        if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
-          sendLengthLemma( n );
-          ++(d_statistics.d_splits);
-        }
-      } else {
-        Node sk = mkSkolemS("lsym", 2);
-        StringsProxyVarAttribute spva;
-        sk.setAttribute(spva,true);
-        Node eq = Rewriter::rewrite( sk.eqNode(n) );
-        Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
-        d_proxy_var[n] = sk;
-        Trace("strings-assert") << "(assert " << eq << ")" << std::endl;
-        d_out->lemma(eq);
-        Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-        Node lsum;
-        if( n.getKind() == kind::STRING_CONCAT ) {
-          std::vector<Node> node_vec;
-          for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-            if( n[i].getAttribute(StringsProxyVarAttribute()) ){
-              Assert( d_proxy_var_to_length.find( n[i] )!=d_proxy_var_to_length.end() );
-              node_vec.push_back( d_proxy_var_to_length[n[i]] );
-            }else{
-              Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-              node_vec.push_back(lni);
-            }
+  //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) ));
           }
-          lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-        } else if( n.getKind() == kind::CONST_STRING ) {
-          lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-        }
-        lsum = Rewriter::rewrite( lsum );
-        d_proxy_var_to_length[sk] = lsum;
-        if( options::stringEagerLen() || n.getKind()==kind::CONST_STRING ){
-          Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) );
-          Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-          Trace("strings-lemma-debug") << "  prerewrite : " << skl.eqNode( lsum ) << std::endl;
-          Trace("strings-assert") << "(assert " << ceq << ")" << std::endl;
-          d_out->lemma(ceq);
+          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;
       }
-      return true;
+
+      sendLemma( ant, conc, "F-LOOP" );
+      ++(d_statistics.d_loop_lemmas);
+
+      //we will be done
+      addNormalFormPair( normal_form_src[i], normal_form_src[j] );
     } else {
-      AlwaysAssert(false, "String Terms only in registerTerm.");
+      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 false;
+  return true;
 }
 
-void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-  if( conc.isNull() || conc == d_false ) {
-    d_out->conflict(ant);
-    Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
-    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
-    Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
-    d_conflict = true;
-  } else {
-    Node lem;
-    if( ant == d_true ) {
-      lem = conc;
-    }else{
-      lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
-    }
-    Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
-    Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
-    d_lemma_cache.push_back( lem );
-  }
-}
+//return true for lemma, false if we succeed
+bool TheoryStrings::processDeq( Node ni, Node nj ) {
+  //Assert( areDisequal( ni, nj ) );
+  if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){
+    std::vector< Node > nfi;
+    nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
+    std::vector< Node > nfj;
+    nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
 
-void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
-  Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl;
-  eq = Rewriter::rewrite( eq );
-  if( eq==d_false || eq.getKind()==kind::OR ) {
-    sendLemma( eq_exp, eq, c );
-  }else if( eq!=d_true ){
-    if( options::stringInferSym() ){
-      std::vector< Node > vars;
-      std::vector< Node > subs;
-      std::vector< Node > unproc;
-      inferSubstitutionProxyVars( eq_exp, vars, subs, unproc );
-      if( unproc.empty() ){
-        Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
-        Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-        Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl;
-        for( unsigned i=0; i<vars.size(); i++ ){
-          Trace("strings-lemma-debug") << "  " << vars[i] << " -> " << subs[i] << std::endl;
-        }
-        sendLemma( d_true, eqs, c );
-        return;
-      }else{
-        for( unsigned i=0; i<unproc.size(); i++ ){
-          Trace("strings-lemma-debug") << "  non-trivial exp : " << unproc[i] << std::endl;
-        }
-      }
+    int revRet = processReverseDeq( nfi, nfj, ni, nj );
+    if( revRet!=0 ){
+      return revRet==-1;
     }
-    Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
-    Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
-    d_pending.push_back( eq );
-    d_pending_exp[eq] = eq_exp;
-    d_infer.push_back( eq );
-    d_infer_exp.push_back( eq_exp );
-  }
-}
-
-void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
-  Node eq = a.eqNode( b );
-  eq = Rewriter::rewrite( eq );
-  Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
-  Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
-  Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl;
-  d_lemma_cache.push_back(lemma_or);
-  d_pending_req_phase[eq] = preq;
-  ++(d_statistics.d_splits);
-}
 
+    nfi.clear();
+    nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
+    nfj.clear();
+    nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
 
-void TheoryStrings::sendLengthLemma( Node n ){
-  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-  if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
-    Node n_len_eq_z = n_len.eqNode( d_zero );
-    //registerTerm( d_emptyString );
-    Node n_len_eq_z_2 = n.eqNode( d_emptyString );
-    n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-    n_len_eq_z_2 = Rewriter::rewrite( n_len_eq_z_2 );
-    Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, n_len_eq_z, n_len_eq_z_2 ),
-                NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-    Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-    d_out->lemma(n_len_geq_zero);
-    d_out->requirePhase( n_len_eq_z, true );
-    d_out->requirePhase( n_len_eq_z_2, true );
-  }
-  //AJR: probably a good idea
-  if( options::stringLenGeqZ() ){
-    Node n_len_geq = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
-    n_len_geq = Rewriter::rewrite( n_len_geq );
-    d_out->lemma( n_len_geq );
-  }
-}
+    unsigned index = 0;
+    while( index<nfi.size() || index<nfj.size() ){
+      int ret = processSimpleDeq( nfi, nfj, ni, nj, index, false );
+      if( ret!=0 ) {
+        return ret==-1;
+      } else {
+        Assert( index<nfi.size() && index<nfj.size() );
+        Node i = nfi[index];
+        Node j = nfj[index];
+        Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
+        if( !areEqual( i, j ) ) {
+          Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
+          if( areDisequal(li, lj) ){
+            //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
 
-void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ) {
-  if( n.getKind()==kind::AND ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      inferSubstitutionProxyVars( n[i], vars, subs, unproc );
-    }
-    return;
-  }else if( n.getKind()==kind::EQUAL ){
-    Node ns = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-    ns = Rewriter::rewrite( ns );
-    if( ns.getKind()==kind::EQUAL ){
-      Node s;
-      Node v;
-      for( unsigned i=0; i<2; i++ ){
-        Node ss;
-        if( ns[i].getAttribute(StringsProxyVarAttribute()) ){
-          ss = ns[i];
-        }else if( ns[i].isConst() ){
-          NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] );
-          if( it!=d_proxy_var.end() ){
-            ss = (*it).second;
-          }
-        }
-        if( !ss.isNull() ){
-          v = ns[1-i];
-          if( v.getNumChildren()==0 ){
-            if( s.isNull() ){
-              s = ss;
+            Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
+            //must add lemma
+            std::vector< Node > antec;
+            std::vector< Node > antec_new_lits;
+            antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+            antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+            //check disequal
+            if( areDisequal( ni, nj ) ){
+              antec.push_back( ni.eqNode( nj ).negate() );
             }else{
-              //both sides involved in proxy var
-              if( ss==s ){
-                return;
-              }else{
-                s = Node::null();
-              }
+              antec_new_lits.push_back( ni.eqNode( nj ).negate() );
             }
+            antec_new_lits.push_back( li.eqNode( lj ).negate() );
+            std::vector< Node > conc;
+            Node sk1 = mkSkolemCached( i, j, sk_id_deq_x, "x_dsplit" );
+            Node sk2 = mkSkolemCached( i, j, sk_id_deq_y, "y_dsplit" );
+            Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 );
+            //Node nemp = sk3.eqNode(d_emptyString).negate();
+            //conc.push_back(nemp);
+            Node lsk1 = mkLength( sk1 );
+            conc.push_back( lsk1.eqNode( li ) );
+            Node lsk2 = mkLength( sk2 );
+            conc.push_back( lsk2.eqNode( lj ) );
+            conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
+            sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
+            ++(d_statistics.d_deq_splits);
+            return true;
+          }else if( areEqual( li, lj ) ){
+            Assert( !areDisequal( i, j ) );
+            //splitting on demand : try to make them disequal
+            Node eq = i.eqNode( j );
+            sendSplit( i, j, "S-Split(DEQL)" );
+            eq = Rewriter::rewrite( eq );
+            d_pending_req_phase[ eq ] = false;
+            return true;
+          }else{
+            //splitting on demand : try to make lengths equal
+            Node eq = li.eqNode( lj );
+            sendSplit( li, lj, "D-Split" );
+            eq = Rewriter::rewrite( eq );
+            d_pending_req_phase[ eq ] = true;
+            return true;
           }
         }
+        index++;
       }
-      if( !s.isNull() ){
-        subs.push_back( s );
-        vars.push_back( v );
-        return;
-      }
-    }else{
-      n = ns;
     }
+    Assert( false );
   }
-  if( n!=d_true ){
-    unproc.push_back( n );
-  }
-}
-
-
-Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
-  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
-}
-
-Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) {
-  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) );
+  return false;
 }
 
-Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
-  return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
-}
+int TheoryStrings::processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ) {
+  //reverse normal form of i, j
+  std::reverse( nfi.begin(), nfi.end() );
+  std::reverse( nfj.begin(), nfj.end() );
 
-Node TheoryStrings::mkLength( Node t ) {
-  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
-}
+  unsigned index = 0;
+  int ret = processSimpleDeq( nfi, nfj, ni, nj, index, true );
 
-//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" );
-  d_length_intro_vars.insert(n);
-  ++(d_statistics.d_new_skolems);
-  if(isLenSplit == 0) {
-    sendLengthLemma( n );
-    ++(d_statistics.d_splits);
-  } else if(isLenSplit == 1) {
-    d_equalityEngine.assertEquality(n.eqNode(d_emptyString), false, d_true);
-    Node len_n_gt_z = NodeManager::currentNM()->mkNode(kind::GT,
-                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n), d_zero);
-    Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z << std::endl;
-    Trace("strings-assert") << "(assert " << len_n_gt_z << ")" << std::endl;
-    d_out->lemma(len_n_gt_z);
-  }
-  return n;
-}
+  //reverse normal form of i, j
+  std::reverse( nfi.begin(), nfi.end() );
+  std::reverse( nfj.begin(), nfj.end() );
 
-Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
-  std::vector< Node > an;
-  return mkExplain( a, an );
+  return ret;
 }
 
-Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
-  std::vector< TNode > antec_exp;
-  for( unsigned i=0; i<a.size(); i++ ) {
-    if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
-      bool exp = true;
-      Debug("strings-explain") << "Ask for explanation of " << a[i] << std::endl;
-      //assert
-      if(a[i].getKind() == kind::EQUAL) {
-        //assert( hasTerm(a[i][0]) );
-        //assert( hasTerm(a[i][1]) );
-        Assert( areEqual(a[i][0], a[i][1]) );
-        if( a[i][0]==a[i][1] ){
-          exp = false;
-        }
-      } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
-        Assert( hasTerm(a[i][0][0]) );
-        Assert( hasTerm(a[i][0][1]) );
-        AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
-      }else if( a[i].getKind() == kind::AND ){
-        for( unsigned j=0; j<a[i].getNumChildren(); j++ ){
-          a.push_back( a[i][j] );
-        }
-        exp = false;
+int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ) {
+  while( index<nfi.size() || index<nfj.size() ) {
+    if( index>=nfi.size() || index>=nfj.size() ) {
+      Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
+      std::vector< Node > ant;
+      //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
+      Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] );
+      Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] );
+      ant.push_back( lni.eqNode( lnj ) );
+      ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+      ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+      std::vector< Node > cc;
+      std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
+      for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
+        cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
       }
-      if( exp ) {
-        unsigned ps = antec_exp.size();
-        explain(a[i], antec_exp);
-        Debug("strings-explain") << "Done, explanation was : " << std::endl;
-        for( unsigned j=ps; j<antec_exp.size(); j++ ) {
-          Debug("strings-explain") << "  " << antec_exp[j] << std::endl;
+      Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+      conc = Rewriter::rewrite( conc );
+      sendLemma(mkExplain( ant ), conc, "Disequality Normalize Empty");
+      //sendInfer(mkAnd( ant ), conc, "Disequality Normalize Empty");
+      return -1;
+    } else {
+      Node i = nfi[index];
+      Node j = nfj[index];
+      Trace("strings-solve-debug")  << "...Processing(QED) " << i << " " << j << std::endl;
+      if( !areEqual( i, j ) ) {
+        if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
+          unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
+          bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
+          if( isSameFix ) {
+            //same prefix/suffix
+            //k is the index of the string that is shorter
+            Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j;
+            Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i;
+            Node remainderStr;
+            if(isRev) {
+              int new_len = nl.getConst<String>().size() - len_short;
+              remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) );
+              Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
+            } else {
+              remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
+              Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
+            }
+            if( i.getConst<String>().size() < j.getConst<String>().size() ) {
+              nfj.insert( nfj.begin() + index + 1, remainderStr );
+              nfj[index] = nfi[index];
+            } else {
+              nfi.insert( nfi.begin() + index + 1, remainderStr );
+              nfi[index] = nfj[index];
+            }
+          } else {
+            return 1;
+          }
+        } else {
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
+          if( areEqual( li, lj ) && areDisequal( i, j ) ) {
+            Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
+            //we are done: D-Remove
+            return 1;
+          } else {
+            return 0;
+          }
         }
-        Debug("strings-explain") << std::endl;
       }
+      index++;
     }
   }
-  for( unsigned i=0; i<an.size(); i++ ) {
-    if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
-      Debug("strings-explain") << "Add to explanation (new literal) " << an[i] << std::endl;
-      antec_exp.push_back(an[i]);
-    }
-  }
-  Node ant;
-  if( antec_exp.empty() ) {
-    ant = d_true;
-  } else if( antec_exp.size()==1 ) {
-    ant = antec_exp[0];
-  } else {
-    ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
-  }
-  ant = Rewriter::rewrite( ant );
-  return ant;
+  return 0;
 }
 
-Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
-  std::vector< Node > au;
-  for( unsigned i=0; i<a.size(); i++ ){
-    if( std::find( au.begin(), au.end(), a[i] )==au.end() ){
-      au.push_back( a[i] );
+void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){
+  if( !isNormalFormPair( n1, n2 ) ){
+    //Assert( !isNormalFormPair( n1, n2 ) );
+    NodeList* lst;
+    NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
+    if( nf_i == d_nf_pairs.end() ){
+      if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){
+        addNormalFormPair( n2, n1 );
+        return;
+      }
+      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+                                                           ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+      d_nf_pairs.insertDataFromContextMemory( n1, lst );
+      Trace("strings-nf") << "Create cache for " << n1 << std::endl;
+    } else {
+      lst = (*nf_i).second;
     }
-  }
-  if( au.empty() ) {
-    return d_true;
-  } else if( au.size() == 1 ) {
-    return au[0];
+    Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl;
+    lst->push_back( n2 );
+    Assert( isNormalFormPair( n1, n2 ) );
   } else {
-    return NodeManager::currentNM()->mkNode( kind::AND, au );
+    Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
   }
 }
 
-void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
-  if( n.getKind()==kind::STRING_CONCAT ) {
-    for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-      if( !areEqual( n[i], d_emptyString ) ) {
-        c.push_back( n[i] );
-      }
-    }
-  } else {
-    c.push_back( n );
-  }
+bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) {
+  //TODO: modulo equality?
+  return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 );
 }
 
-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;
+bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
+    //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
+  NodeList* lst;
+  NodeListMap::iterator nf_i = d_nf_pairs.find( n1 );
+  if( nf_i != d_nf_pairs.end() ) {
+    lst = (*nf_i).second;
+    for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) {
+      Node n = *i;
+      if( n==n2 ) {
+          return true;
       }
     }
-    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;
+  }
+  return false;
+}
+
+bool TheoryStrings::registerTerm( Node n ) {
+  if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) {
+    d_registered_terms_cache.insert(n);
+    Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl;
+    if(n.getType().isString()) {
+      //register length information:
+      //  for variables, split on empty vs positive length
+      //  for concat/const, introduce proxy var and state length relation
+      if( n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
+        if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
+          sendLengthLemma( n );
+          ++(d_statistics.d_splits);
+        }
+      } else {
+        Node sk = mkSkolemS("lsym", 2);
+        StringsProxyVarAttribute spva;
+        sk.setAttribute(spva,true);
+        Node eq = Rewriter::rewrite( sk.eqNode(n) );
+        Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
+        d_proxy_var[n] = sk;
+        Trace("strings-assert") << "(assert " << eq << ")" << std::endl;
+        d_out->lemma(eq);
+        Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+        Node lsum;
+        if( n.getKind() == kind::STRING_CONCAT ) {
+          std::vector<Node> node_vec;
+          for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+            if( n[i].getAttribute(StringsProxyVarAttribute()) ){
+              Assert( d_proxy_var_to_length.find( n[i] )!=d_proxy_var_to_length.end() );
+              node_vec.push_back( d_proxy_var_to_length[n[i]] );
+            }else{
+              Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+              node_vec.push_back(lni);
+            }
           }
+          lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+        } else if( n.getKind() == kind::CONST_STRING ) {
+          lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
         }
-        if( n!=eqc ){
-          Trace( tc ) << ", from " << n;
+        lsum = Rewriter::rewrite( lsum );
+        d_proxy_var_to_length[sk] = lsum;
+        if( options::stringEagerLen() || n.getKind()==kind::CONST_STRING ){
+          Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) );
+          Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+          Trace("strings-lemma-debug") << "  prerewrite : " << skl.eqNode( lsum ) << std::endl;
+          Trace("strings-assert") << "(assert " << ceq << ")" << std::endl;
+          d_out->lemma(ceq);
         }
-        Trace( tc ) << std::endl;
       }
-    }else{
-      Trace( tc ) << std::endl;
+      return true;
+    } else {
+      AlwaysAssert(false, "String Terms only in registerTerm.");
     }
   }
-  Trace( tc ) << std::endl;
+  return false;
 }
 
-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() );
+void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
+  if( conc.isNull() || conc == d_false ) {
+    d_out->conflict(ant);
+    Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
+    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
+    Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+    d_conflict = true;
+  } else {
+    Node lem;
+    if( ant == d_true ) {
+      lem = conc;
+    }else{
+      lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
+    }
+    Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
+    Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
+    d_lemma_cache.push_back( lem );
+  }
+}
 
-            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() );
-            }
-          }
+void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
+  Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl;
+  eq = Rewriter::rewrite( eq );
+  if( eq==d_false || eq.getKind()==kind::OR ) {
+    sendLemma( eq_exp, eq, c );
+  }else if( eq!=d_true ){
+    if( options::stringInferSym() ){
+      std::vector< Node > vars;
+      std::vector< Node > subs;
+      std::vector< Node > unproc;
+      inferSubstitutionProxyVars( eq_exp, vars, subs, unproc );
+      if( unproc.empty() ){
+        Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
+        Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl;
+        for( unsigned i=0; i<vars.size(); i++ ){
+          Trace("strings-lemma-debug") << "  " << vars[i] << " -> " << subs[i] << std::endl;
+        }
+        sendLemma( d_true, eqs, c );
+        return;
+      }else{
+        for( unsigned i=0; i<unproc.size(); i++ ){
+          Trace("strings-lemma-debug") << "  non-trivial exp : " << unproc[i] << std::endl;
         }
       }
     }
+    Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
+    Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
+    d_pending.push_back( eq );
+    d_pending_exp[eq] = eq_exp;
+    d_infer.push_back( eq );
+    d_infer_exp.push_back( eq_exp );
   }
 }
 
-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 );
+void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
+  Node eq = a.eqNode( b );
+  eq = Rewriter::rewrite( eq );
+  Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq );
+  Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq );
+  Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl;
+  d_lemma_cache.push_back(lemma_or);
+  d_pending_req_phase[eq] = preq;
+  ++(d_statistics.d_splits);
+}
+
+
+void TheoryStrings::sendLengthLemma( Node n ){
+  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+  if( options::stringSplitEmp() || !options::stringLenGeqZ() ){
+    Node n_len_eq_z = n_len.eqNode( d_zero );
+    //registerTerm( d_emptyString );
+    Node n_len_eq_z_2 = n.eqNode( d_emptyString );
+    n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+    n_len_eq_z_2 = Rewriter::rewrite( n_len_eq_z_2 );
+    Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, n_len_eq_z, n_len_eq_z_2 ),
+                NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+    Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+    d_out->lemma(n_len_geq_zero);
+    d_out->requirePhase( n_len_eq_z, true );
+    d_out->requirePhase( n_len_eq_z_2, true );
+  }
+  //AJR: probably a good idea
+  if( options::stringLenGeqZ() ){
+    Node n_len_geq = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
+    n_len_geq = Rewriter::rewrite( n_len_geq );
+    d_out->lemma( n_len_geq );
+  }
+}
+
+void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ) {
+  if( n.getKind()==kind::AND ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      inferSubstitutionProxyVars( n[i], vars, subs, unproc );
+    }
+    return;
+  }else if( n.getKind()==kind::EQUAL ){
+    Node ns = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    ns = Rewriter::rewrite( ns );
+    if( ns.getKind()==kind::EQUAL ){
+      Node s;
+      Node v;
+      for( unsigned i=0; i<2; i++ ){
+        Node ss;
+        if( ns[i].getAttribute(StringsProxyVarAttribute()) ){
+          ss = ns[i];
+        }else if( ns[i].isConst() ){
+          NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] );
+          if( it!=d_proxy_var.end() ){
+            ss = (*it).second;
           }
-          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();
-              }
+        }
+        if( !ss.isNull() ){
+          v = ns[1-i];
+          if( v.getNumChildren()==0 ){
+            if( s.isNull() ){
+              s = ss;
             }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;
-                }
+              //both sides involved in proxy var
+              if( ss==s ){
+                return;
               }else{
-                if( hasProcessed() ){
-                  return Node::null();
-                }
+                s = Node::null();
               }
             }
           }
         }
       }
-      ++eqc_i;
+      if( !s.isNull() ){
+        subs.push_back( s );
+        vars.push_back( v );
+        return;
+      }
+    }else{
+      n = ns;
+    }
+  }
+  if( n!=d_true ){
+    unproc.push_back( n );
+  }
+}
+
+
+Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
+}
+
+Node TheoryStrings::mkConcat( Node n1, Node n2, Node n3 ) {
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2, n3 ) );
+}
+
+Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
+  return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
+}
+
+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" );
+  d_length_intro_vars.insert(n);
+  ++(d_statistics.d_new_skolems);
+  if(isLenSplit == 0) {
+    sendLengthLemma( n );
+    ++(d_statistics.d_splits);
+  } else if(isLenSplit == 1) {
+    d_equalityEngine.assertEquality(n.eqNode(d_emptyString), false, d_true);
+    Node len_n_gt_z = NodeManager::currentNM()->mkNode(kind::GT,
+                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n), d_zero);
+    Trace("strings-lemma") << "Strings::Lemma SK-NON-ZERO : " << len_n_gt_z << std::endl;
+    Trace("strings-assert") << "(assert " << len_n_gt_z << ")" << std::endl;
+    d_out->lemma(len_n_gt_z);
+  }
+  return n;
+}
+
+Node TheoryStrings::mkExplain( std::vector< Node >& a ) {
+  std::vector< Node > an;
+  return mkExplain( a, an );
+}
+
+Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) {
+  std::vector< TNode > antec_exp;
+  for( unsigned i=0; i<a.size(); i++ ) {
+    if( std::find( a.begin(), a.begin() + i, a[i] )==a.begin() + i ) {
+      bool exp = true;
+      Debug("strings-explain") << "Ask for explanation of " << a[i] << std::endl;
+      //assert
+      if(a[i].getKind() == kind::EQUAL) {
+        //assert( hasTerm(a[i][0]) );
+        //assert( hasTerm(a[i][1]) );
+        Assert( areEqual(a[i][0], a[i][1]) );
+        if( a[i][0]==a[i][1] ){
+          exp = false;
+        }
+      } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ) {
+        Assert( hasTerm(a[i][0][0]) );
+        Assert( hasTerm(a[i][0][1]) );
+        AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) );
+      }else if( a[i].getKind() == kind::AND ){
+        for( unsigned j=0; j<a[i].getNumChildren(); j++ ){
+          a.push_back( a[i][j] );
+        }
+        exp = false;
+      }
+      if( exp ) {
+        unsigned ps = antec_exp.size();
+        explain(a[i], antec_exp);
+        Debug("strings-explain") << "Done, explanation was : " << std::endl;
+        for( unsigned j=ps; j<antec_exp.size(); j++ ) {
+          Debug("strings-explain") << "  " << antec_exp[j] << std::endl;
+        }
+        Debug("strings-explain") << std::endl;
+      }
     }
-    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();
+  for( unsigned i=0; i<an.size(); i++ ) {
+    if( std::find( an.begin(), an.begin() + i, an[i] )==an.begin() + i ){
+      Debug("strings-explain") << "Add to explanation (new literal) " << an[i] << std::endl;
+      antec_exp.push_back(an[i]);
+    }
+  }
+  Node ant;
+  if( antec_exp.empty() ) {
+    ant = d_true;
+  } else if( antec_exp.size()==1 ) {
+    ant = antec_exp[0];
+  } else {
+    ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
+  }
+  ant = Rewriter::rewrite( ant );
+  return ant;
 }
 
-
-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;
+Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
+  std::vector< Node > au;
+  for( unsigned i=0; i<a.size(); i++ ){
+    if( std::find( au.begin(), au.end(), a[i] )==au.end() ){
+      au.push_back( a[i] );
     }
+  }
+  if( au.empty() ) {
+    return d_true;
+  } else if( au.size() == 1 ) {
+    return au[0];
+  } else {
+    return NodeManager::currentNM()->mkNode( kind::AND, au );
+  }
+}
 
-    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;
+void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
+  if( n.getKind()==kind::STRING_CONCAT ) {
+    for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+      if( !areEqual( n[i], d_emptyString ) ) {
+        c.push_back( n[i] );
       }
     }
+  }else{
+    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;
       //}
@@ -3547,149 +3867,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
       return false;
     }
   }
-  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;
-  }
+  return true;
 }
 
 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
@@ -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
-- 
2.30.2