removes unsound cases, adds unrolling

9 files changed, 379 insertions, 124 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8af543039..c84046570 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1619,15 +1619,15 @@ BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
 //STRING
-STRCST_TOK : 'str.const';
+//STRCST_TOK : 'str.cst';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
+//STRSUB_TOK : 'str.sub' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
-//STRSUB_TOK : 'str.sub' ;
 RECON_TOK : 're.++';
 REOR_TOK : 're.or';
-REINTER_TOK : 're.inter';
+REINTER_TOK : 're.itr';
 RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e1dc3531e..15c0f86e8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
 #include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2855,6 +2856,14 @@ void SmtEnginePrivate::processAssertions() {
 
   // Assertions ARE guaranteed to be rewritten by this point
 
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ){
+	CVC4::theory::strings::StringsPreprocess sp;
+	sp.simplify( d_assertionsToPreprocess );
+    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+		d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+	}
+  }
+
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){
     //apply pre-skolemization to existential quantifiers
diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
index 15bd04b88..38efa33f3 100644
--- a/src/theory/strings/Makefile.am
+++ b/src/theory/strings/Makefile.am
@@ -11,7 +11,9 @@ libstrings_la_SOURCES = \
 	theory_strings_rewriter.h \
 	theory_strings_rewriter.cpp \
 	theory_strings_type_rules.h \
-	type_enumerator.h
+	type_enumerator.h \
+	theory_strings_preprocess.h \
+	theory_strings_preprocess.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/strings/options b/src/theory/strings/options
index c90d654b1..9226f9999 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,7 +5,7 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality str-cardinality --str-cardinality=N int16_t :default 256 :read-write
+option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
  the cardinality of the characters used by the theory of string, default 256
 
 endmodule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index df55bcf83..f9bb74486 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,6 +26,8 @@
 #include "theory/strings/type_enumerator.h"
 #include <cmath>
 
+#define STR_UNROLL_INDUCTION
+
 using namespace std;
 using namespace CVC4::context;
 
@@ -44,7 +46,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_ind_map1(c),
     d_ind_map2(c),
     d_ind_map_exp(c),
-    d_ind_map_lemma(c)
+    d_ind_map_lemma(c),
+	//d_lit_to_decide_index( c, 0 ),
+	//d_lit_to_decide( c ),
+	d_lit_to_unroll( c )
 {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
@@ -63,6 +68,14 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+Node TheoryStrings::getRepresentative( Node t ) {
+	if( d_equalityEngine.hasTerm( t ) ){
+		return d_equalityEngine.getRepresentative( t );
+	}else{
+		return t;
+	}
+}
+
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -182,7 +195,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
             Node cst = ei ? ei->d_const_term : Node::null();
 			if( cst.isNull() ){
 				Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
-				if( d_normal_forms[col[i][j]].size()==1 && d_normal_forms[col[i][j]][0]==col[i][j] ){
+				if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
 					pure_eq.push_back( col[i][j] );
 				}
 			}else{
@@ -218,10 +231,21 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 	for( unsigned i=0; i<nodes.size(); i++ ){
 		if( processed.find( nodes[i] )==processed.end() ){
 			Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
+			Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
+			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
+				if( j>0 ) Trace("strings-model") << " ++ ";
+				Trace("strings-model") << d_normal_forms[nodes[i]][j];
+				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+				if( !r.isConst() && processed.find( r )==processed.end() ){
+					Trace("strings-model") << "(UNPROCESSED)";
+				}
+			}
+			Trace("strings-model") << std::endl;
 			std::vector< Node > nc;
 			for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
-				Assert( processed.find( d_normal_forms[nodes[i]][j] )!=processed.end() );
-				nc.push_back(processed[d_normal_forms[nodes[i]][j]]);
+				Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+				Assert( r.isConst() || processed.find( r )!=processed.end() );
+				nc.push_back(r.isConst() ? r : processed[r]);
 			}
 			Node cc = mkConcat( nc );
 			Assert( cc.getKind()==kind::CONST_STRING );
@@ -295,33 +319,16 @@ void TheoryStrings::check(Effort e) {
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
-      //head
-      //if(atom[0].getKind() == kind::CONST_STRING) {
-          //if(atom[1].getKind() == kind::STRING_CONCAT) {
-          //}
-      //}
-      //tail
       d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
-    switch(atom.getKind()) {
-        case kind::EQUAL:
-            if(polarity) {
-                //if(atom[0].isString() && atom[1].isString()) {
-                    //dealPositiveWordEquation(atom);
-                //}
-            } else {
-                // TODO: Word Equation negaitive
-            }
-            break;
-        case kind::STRING_IN_REGEXP:
-            // TODO: membership
-            break;
-        default:
-            //possibly error
-            break;
-    }
+#ifdef STR_UNROLL_INDUCTION
+	//check if it is a literal to unroll?
+	if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){
+		Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl;
+	}
+#endif
   }
   doPendingFacts();
 
@@ -607,9 +614,11 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
         //nf.push_back( eqc );
         if( eqc.getKind()==kind::STRING_CONCAT ){
             for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-                nf.push_back( eqc[i] );
+				if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
+					nf.push_back( eqc[i] );
+				}
             }
-        }else{
+        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){
             nf.push_back( eqc );
         }
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
@@ -665,7 +674,10 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
                                 //add loop equations that we've accumulated
                                 for( unsigned r=0; r<loop_eqs_x.size(); r++ ){
-                                    addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] );
+                                    if( addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r], "Discovered Loop Induction" ) ){
+										//added a lemma, we are done
+										return;
+									}
                                 }
                             }else{
                                 //the remainder must be empty
@@ -684,7 +696,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
                                     Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
 									Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
-                                    //d_equalityEngine.assertEquality( eq, true, eq_exp );
                                     d_pending.push_back( eq );
                                     d_pending_exp[eq] = eq_exp;
                                     d_infer.push_back(eq);
@@ -737,8 +748,29 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     d_infer.push_back(eq);
                                     d_infer_exp.push_back(eq_exp);
                                     return;
-                                }else{
-                                    Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl;
+								}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") << "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 > antec_new_lits;
+									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++ ){
+											eqnc.push_back( normal_forms[k][index_l] );
+										}
+										eqn.push_back( mkConcat( eqnc ) );
+									}
+									conc = eqn[0].eqNode( eqn[1] );
+									Node ant = mkExplain( antec, antec_new_lits );
+									sendLemma( ant, conc, "Endpoint" );
+									return;
+								}else{
+                                    Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
                                     Node conc;
                                     std::vector< Node > antec;
                                     std::vector< Node > antec_new_lits;
@@ -787,7 +819,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										}
 										term_s = mkConcat( sc );
 										Trace("strings-loop") << "Find y,z from t,s = " << term_t << ", " << term_s << std::endl;
