length lemma is changed, var-split lemma is changed

3 files changed, 347 insertions, 330 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index fa686dd9f..a3921bb42 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -237,7 +237,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 							vec_nodes.push_back( dc );

 						}

 					}

-					Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << (dc.isNull() ?  "NULL" : mkString(dc) ) << std::endl;

+					Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;

 				}

 				retNode = vec_nodes.size() == 0 ? Node::null() :

 							( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );

@@ -321,7 +321,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 		}

 		d_dv_cache[dv] = retNode;

 	}

-	Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) )  << std::endl;

+	Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode ) << std::endl;

 	return retNode;

 }

 

@@ -577,79 +577,83 @@ std::string RegExpOpr::niceChar( Node r ) {
 }

 std::string RegExpOpr::mkString( Node r ) {

 	std::string retStr;

-	int k = r.getKind();

-	switch( k ) {

-		case kind::STRING_TO_REGEXP:

-		{

-			retStr += niceChar( r[0] );

-		}

-			break;

-		case kind::REGEXP_CONCAT:

-		{

-			retStr += "(";

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

-				if(i != 0) retStr += ".";

-				retStr += mkString( r[i] );

+	if(r.isNull()) {

+		retStr = "EmptySet";

+	} else {

+		int k = r.getKind();

+		switch( k ) {

+			case kind::STRING_TO_REGEXP:

+			{

+				retStr += niceChar( r[0] );

 			}

-			retStr += ")";

-		}

-			break;

-		case kind::REGEXP_OR:

-		{

-			if(r == d_sigma) {

-				retStr += "{A}";

-			} else {

+				break;

+			case kind::REGEXP_CONCAT:

+			{

 				retStr += "(";

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

-					if(i != 0) retStr += "|";

+					if(i != 0) retStr += ".";

 					retStr += mkString( r[i] );

 				}

 				retStr += ")";

 			}

-		}

-			break;

-		case kind::REGEXP_INTER:

-		{

-			retStr += "(";

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

-				if(i != 0) retStr += "&";

-				retStr += mkString( r[i] );

+				break;

+			case kind::REGEXP_OR:

+			{

+				if(r == d_sigma) {

+					retStr += "{A}";

+				} else {

+					retStr += "(";

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

+						if(i != 0) retStr += "|";

+						retStr += mkString( r[i] );

+					}

+					retStr += ")";

+				}

 			}

-			retStr += ")";

-		}

-			break;

-		case kind::REGEXP_STAR:

-		{

-			retStr += mkString( r[0] );

-			retStr += "*";

-		}

-			break;

-		case kind::REGEXP_PLUS:

-		{

-			retStr += mkString( r[0] );

-			retStr += "+";

-		}

-			break;

-		case kind::REGEXP_OPT:

-		{

-			retStr += mkString( r[0] );

-			retStr += "?";

-		}

-			break;

-		case kind::REGEXP_RANGE:

-		{

-			retStr += "[";

-			retStr += niceChar( r[0] );

-			retStr += "-";

-			retStr += niceChar( r[1] );

-			retStr += "]";

+				break;

+			case kind::REGEXP_INTER:

+			{

+				retStr += "(";

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

+					if(i != 0) retStr += "&";

+					retStr += mkString( r[i] );

+				}

+				retStr += ")";

+			}

+				break;

+			case kind::REGEXP_STAR:

+			{

+				retStr += mkString( r[0] );

+				retStr += "*";

+			}

+				break;

+			case kind::REGEXP_PLUS:

+			{

+				retStr += mkString( r[0] );

+				retStr += "+";

+			}

+				break;

+			case kind::REGEXP_OPT:

+			{

+				retStr += mkString( r[0] );

+				retStr += "?";

+			}

+				break;

+			case kind::REGEXP_RANGE:

+			{

+				retStr += "[";

+				retStr += niceChar( r[0] );

+				retStr += "-";

+				retStr += niceChar( r[1] );

+				retStr += "]";

+			}

+				break;

+			default:

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

+				Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;

+				//AlwaysAssert( false );

+				//return Node::null();

 		}

-			break;

-		default:

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

-			Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;

-			//AlwaysAssert( false );

-			//return Node::null();

 	}

 

 	return retStr;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5bc0e5cbe..bbe2eb882 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -41,14 +41,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_infer(c),
     d_infer_exp(c),
     d_nf_pairs(c),
-    //d_ind_map1(c),
-    //d_ind_map2(c),
-    //d_ind_map_exp(c),
-    //d_ind_map_lemma(c),
-	//d_lit_to_decide_index( c, 0 ),
-	//d_lit_to_decide( c ),
+	//d_mpl( c ),
 	d_reg_exp_mem( c ),
-	//d_reg_exp_deriv( c ),
 	d_curr_cardinality( c, 0 )
 {
     // The kinds we are treating as function application in congruence
@@ -356,9 +350,16 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
 	  if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
 		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
-		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
+		  //Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
+		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR,
+			n_len.eqNode( d_zero ),
+			NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+		  Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl;
 		  d_out->lemma(n_len_geq_zero);
+
+		  Node n_len_imp_empty = NodeManager::currentNM()->mkNode( kind::IMPLIES, n_len.eqNode( d_zero ), n.eqNode( d_emptyString) );
+		  Trace("strings-lemma") << "Strings::Lemma ZERO: " << n_len_geq_zero << std::endl;
+		  d_out->lemma(n_len_imp_empty);
 	  }
 	  // FMF
 	  if( options::stringFMF() && n.getKind() == kind::VARIABLE ) {
@@ -402,33 +403,11 @@ void TheoryStrings::check(Effort e) {
     atom = polarity ? fact : fact[0];
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-		//if(fact[0].getKind() != kind::CONST_STRING) {
-		//if(polarity) {
-			d_reg_exp_mem.push_back( assertion );
-		/*} else {
-			Node r = Rewriter::rewrite( atom[1] );
-			r = d_regexp_opr.complement( r );
-			r = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, atom[0], r );
-			std::vector< Node > vec_r;
-			vec_r.push_back( r );
-
-			StringsPreprocess spp;
-			spp.simplify( vec_r );
-			for( unsigned i=1; i<vec_r.size(); i++ ){
-				if(vec_r[i].getKind() == kind::STRING_IN_REGEXP) {
-					d_reg_exp_mem.push_back( vec_r[i] );
-				} else if(vec_r[i].getKind() == kind::EQUAL) {
-					d_equalityEngine.assertEquality(vec_r[i], true, vec_r[i]);
-				} else {
-					Assert(false);
-				}
-			}
-		}*/
-		//}
+		d_reg_exp_mem.push_back( assertion );
 	}else if (atom.getKind() == kind::EQUAL) {
-      d_equalityEngine.assertEquality(atom, polarity, fact);
+		d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
-      d_equalityEngine.assertPredicate(atom, polarity, fact);
+		d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
   }
   doPendingFacts();
@@ -644,7 +623,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
 					if( nf.size()!=1 || nf[0]!=d_emptyString ) {
 						for( unsigned r=0; r<nf_temp.size(); r++ ) {
 							if( nresult && nf_temp[r].getKind()==kind::STRING_CONCAT ){
-								Trace("strings-error") << "From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
+								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] << " ";
 								}
@@ -758,14 +737,14 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 		getConcatVec( eqc, nf );
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
 		return false;
-    } else if( areEqual( eqc, d_emptyString ) ){
+    } else if( areEqual( eqc, d_emptyString ) ) {
 		eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
 		while( !eqc_i.isFinished() ) {
 			Node n = (*eqc_i);
 			if( n.getKind()==kind::STRING_CONCAT ){
 				for( unsigned i=0; i<n.getNumChildren(); i++ ){
 					if( !areEqual( n[i], d_emptyString ) ){
-						sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "Empty Concatenation" );
+						sendLemma( n.eqNode( d_emptyString ), n[i].eqNode( d_emptyString ), "CYCLE" );
 					}
 				}
 			}
@@ -909,7 +888,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										}else{
 											conc = eqn[0].eqNode( eqn[1] );
 											Node ant = mkExplain( antec, antec_new_lits );
-											sendLemma( ant, conc, "Endpoint" );
+											sendLemma( ant, conc, "ENDPOINT" );
 											return true;
 										}
 									}else{
@@ -921,7 +900,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										//Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
 										int has_loop[2] = { -1, -1 };
 										//if( !options::stringFMF() ) {
-											for( unsigned r=0; r<2; r++ ){
+											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);
@@ -1091,7 +1070,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												//unroll the str in re constraint once
 												unrollStar( str_in_re );
 												//conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc );
-												sendLemma( ant, conc, "Loop" );
+												sendLemma( ant, conc, "LOOP-BREAK" );
 
 												//we will be done
 												addNormalFormPair( normal_form_src[i], normal_form_src[j] );
@@ -1145,7 +1124,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 													Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
 
 													Node ant = mkExplain( antec, antec_new_lits );
-													sendLemma( ant, conc, "Constant Split" );
+													sendLemma( ant, conc, "CST-SPLIT" );
 													return true;
 												}
 											}else{
@@ -1157,6 +1136,18 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												}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( areDisequal( x, d_emptyString ) ) {
+														antec.push_back( xgtz );
+													} else {
+														antec_new_lits.push_back( xgtz );
+													}
+												}
+
 												Node sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", normal_forms[i][index_i].getType(), "created for v/v 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 ) );
