Bug fix for theory strings related to old cycle detection code (was leading to bogus model). Minor cleanup of QCF.

4 files changed, 200 insertions, 134 deletions

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 96ea46b6b..25a62a4e8 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -271,7 +271,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
       //}
     }
     //now, generate the trigger...
-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    int matchOption = 0;
     Trigger* tr = NULL;
     if( d_is_single_trigger[ patTerms[0] ] ){
       tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 95744a651..4a5c92c7e 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -125,12 +125,12 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){

       if( quantifiers::TermDb::hasBoundVarAttr( n ) ){

         //literals

-        if( n.getKind()==APPLY_UF ){

-          flatten( n );

-        }else if( n.getKind()==EQUAL ){

+        if( n.getKind()==EQUAL ){

           for( unsigned i=0; i<n.getNumChildren(); i++ ){

             flatten( n[i] );

           }

+        }else if( MatchGen::isHandledUfTerm( n ) ){

+          flatten( n );

         }

       }

     }

@@ -496,6 +496,12 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 eqc_count[index]++;

                 Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;

                 if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){

+                  //if( currIndex==0 ){

+                  //  Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) );

+                  //  d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]];

+                  //}else{

+                  d_match_term[unassigned[r][index]] = TNode::null();

+                  //}

                   Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;

                   index++;

                 }else{

@@ -559,14 +565,11 @@ void QuantInfo::debugPrintMatch( const char * c ) {
 }

 

 

-/*

-struct MatchGenSort {

-  MatchGen * d_mg;

-  bool operator() (int i,int j) {

-    return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;

-  }

-};

-*/

+//void QuantInfo::addFuncParent( int v, Node f, int arg ) {

+//  if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){

+//    d_f_parent[v][f].push_back( arg );

+//  }

+//}

 

 MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){

   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;

@@ -580,12 +583,15 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
       d_type = typ_var;

       d_type_not = false;

       d_n = n;

+      //Node f = getOperator( n );

       for( unsigned j=0; j<d_n.getNumChildren(); j++ ){

         Node nn = d_n[j];

         Trace("qcf-qregister-debug") << "  " << d_qni_size;

         if( qi->isVar( nn ) ){

-          Trace("qcf-qregister-debug") << " is var #" << qi->d_var_num[nn] << std::endl;

-          d_qni_var_num[d_qni_size] = qi->d_var_num[nn];

+          int v = qi->d_var_num[nn];

+          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

+          d_qni_var_num[d_qni_size] = v;

+          //qi->addFuncParent( v, f, j );

         }else{

           Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

           d_qni_gterm[d_qni_size] = nn;

@@ -640,10 +646,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
       }else{

         d_type = typ_invalid;

         //literals

-        if( d_n.getKind()==APPLY_UF ){

-          Assert( qi->isVar( d_n ) );

-          d_type = typ_pred;

-        }else if( d_n.getKind()==EQUAL ){

+        if( d_n.getKind()==EQUAL ){

           for( unsigned i=0; i<2; i++ ){

             if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){

               Assert( qi->isVar( d_n[i] ) );

@@ -652,6 +655,11 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
             }

           }

           d_type = typ_eq;

+        }else if( isHandledUfTerm( d_n ) ){

+          Assert( qi->isVar( d_n ) );

+          d_type = typ_pred;

+        }else{

+          Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;

         }

       }

     }else{

@@ -812,12 +820,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }

   }else if( d_type==typ_var ){

     Assert( isHandledUfTerm( d_n ) );

-    Node f = d_n.getOperator();

+    Node f = getOperator( p, d_n );

     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;

     QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );

     if( qni!=NULL ){

       d_qn.push_back( qni );

     }