-										/*TODO: incomplete start */
+										/*TODO: incomplete start 
 										if( term_t==term_s ){
 											found_size_y = -2;
 										}else if( term_t.getKind()==kind::STRING_CONCAT && term_s.getKind()==kind::STRING_CONCAT ){
@@ -820,12 +852,12 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												}
 											}
 										}
-										/*TODO: end incomplete*/
+										TODO: end incomplete*/
                                         if( found_size_y==-1 ){
 											Trace("strings-loop") << "Must add lemma." << std::endl;
                                             //need to break
-                                            Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
-                                            Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+                                            Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+                                            Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
 
                                             antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
                                             //t1 * ... * tn = y * z
@@ -864,31 +896,16 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											//Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
 											//						NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
 											//						sk_y_len );
-                                            //Node sk_x_rest = NodeManager::currentNM()->mkSkolem( "ldissym_$$", normal_forms[i][index_i].getType(), "created for induction" );
-											//Node x_eq_y_rest = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], 
-											//						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_x_rest ) );
-											
+											Node ant = mkExplain( antec, antec_new_lits );
 											conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+
 											//Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
 											//conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
 
-                                            
-											Node loop_x = normal_forms[other_n_index][other_index];
-											Node loop_y = sk_y;
-											Node loop_z = sk_z;
-
-											//Node loop_x = sk_x_rest;
-											//std::vector< Node > skc;
-											//skc.push_back( sk_y );
-											//skc.push_back( sk_z );
-                                            //Node loop_y = d_emptyString;
-                                            //Node loop_z = mkConcat( skc );
-
                                             //we will be done
                                             addNormalFormPair( normal_form_src[i], normal_form_src[j] );
-											Node ant = mkExplain( antec, antec_new_lits );
 											sendLemma( ant, conc, "Loop" );
-											addInductiveEquation( loop_x, loop_y, loop_z, ant );
+											addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
 											return;
                                         } else {
 											// x = (yz)*y
@@ -970,30 +987,16 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             } else {
                                                 Assert( other_str.getKind()!=kind::STRING_CONCAT );
                                                 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-												if( nconst_index_k==normal_forms[nconst_k].size()-1 ){
-													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++ ){
-															eqnc.push_back( normal_forms[k][index_l] );
-														}
-														eqn.push_back( mkConcat( eqnc ) );
-													}
-													conc = eqn[0].eqNode( eqn[1] );
-												}else{
-													Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-														NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-													//split the string
-													Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
-
-													Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
-													Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
-																NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
-													Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
-													conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-												}
+												Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+													NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+												//split the string
+												Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
+
+												Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
+												Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+															NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+												Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
+												conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
                                                 Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
 
 												Node ant = mkExplain( antec, antec_new_lits );