@@ -1172,7 +1163,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												d_lemma_cache.push_back( sk_gt_zero );
 
 												Node ant = mkExplain( antec, antec_new_lits );
-												sendLemma( ant, conc, "Split" );
+												sendLemma( ant, conc, "VAR-SPLIT" );
 												return true;
 											}
 										}
@@ -1372,14 +1363,14 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 	if( conc.isNull() || conc==d_false ){
 		d_out->conflict(ant);
-		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
+		Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
 		d_conflict = true;
 	}else{
 		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
 		if( ant == d_true ) {
 			lem = conc;
 		}
-		Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+		Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
 		d_lemma_cache.push_back( lem );
 	}
 }
@@ -1389,7 +1380,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c ) {
 	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 " << c << " split lemma : " << lemma_or << std::endl;
+	Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl;
 	d_lemma_cache.push_back(lemma_or);
 	d_pending_req_phase[eq] = true;
 }
@@ -1488,18 +1479,18 @@ bool TheoryStrings::checkLengths() {
 			//if n has not instantiatied the concat..length axiom
 			//then, add lemma
 			if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){
-				if( d_length_inst.find(n)==d_length_inst.end() ){
+				if( d_length_inst.find(n)==d_length_inst.end() ) {
 					d_length_inst[n] = true;
 					Trace("strings-debug") << "get n: " << n << endl;
 					Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
 					d_length_intro_vars.push_back( sk );
 					Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
 					eq = Rewriter::rewrite(eq);
-					Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
+					Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl;
 					d_out->lemma(eq);
 					Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
 					Node lsum;
-					if( n.getKind() == kind::STRING_CONCAT ){
+					if( n.getKind() == kind::STRING_CONCAT ) {
 						//add lemma
 						std::vector<Node> node_vec;
 						for( unsigned i=0; i<n.getNumChildren(); i++ ) {
@@ -1507,13 +1498,13 @@ bool TheoryStrings::checkLengths() {
 							node_vec.push_back(lni);
 						}
 						lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-					}else{
+					} else {
 						//add lemma
 						lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
 					}
 					Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
 					ceq = Rewriter::rewrite(ceq);
-					Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl;
+					Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
 					d_out->lemma(ceq);
 					addedLemma = true;
 				}
@@ -1695,26 +1686,26 @@ bool TheoryStrings::checkLengthsEqc() {
 	std::vector< Node > nodes;
 	getEquivalenceClasses( nodes );
 	for( unsigned i=0; i<nodes.size(); i++ ){
-		if( d_normal_forms[nodes[i]].size()>1 ){
+		if( d_normal_forms[nodes[i]].size()>1 ) {
 			Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl;
 			//check if there is a length term for this equivalence class
 			EqcInfo* ei = getOrMakeEqcInfo( nodes[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[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
-				ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
-				Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
-				lc = Rewriter::rewrite( lc );
-				Node eq = llt.eqNode( lc );
-				ei->d_normalized_length.set( eq );
-				sendLemma( mkExplain( ant ), eq, "Length Normalization" );
-				addedLemma = true;
-			  }
+			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[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() );
+					ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) );
+					Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) );
+					lc = Rewriter::rewrite( lc );
+					Node eq = llt.eqNode( lc );
+					ei->d_normalized_length.set( eq );
+					sendLemma( mkExplain( ant ), eq, "Length Normalization" );
+					addedLemma = true;
+				}
 			}
 		}else{
 			Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl;
@@ -1900,6 +1891,20 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
 	}
 }
 
+
+//// Measurements
+/*
+void TheoryStrings::updateMpl( Node n, int b ) {
+	if(d_mpl.find(n) == d_mpl.end()) {
+		//d_curr_cardinality.get();
+		d_mpl[n] = b;
+	} else if(b < d_mpl[n]) {
+		d_mpl[n] = b;
+	}
+}
+*/
+
+//// Regular Expressions
 bool TheoryStrings::unrollStar( Node atom ) {
 	Node x = atom[0];
 	Node r = atom[1];
@@ -2128,6 +2133,8 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 	}
 }
 
+//// Finite Model Finding
+
 Node TheoryStrings::getNextDecisionRequest() {
 	if(options::stringFMF() && !d_conflict) {
 		//Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 7d4b740e4..e036d5646 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -36,86 +36,93 @@ 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;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
-  public:
-
-  TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
-  ~TheoryStrings();
-
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
-  std::string identify() const { return std::string("TheoryStrings"); }
-
-  Node getRepresentative( Node t );
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getLengthTerm( Node t );
-  Node getLength( Node t );
-  public:
-
-  void propagate(Effort e);
-  bool propagate(TNode literal);
-  void explain( TNode literal, std::vector<TNode>& assumptions );
-  Node explain( TNode literal );
-
-
-  // NotifyClass for equality engine
-  class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryStrings& d_str;
-  public:
-    NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-      if (value) {
-        return d_str.propagate(equality);
-      } else {
-        // We use only literal triggers so taking not is safe
-        return d_str.propagate(equality.notNode());
-      }
-    }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
-      if (value) {
-        return d_str.propagate(predicate);
-      } else {
-       return d_str.propagate(predicate.notNode());
-      }
-    }
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
-      if (value) {
-        return d_str.propagate(t1.eqNode(t2));
-      } else {
-        return d_str.propagate(t1.eqNode(t2).notNode());
-      }
-    }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      d_str.conflict(t1, t2);
-    }
-    void eqNotifyNewClass(TNode t) {
-      Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
-      d_str.eqNotifyNewClass(t);
-    }
-    void eqNotifyPreMerge(TNode t1, TNode t2) {
-      Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
-      d_str.eqNotifyPreMerge(t1, t2);
-    }
-    void eqNotifyPostMerge(TNode t1, TNode t2) {
-      Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
-      d_str.eqNotifyPostMerge(t1, t2);
-    }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-      Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
-      d_str.eqNotifyDisequal(t1, t2, reason);
-    }
-  };/* class TheoryStrings::NotifyClass */
-
-  private:
+	typedef context::CDChunkList<Node> NodeList;
+	typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+	typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+	typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+
+public:
+	TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+	~TheoryStrings();
+
+	void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
+	std::string identify() const { return std::string("TheoryStrings"); }
+
+public:
+	void propagate(Effort e);
+	bool propagate(TNode literal);
+	void explain( TNode literal, std::vector<TNode>& assumptions );
+	Node explain( TNode literal );
+
+
+	// NotifyClass for equality engine
+	class NotifyClass : public eq::EqualityEngineNotify {
+		TheoryStrings& d_str;
+	public:
+		NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
+		bool eqNotifyTriggerEquality(TNode equality, bool value) {
+		  Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+		  if (value) {
+			return d_str.propagate(equality);
+		  } else {
+			// We use only literal triggers so taking not is safe
+			return d_str.propagate(equality.notNode());
+		  }
+		}
+		bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+		  Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
+		  if (value) {
+			return d_str.propagate(predicate);
+		  } else {
+		   return d_str.propagate(predicate.notNode());
+		  }
+		}
+		bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+		  Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
+		  if (value) {
+			return d_str.propagate(t1.eqNode(t2));
+		  } else {
+			return d_str.propagate(t1.eqNode(t2).notNode());
+		  }
+		}
+		void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+		  Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+		  d_str.conflict(t1, t2);
+		}
+		void eqNotifyNewClass(TNode t) {
+		  Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
+		  d_str.eqNotifyNewClass(t);
+		}
+		void eqNotifyPreMerge(TNode t1, TNode t2) {
+		  Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
+		  d_str.eqNotifyPreMerge(t1, t2);
+		}
+		void eqNotifyPostMerge(TNode t1, TNode t2) {
+		  Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+		  d_str.eqNotifyPostMerge(t1, t2);
+		}
+		void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+		  Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
+		  d_str.eqNotifyDisequal(t1, t2, reason);
+		}
+	};/* class TheoryStrings::NotifyClass */
+
+private:
+	// Constants
+    Node d_emptyString;
+    Node d_true;
+    Node d_false;
+    Node d_zero;
+	// Helper functions
+	Node getRepresentative( Node t );
+	bool hasTerm( Node a );
+	bool areEqual( Node a, Node b );
+	bool areDisequal( Node a, Node b );
+	Node getLengthTerm( Node t );
+	Node getLength( Node t );
+
+private:
     /** The notify class */
     NotifyClass d_notify;
     /** Equaltity engine */