+    d_matched_basis = false;

   }else if( d_type==typ_pred || d_type==typ_eq ){

     //add initial constraint

     Node nn[2];

@@ -986,6 +995,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     //if not successful, clean up the variables you bound

     if( !success ){

       if( d_type==typ_eq || d_type==typ_pred ){

+        //clean up the constraints you added

         for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){

           if( !it->second.isNull() ){

             Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;

@@ -998,7 +1008,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         d_qni_bound_cons_var.clear();

         d_qni_bound.clear();

       }else{

-        //clean up the match : remove equalities/disequalities

+        //clean up the matches you set

         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

           Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;

           Assert( it->second<qi->getNumVars() );

@@ -1007,6 +1017,17 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         }

         d_qni_bound.clear();

       }

+      /*

+      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){

+        d_matched_basis = true;

+        Node f = getOperator( d_n );

+        TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );

+        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){

+          success = true;

+          d_qni_bound[0] = d_qni_var_num[0];

+        }

+      }

+      */

     }

     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;

     return success;

@@ -1124,7 +1145,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
         if( d_qn.size()==d_qni.size()+1 ) {

           int index = (int)d_qni.size();

           //initialize

-          Node val;

+          TNode val;

           std::map< int, int >::iterator itv = d_qni_var_num.find( index );

           if( itv!=d_qni_var_num.end() ){

             //get the representative variable this variable is equal to

@@ -1213,7 +1234,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
         //Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );

         //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;

         Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );

-        Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;

+        TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;

         Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;

         //set the match terms

         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

@@ -1260,10 +1281,10 @@ void MatchGen::setInvalid() {
 }

 

 bool MatchGen::isHandledUfTerm( TNode n ) {

-  return n.getKind()==APPLY_UF;

+  return n.getKind()==APPLY_UF;// || n.getKind()==GEQ;

 }

 

-Node MatchGen::getFunction( Node n ) {

+Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

   if( isHandledUfTerm( n ) ){

     return n.getOperator();

   }else{

@@ -1333,7 +1354,7 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
     //else if( d_effort>QuantConflictFind::effort_conflict ){

     //  ret = -1;

     //}

-  }else if( n.getKind()==APPLY_UF ){  //predicate

+  }else if( MatchGen::isHandledUfTerm( n ) ){  //predicate

     Node nn = evaluateTerm( n );

     Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;

     if( areEqual( nn, d_true ) ){

@@ -1402,7 +1423,7 @@ bool QuantConflictFind::isPropagationSet() {
 }

 

 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {

-  //if( d_effort==QuantConflictFind::effort_prop_deq ){

+  //if( d_effort==QuantConflictFind::effort_mc ){

   //  return n1==n2 || !areDisequal( n1, n2 );

   //}else{

   return n1==n2;

@@ -1449,17 +1470,18 @@ Node QuantConflictFind::getRepresentative( Node n ) {
 }

 Node QuantConflictFind::evaluateTerm( Node n ) {

   if( MatchGen::isHandledUfTerm( n ) ){

+    Node f = MatchGen::getOperator( this, n );

     Node nn;

     if( getEqualityEngine()->hasTerm( n ) ){

       computeArgReps( n );

-      nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );

+      nn = d_uf_terms[f].existsTerm( n, d_arg_reps[n] );

     }else{

       std::vector< TNode > args;

       for( unsigned i=0; i<n.getNumChildren(); i++ ){

         Node c = evaluateTerm( n[i] );

         args.push_back( c );

       }

-      nn = d_uf_terms[n.getOperator()].existsTerm( n, args );

+      nn = d_uf_terms[f].existsTerm( n, args );

     }

     if( !nn.isNull() ){

       Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;

@@ -1612,7 +1634,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         debugPrint("qcf-debug");

         Trace("qcf-debug") << std::endl;

       }

-      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;

+      short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc;

       for( short e = effort_conflict; e<=end_e; e++ ){

         d_effort = e;

         if( e == effort_prop_eq ){

@@ -1706,7 +1728,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);

         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);

         if( addedLemmas>0 ){

-          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );

+          Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );

           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;

         }

         Trace("qcf-engine") << std::endl;

@@ -1734,6 +1756,7 @@ void QuantConflictFind::computeRelevantEqr() {
   d_uf_terms.clear();

   d_eqc_uf_terms.clear();

   d_eqcs.clear();

+  d_model_basis.clear();

   d_arg_reps.clear();

   double clSet = 0;

   if( Trace.isOn("qcf-opt") ){

@@ -1751,7 +1774,27 @@ void QuantConflictFind::computeRelevantEqr() {
   while( !eqcs_i.isFinished() ){

     nEqc++;

     Node r = (*eqcs_i);

-    d_eqcs[r.getType()].push_back( r );

+    TypeNode rtn = r.getType();

+    if( options::qcfMode()==QCF_MC ){

+      std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );

+      if( itt==d_eqcs.end() ){

+        Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );

+        if( !getEqualityEngine()->hasTerm( mb ) ){

+          Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;

+          Assert( false );

+        }

+        Node mbr = getRepresentative( mb );

+        if( mbr!=r ){

+          d_eqcs[rtn].push_back( mbr );

+        }

+        d_eqcs[rtn].push_back( r );

+        d_model_basis[rtn] = mb;

+      }else{

+        itt->second.push_back( r );

+      }

+    }else{

+      d_eqcs[rtn].push_back( r );

+    }

     //EqcInfo * eqcir = getEqcInfo( r, false );

     //get relevant nodes that we are disequal from

     /*

@@ -1786,12 +1829,13 @@ void QuantConflictFind::computeRelevantEqr() {
         std::map< TNode, std::vector< TNode > >::iterator it_na;

         TNode fn;

         if( MatchGen::isHandledUfTerm( n ) ){

+          Node f = MatchGen::getOperator( this, n );

           computeArgReps( n );

           it_na = d_arg_reps.find( n );

           Assert( it_na!=d_arg_reps.end() );

-          Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );

+          Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );

           isRedundant = (nadd!=n);

-          d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );

+          d_uf_terms[f].addTerm( n, d_arg_reps[n] );

         }else{

           isRedundant = false;

         }

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 2663ff0b9..80e56acbd 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -65,6 +65,7 @@ private:
   std::map< int, int > d_qni_bound_cons_var;

   std::map< int, int >::iterator d_binding_it;

   //std::vector< int > d_independent;

+  bool d_matched_basis;

   bool d_binding;

   //int getVarBindingVar();

   std::map< int, Node > d_ground_eval;

@@ -99,7 +100,7 @@ public:
 

   // is this term treated as UF application?

   static bool isHandledUfTerm( TNode n );

-  static Node getFunction( Node n );

+  static Node getOperator( QuantConflictFind * p, Node n );

 };

 

 //info for quantifiers

@@ -139,6 +140,9 @@ public:
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );

   void debugPrintMatch( const char * c );

   bool isConstrainedVar( int v );

+//public: //optimization : relevant domain

+  //std::map< int, std::map< Node, std::vector< int > > > d_f_parent;

+  //void addFuncParent( int v, Node f, int arg );

 };

 

 class QuantConflictFind : public QuantifiersModule

@@ -195,6 +199,7 @@ private:  //for equivalence classes
   QcfNodeIndex * getQcfNodeIndex( Node f );

   // type -> list(eqc)

   std::map< TypeNode, std::vector< TNode > > d_eqcs;

+  std::map< TypeNode, Node > d_model_basis;

   //mapping from UF terms to representatives of their arguments

   std::map< TNode, std::vector< TNode > > d_arg_reps;

   //compute arg reps

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 58344964c..4fa37a732 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -62,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
-	
+
 	d_all_warning = true;
 	d_regexp_incomplete = false;
 	d_opt_regexp_gcd = true;
@@ -285,7 +285,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	}
 	////step 2 : assign arbitrary values for unknown lengths?
 	//for( unsigned i=0; i<col.size(); i++ ){
-	//	if( 
+	//	if(
 	//}
 	Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
 	//step 3 : assign values to equivalence classes that are pure variables
@@ -307,13 +307,13 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 			}
 		}
 		Trace("strings-model") << "have length " << lts_values[i] << std::endl;
-		
+
 		//assign a new length if necessary
 		if( !pure_eq.empty() ){
 			if( lts_values[i].isNull() ){
 				unsigned lvalue = 0;
 				while( values_used.find( lvalue )!=values_used.end() ){
-					lvalue++;	
+					lvalue++;
 				}
 				Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
 				lts_values[i] = NodeManager::currentNM()->mkConst( Rational( lvalue ) );
@@ -423,7 +423,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		  d_out->requirePhase( n_len_eq_z, true );
 	  }
 	  // FMF
-	  if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && 
+	  if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&
 		  if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) {
 			  d_in_vars.push_back( n );
 		  }
@@ -673,29 +673,34 @@ void TheoryStrings::doPendingLemmas() {
 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( 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;
+  // EqcItr
+  eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+  while( !eqc_i.isFinished() ) {
+    Node n = (*eqc_i);
+    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 );
-                }
-            } 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 = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
-                    if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
-                        return true;
-                    }
+      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;
+          bool nresult = false;
+          if( nr==eqc ){
+            nf_temp.push_back( nr );
+          }else{
+            nresult = normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp );
+            if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) {
+                return true;
+            }
+          }
 					//successfully computed normal form
 					if( nf.size()!=1 || nf[0]!=d_emptyString ) {
 						for( unsigned r=0; r<nf_temp.size(); r++ ) {
@@ -715,7 +720,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 						nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) );
 					}
 					if( !nresult ){
-						//Trace("strings-process-debug") << "....Caused already asserted 
+						//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] );
@@ -726,62 +731,66 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 							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 ) );
                 }
+                ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
+                std::vector< Node > cc;
+                for( unsigned j=0; j<nf_n.size(); j++ ){
+                  if( i!=j ){
+                    cc.push_back( nf_n[j].eqNode( d_emptyString ) );
+                  }
+                }
+                std::vector< Node > empty_vec;
+                Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
+                sendLemma( mkExplain( ant ), conc, "CYCLE" );
+                return true;
+              }
             }
-			if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ) {
-				if( nf_n.size()>1 ){
-					Trace("strings-process-debug") << "Check for cycle lemma for normal form "; 
-					printConcat(nf_n,"strings-process-debug");
-					Trace("strings-process-debug") << "..." << std::endl;
-					for( unsigned i=0; i<nf_n.size(); i++ ){
-						//if a component is equal to whole,
-						if( areEqual( nf_n[i], n ) ){
-							//all others must be empty
-							std::vector< Node > ant;
-							if( nf_n[i]!=n ){
-								ant.push_back( nf_n[i].eqNode( n ) );
-							}
-							ant.insert( ant.end(), nf_exp_n.begin(), nf_exp_n.end() );
-							std::vector< Node > cc;
-							for( unsigned j=0; j<nf_n.size(); j++ ){
-								if( i!=j ){
-									cc.push_back( nf_n[j].eqNode( d_emptyString ) );
-								}
-							}
-							std::vector< Node > empty_vec;
-							Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
-							sendLemma( mkExplain( ant ), conc, "CYCLE" );
-							return true;
-						}
-					}
-				}
-				if( !result ) {
-					//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 = nn.eqNode( eqc );
-					sendLemma( mkExplain( ant ), conc, "CYCLE-T" );
-					return true;
-				}
-			}
+          }
+          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 = nn.eqNode( eqc );
+            sendLemma( mkExplain( ant ), conc, "CYCLE-T" );
+            return true;
+          }
         }
-        ++eqc_i;
+      //}
     }
+    ++eqc_i;
+  }
 
     // Test the result
     if( !normal_forms.empty() ) {
@@ -805,6 +814,14 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
             }
             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;
 }
@@ -831,7 +848,7 @@ void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
 }
 
 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
-								int i, int j, int index_i, int index_j, 
+								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 ) {
@@ -859,7 +876,7 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
 	}
 }
 //xs(zy)=t(yz)xr
-bool TheoryStrings::processLoop(std::vector< Node > &antec, 
+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,
@@ -867,7 +884,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 	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) {
@@ -945,7 +962,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 				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], 
+				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;
@@ -963,13 +980,13 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 				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 ) );
-				str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, 
+				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, mkConcat( sk_z, sk_y ) ) ) );
-				
+
 				//Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
 				//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString));
-				
+
 				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);
@@ -1042,7 +1059,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 						//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[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 );
@@ -1071,7 +1088,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 									if(options::stringLB() == 0) {
 										flag_lb = true;
 									} else {
-										if(processLoop(c_lb_exp, normal_forms, normal_form_src, 
+										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;
 										}
@@ -1147,7 +1164,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 		}
 	}
 	if(flag_lb) {
-		if(processLoop(c_lb_exp, normal_forms, normal_form_src, 
+		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;
 		}
@@ -1229,7 +1246,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
 									temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
 					sendInfer( eq_exp, eq, "LengthEq" );
 					return true;
-				} else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
+				} 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;
@@ -1388,7 +1405,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 		if( revRet!=0 ){
 			return revRet==-1;
 		}
-		
+
 		nfi.clear();
 		nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
 		nfj.clear();
@@ -1410,7 +1427,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 					Node lj = getLength( j );
 					if( areDisequal(li, lj) ){
 						//if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
-			
+
 						Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
 						//must add lemma
 						std::vector< Node > antec;
@@ -1436,7 +1453,7 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
 						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;
@@ -1771,7 +1788,7 @@ bool TheoryStrings::checkSimple() {
 								Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
 								Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
 								d_statistics.d_new_skolems += 2;
-								Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
+								Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
 													NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
 								Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
 								Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
@@ -1786,7 +1803,7 @@ bool TheoryStrings::checkSimple() {
 								Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
 								Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
 								d_statistics.d_new_skolems += 2;
-								Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+								Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
 													NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
 													NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
 								Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
@@ -2244,7 +2261,7 @@ bool TheoryStrings::unrollStar( Node atom ) {
 		}
 
 		//|x|>|xp|
-		Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, 
+		Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT,
 								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
 								NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) );
 
@@ -2398,7 +2415,7 @@ bool TheoryStrings::checkNegContains() {
 		argTypes.push_back(NodeManager::currentNM()->stringType());
 		argTypes.push_back(NodeManager::currentNM()->integerType());
 		argTypes.push_back(NodeManager::currentNM()->integerType());
-		d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", 
+		d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
 							NodeManager::currentNM()->mkFunctionType(
 								argTypes, NodeManager::currentNM()->stringType()),
 							"uf substr",
@@ -2597,7 +2614,7 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 					//add the others as lemmas
 					sendLemma( d_true, sdc[i], "RegExp-DEF");
 				}
-				
+
 				conc = sdc[0];
 			}
 		}
@@ -2683,7 +2700,7 @@ Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node
 		d_var_split_graph_lhs[sk] = lhs;
 		d_var_split_graph_rhs[sk] = rhs;
 		//d_var_split_eq[sk] = eq;
-		
+
 		//int mpl = getMaxPossibleLength( sk );
 		Trace("strings-progress") << "Strings::Progress: Because of " << eq << std::endl;
 		Trace("strings-progress") << "Strings::Progress: \t" << lhs << "(up:" << getMaxPossibleLength(lhs) << ") is removed" << std::endl;