@@ -1002,25 +1005,26 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             }
                                         }else{
                                             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);
-                                            }
-                                            Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
-                                            Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
-                                                        NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
-                                            Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
-                                                        NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
-                                            conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                            // |sk| > 0
-                                            //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                            //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
+
+											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);
+											}
+											Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
+											Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
+														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) );
+											Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
+														NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
+											conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+											// |sk| > 0
+											//Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+											//Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
 											Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
-                                            Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
-                                            //d_out->lemma(sk_gt_zero);
-                                            d_lemma_cache.push_back( sk_gt_zero );
+											Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
+											//d_out->lemma(sk_gt_zero);
+											d_lemma_cache.push_back( sk_gt_zero );
 
 											Node ant = mkExplain( antec, antec_new_lits );
 											sendLemma( ant, conc, "Split" );
@@ -1120,8 +1124,39 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
   return false;
 }
 
-void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
+bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) {
     Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
+#ifdef STR_UNROLL_INDUCTION
+	Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" );
+	Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, 
+							NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) );
+	Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w );
+	Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+	d_lemma_cache.push_back( lem );
+
+	//add initial induction
+	Node lit1 = w.eqNode( d_emptyString );
+	lit1 = Rewriter::rewrite( lit1 );
+	Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" );
+	Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) );
+	lit2 = Rewriter::rewrite( lit2 );
+	Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 );
+	Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+	Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+	d_lemma_cache.push_back( split_lem );
+
+	//d_lit_to_decide.push_back( lit1 );
+	d_lit_to_unroll[lit2] = true;
+	d_pending_req_phase[lit1] = true;
+	d_pending_req_phase[lit2] = false;
+
+	x = w;
+	std::vector< Node > skc;
+	skc.push_back( y );
+	skc.push_back( z );
+	y = d_emptyString;
+	z = mkConcat( skc );
+#endif
 
     NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
     NodeList* lst1;
@@ -1157,6 +1192,11 @@ void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
     lst1->push_back( y );
     lst2->push_back( z );
     lste->push_back( exp );
+#ifdef STR_UNROLL_INDUCTION
+	return true;
+#else
+	return false;
+#endif
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
@@ -1268,6 +1308,7 @@ bool TheoryStrings::checkNormalForms() {
 
   bool addedFact = false;
   do {
+	  Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
     d_normal_forms_exp.clear();
@@ -1275,11 +1316,12 @@ bool TheoryStrings::checkNormalForms() {
     std::map< Node, Node > eqc_to_exp;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       d_lemma_cache.clear();
+	   d_pending_req_phase.clear();
       while( !eqcs_i.isFinished() ){
         Node eqc = (*eqcs_i);
         //if eqc.getType is string
         if (eqc.getType().isString()) {
-            Trace("strings-process") << "Verify normal forms are the same for " << eqc << std::endl;
+            Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
             std::vector< Node > visited;
             std::vector< Node > nf;
             std::vector< Node > nf_exp;
@@ -1319,16 +1361,25 @@ bool TheoryStrings::checkNormalForms() {
         }
         ++eqcs_i;
       }
+	  Trace("strings-nf-debug") << "**** 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-debug") << "  normal_form(" << it->second << ") = " << it->first << std::endl;
+	  }
+	  Trace("strings-nf-debug") << std::endl;
       addedFact = !d_pending.empty();
       doPendingFacts();
       if( !d_conflict ){
-          for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
-              Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
-              d_out->lemma( d_lemma_cache[i] );
-          }
           if( !d_lemma_cache.empty() ){
-            d_lemma_cache.clear();
-            return true;
+			  for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
+				  Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
+				  d_out->lemma( d_lemma_cache[i] );
+			  }
+			  for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
+				d_out->requirePhase( it->first, it->second );
+			  }
+			d_lemma_cache.clear();
+		    d_pending_req_phase.clear();
+			return true;
           }
       }
   } while (!d_conflict && addedFact);