@@ -123,82 +130,62 @@ class TheoryStrings : public Theory {
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
 	std::vector< Node > d_length_intro_vars;
-    Node d_emptyString;
-    Node d_true;
-    Node d_false;
-    Node d_zero;
-	// RegExp depth
-	//int d_regexp_unroll_depth;
-    //list of pairs of nodes to merge
-      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;
-  /** inferences */
-  NodeList d_infer;
-  NodeList d_infer_exp;
-  /** normal forms */
-  std::map< Node, Node > d_normal_forms_base;
-  std::map< Node, std::vector< Node > > d_normal_forms;
-  std::map< Node, std::vector< Node > > d_normal_forms_exp;
-  //map of pairs of terms that have the same normal form
-  NodeListMap d_nf_pairs;
-  void addNormalFormPair( Node n1, Node n2 );
-  bool isNormalFormPair( Node n1, Node n2 );
-  bool isNormalFormPair2( Node n1, Node n2 );
-
-  //loop
-  //std::map< Node, bool > d_loop_processed;
-
-  //regular expression memberships
-  NodeList d_reg_exp_mem;
-  std::map< Node, bool > d_reg_exp_unroll;
-  std::map< Node, int > d_reg_exp_unroll_depth;
-  std::map< Node, bool > d_reg_exp_deriv;
-  //antecedant for why reg exp membership must be true
-  std::map< Node, Node > d_reg_exp_ant;
-
-  /////////////////////////////////////////////////////////////////////////////
-  // MODEL GENERATION
-  /////////////////////////////////////////////////////////////////////////////
-  public:
-
-  void collectModelInfo(TheoryModel* m, bool fullModel);
-
-  /////////////////////////////////////////////////////////////////////////////
-  // NOTIFICATIONS
-  /////////////////////////////////////////////////////////////////////////////
-
-  public:
-  void presolve();
-  void shutdown() { }
-
-  /////////////////////////////////////////////////////////////////////////////
-  // MAIN SOLVER
-  /////////////////////////////////////////////////////////////////////////////
-  private:
-  void addSharedTerm(TNode n);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-
-  private:
-  class EqcInfo
-  {
-  public:
-    EqcInfo( context::Context* c );
-    ~EqcInfo(){}
-    //constant in this eqc
-    context::CDO< Node > d_const_term;
-    context::CDO< Node > d_length_term;
-    context::CDO< unsigned > d_cardinality_lem_k;
-	// 1 = added length lemma
-	context::CDO< Node > d_normalized_length;
-  };
-  /** map from representatives to information necessary for equivalence classes */
-  std::map< Node, EqcInfo* > d_eqc_info;
-  EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
-  //maintain which concat terms have the length lemma instantiatied
-  std::map< Node, bool > d_length_inst;
-  private:
+	//list of pairs of nodes to merge
+	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;
+	/** inferences */
+	NodeList d_infer;
+	NodeList d_infer_exp;
+	/** normal forms */
+	std::map< Node, Node > d_normal_forms_base;
+	std::map< Node, std::vector< Node > > d_normal_forms;
+	std::map< Node, std::vector< Node > > d_normal_forms_exp;
+	//map of pairs of terms that have the same normal form
+	NodeListMap d_nf_pairs;
+	void addNormalFormPair( Node n1, Node n2 );
+	bool isNormalFormPair( Node n1, Node n2 );
+	bool isNormalFormPair2( Node n1, Node n2 );
+
+	/////////////////////////////////////////////////////////////////////////////
+	// MODEL GENERATION
+	/////////////////////////////////////////////////////////////////////////////
+public:
+	void collectModelInfo(TheoryModel* m, bool fullModel);
+
+	/////////////////////////////////////////////////////////////////////////////
+	// NOTIFICATIONS
+	/////////////////////////////////////////////////////////////////////////////
+public:
+	void presolve();
+	void shutdown() { }
+
+	/////////////////////////////////////////////////////////////////////////////
+	// MAIN SOLVER
+	/////////////////////////////////////////////////////////////////////////////
+private:
+	void addSharedTerm(TNode n);
+	EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+private:
+	class EqcInfo {
+	public:
+		EqcInfo( context::Context* c );
+		~EqcInfo(){}
+		//constant in this eqc
+		context::CDO< Node > d_const_term;
+		context::CDO< Node > d_length_term;
+		context::CDO< unsigned > d_cardinality_lem_k;
+		// 1 = added length lemma
+		context::CDO< Node > d_normalized_length;
+	};
+	/** map from representatives to information necessary for equivalence classes */
+	std::map< Node, EqcInfo* > d_eqc_info;
+	EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
+	//maintain which concat terms have the length lemma instantiatied
+	std::map< Node, bool > d_length_inst;
+private:
     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 > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
@@ -212,57 +199,76 @@ class TheoryStrings : public Theory {
     bool checkInductiveEquations();
 	bool checkMemberships();
 	int gcd(int a, int b);
-  public:
-  void preRegisterTerm(TNode n);
-  void check(Effort e);
-
-  /** Conflict when merging two constants */
-  void conflict(TNode a, TNode b);
-  /** called when a new equivalance class is created */
-  void eqNotifyNewClass(TNode t);
-  /** called when two equivalance classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  /** called when two equivalance classes have merged */
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  /** called when two equivalence classes are made disequal */
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+
+public:
+	void preRegisterTerm(TNode n);
+	void check(Effort e);
+
+	/** Conflict when merging two constants */
+	void conflict(TNode a, TNode b);
+	/** called when a new equivalance class is created */
+	void eqNotifyNewClass(TNode t);
+	/** called when two equivalance classes will merge */
+	void eqNotifyPreMerge(TNode t1, TNode t2);
+	/** called when two equivalance classes have merged */
+	void eqNotifyPostMerge(TNode t1, TNode t2);
+	/** called when two equivalence classes are made disequal */
+	void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 protected:
-  /** compute care graph */
-  void computeCareGraph();
-
-  //do pending merges
-  void doPendingFacts();
-  void doPendingLemmas();
-
-  void sendLemma( Node ant, Node conc, const char * c );
-  void sendSplit( Node a, Node b, const char * c );
-  /** mkConcat **/
-  Node mkConcat( Node n1, Node n2 );
-  Node mkConcat( std::vector< Node >& c );
-  /** mkExplain **/
-  Node mkExplain( std::vector< Node >& a );
-  Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
-  /** get concat vector */
-  void getConcatVec( Node n, std::vector< Node >& c );
-
-  //get equivalence classes
-  void getEquivalenceClasses( std::vector< Node >& eqcs );
-  //get final normal form
-  void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
-
-  //seperate into collections with equal length
-  void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
-  void printConcat( std::vector< Node >& n, const char * c );
+	/** compute care graph */
+	void computeCareGraph();
+
+	//do pending merges
+	void doPendingFacts();
+	void doPendingLemmas();
+
+	void sendLemma( Node ant, Node conc, const char * c );
+	void sendSplit( Node a, Node b, const char * c );
+	/** mkConcat **/
+	Node mkConcat( Node n1, Node n2 );
+	Node mkConcat( std::vector< Node >& c );
+	/** mkExplain **/
+	Node mkExplain( std::vector< Node >& a );
+	Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+	/** get concat vector */
+	void getConcatVec( Node n, std::vector< Node >& c );
+
+	//get equivalence classes
+	void getEquivalenceClasses( std::vector< Node >& eqcs );
+	//get final normal form
+	void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
+
+	//seperate into collections with equal length
+	void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
+	void printConcat( std::vector< Node >& n, const char * c );
+
+	// Measurement
+private:
+	//NodeIntMap d_mpl;
+	//void updateMpl(Node n, int b);
+
+	//NodeIntMap d_var_lmin;
+	//NodeIntMap d_var_lmax;
 
 	// Regular Expression
 private:
+	// regular expression memberships
+	NodeList d_reg_exp_mem;
+	// antecedant for why reg exp membership must be true
+	std::map< Node, Node > d_reg_exp_ant;
+	std::map< Node, bool > d_reg_exp_unroll;
+	std::map< Node, int > d_reg_exp_unroll_depth;
+	// regular expression derivative
+	std::map< Node, bool > d_reg_exp_deriv;
+	// regular expression operations
 	RegExpOpr d_regexp_opr;
+
 	CVC4::String getHeadConst( Node x );
 	bool splitRegExp( Node x, Node r, Node ant );
 
-private:
+
 	// Finite Model Finding
-	//bool d_fmf;
+private:
 	std::vector< Node > d_in_vars;
 	Node d_in_var_lsum;
 	std::map< int, Node > d_cardinality_lits;