@@ -1428,6 +1479,7 @@ bool TheoryStrings::checkInductiveEquations() {
     Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
     for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
         Node x = (*it).first;
+		Trace("strings-ind-debug") << "Check eq for " << x << std::endl;
         NodeList* lst1 = (*it).second;
         NodeList* lst2 = (*d_ind_map2.find(x)).second;
         NodeList* lste = (*d_ind_map_exp.find(x)).second;
@@ -1439,21 +1491,25 @@ bool TheoryStrings::checkInductiveEquations() {
         while( i1!=lst1->end() ){
             Node y = *i1;
             Node z = *i2;
+			//Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl;
             //if( il==lstl->end() ) {
 				std::vector< Node > nf_y, nf_z, exp_y, exp_z;
 				
-				getFinalNormalForm( y, nf_y, exp_y);
-				getFinalNormalForm( z, nf_z, exp_z);
-				std::vector< Node > vec_empty;
-				Node nexp_y = mkExplain( exp_y, vec_empty );
-				Node nexp_z = mkExplain( exp_z, vec_empty );
+				//getFinalNormalForm( y, nf_y, exp_y);
+				//getFinalNormalForm( z, nf_z, exp_z);
+				//std::vector< Node > vec_empty;
+				//Node nexp_y = mkExplain( exp_y, vec_empty );
+				//Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl;
+				//Node nexp_z = mkExplain( exp_z, vec_empty );
 
-				Node exp = *ie;
+				//Node exp = *ie;
+				//Trace("strings-ind-debug") << "Check exp=" << exp << std::endl;
 
-				exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
-				exp = Rewriter::rewrite( exp );
+				//exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
+				//exp = Rewriter::rewrite( exp );
 
-				Trace("strings-ind") << "Inductive equation : " << x << " = ( ";
+				Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl;
+				/*
 				for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
 					Trace("strings-ind") << (*itr) << " ";
 				}
@@ -1466,6 +1522,7 @@ bool TheoryStrings::checkInductiveEquations() {
 					Trace("strings-ind") << (*itr) << " ";
 				}
 				Trace("strings-ind") << std::endl;
+				*/
 				/*
 				Trace("strings-ind") << "Explanation is : " << exp << std::endl;
 				std::vector< Node > nf_yz;
@@ -1520,12 +1577,17 @@ bool TheoryStrings::checkInductiveEquations() {
             ++i2;
             ++ie;
             //++il;
-            hasEq = true;
+			if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){
+				hasEq = true;
+			}
         }
     }
     if( hasEq ){
+		Trace("strings-ind") << "It is incomplete." << std::endl;
         d_out->setIncomplete();
-    }
+    }else{
+		Trace("strings-ind") << "We can answer SAT." << std::endl;
+	}
   return false;
 }
 
@@ -1601,7 +1663,18 @@ void TheoryStrings::seperateIntoCollections( std::vector< Node >& n, std::vector
   }
 }
 
-
+/*
+Node TheoryStrings::getNextDecisionRequest() {
+	if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
+		Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
+		d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
+		Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
+		return l;
+	}else{
+		return Node::null();
+	}
+}
+*/
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 92cf33de2..2385386ea 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -36,6 +36,7 @@ namespace strings {
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   public:
 
   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -45,7 +46,7 @@ class TheoryStrings : public Theory {
 
   std::string identify() const { return std::string("TheoryStrings"); }
 
-
+  Node getRepresentative( Node t );
   public:
 
   void propagate(Effort e);
@@ -122,6 +123,8 @@ class TheoryStrings : public Theory {
       std::map< Node, Node > d_pending_exp;
       std::vector< Node > d_pending;
       std::vector< Node > d_lemma_cache;
+	  std::map< Node, bool > d_pending_req_phase;
+
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   /** inferences */
@@ -137,7 +140,11 @@ class TheoryStrings : public Theory {
   NodeListMap d_ind_map2;
   NodeListMap d_ind_map_exp;
   NodeListMap d_ind_map_lemma;
-  void addInductiveEquation( Node x, Node y, Node z, Node exp );
+  bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c );
+
+  //for unrolling inductive equations
+  NodeBoolMap d_lit_to_unroll;
+
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
new file mode 100644
index 000000000..d62fd4c9e
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -0,0 +1,120 @@
+/*********************                                                        */

+/*! \file theory_strings_preprocess.cpp

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: Tianyi Liang, Andrew Reynolds

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2013-2013  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Strings Preprocess

+ **

+ ** Strings Preprocess.

+ **/

+

+#include "theory/strings/theory_strings_preprocess.h"

+#include "expr/kind.h"

+

+namespace CVC4 {

+namespace theory {

+namespace strings {

+

+void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {

+	int k = r.getKind();

+	switch( k ) {

+		case kind::STRING_TO_REGEXP:

+		{

+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );

+			ret.push_back( eq );

+		}

+			break;

+		case kind::REGEXP_CONCAT:

+		{

+			std::vector< Node > cc;

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

+				Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );

+				simplifyRegExp( sk, r[i], ret );

+				cc.push_back( sk );

+			}

+			Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, 

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );

+			ret.push_back( cc_eq );

+		}

+			break;

+		case kind::REGEXP_OR:

+		{

+			std::vector< Node > c_or;

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

+				simplifyRegExp( s, r[i], c_or );

+			}

+			Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );

+			ret.push_back( eq );

+		}

+			break;

+		case kind::REGEXP_INTER:

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

+				simplifyRegExp( s, r[i], ret );

+			}

+			break;

+		case kind::REGEXP_STAR:

+		{

+			Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );

+			Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),

+						NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));

+			ret.push_back( eq );

+			simplifyRegExp( sk, r[0], ret );

+		}

+			break;

+		case kind::REGEXP_OPT:

+		{

+			Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );

+			std::vector< Node > rr;

+			simplifyRegExp( s, r[0], rr );

+			Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );

+			ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );

+		}

+			break;

+		default:

+			//TODO:case kind::REGEXP_PLUS:

+			//TODO: special sym: sigma, none, all

+			break;

+	}

+}

+

+Node StringsPreprocess::simplify( Node t ) {

+	if( t.getKind() == kind::STRING_IN_REGEXP ){

+		// t0 in t1

+		//rewrite it

+		std::vector< Node > ret;

+		simplifyRegExp( t[0], t[1], ret );

+

+		return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );

+    }else if( t.getNumChildren()>0 ){

+		std::vector< Node > cc;

+		if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

+			cc.push_back(t.getOperator());

+		}

+		bool changed = false;

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

+			Node tn = simplify( t[i] );

+			cc.push_back( tn );

+			changed = changed || tn!=t[i];

+		}

+		return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;

+	}else{

+		return t;

+	}

+}

+

+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {

+	for( unsigned i=0; i<vec_node.size(); i++ ){

+		vec_node[i] = simplify( vec_node[i] );

+	}

+}

+

+}/* CVC4::theory::strings namespace */

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
new file mode 100644
index 000000000..2b2e7dfea
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -0,0 +1,41 @@
+/*********************                                                        */

+/*! \file theory_strings_preprocess.h

+ ** \verbatim

+ ** Original author: Tianyi Liang

+ ** Major contributors: Tianyi Liang, Andrew Reynolds

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2013-2013  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Strings Preprocess

+ **

+ ** Strings Preprocess.

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H

+#define __CVC4__THEORY__STRINGS__PREPROCESS_H

+

+#include <vector>

+#include "theory/theory.h"

+

+namespace CVC4 {

+namespace theory {

+namespace strings {

+

+class StringsPreprocess {

+private:

+	void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );

+	Node simplify( Node t );

+public:

+void simplify(std::vector< Node > &vec_node);

+};

+

+}/* CVC4::theory::strings namespace */

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

+

+#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index bf284ea7b..9c3d6c71e 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -181,6 +181,9 @@ public:
     if (!t.isString()) {
       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
     }
+	if( (*it).getKind() != kind::CONST_STRING ) {
+      throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+	}
     if(++it != it_end) {
       throw TypeCheckingExceptionPrivate(n, "too many terms");
     }