From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 26 Mar 2014 22:30:30 +0000 (-0500)
Subject: deriv symbolic regexp
X-Git-Tag: cvc5-1.0.0~6998
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39ecf62936e75db50b50a54c24288fd0d7b3c81f;p=cvc5.git

deriv symbolic regexp
---

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 743130727..52c76880b 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -80,11 +80,12 @@ bool RegExpOpr::checkConstRegExp( Node r ) {
 }
 
 // 0-unknown, 1-yes, 2-no
-int RegExpOpr::delta( Node r ) {
-	Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r ) << std::endl;
+int RegExpOpr::delta( Node r, Node &exp ) {
+	Trace("regexp-delta") << "RegExp-Delta starts with " << mkString( r ) << std::endl;
 	int ret = 0;
 	if( d_delta_cache.find( r ) != d_delta_cache.end() ) {
-		ret = d_delta_cache[r];
+		ret = d_delta_cache[r].first;
+		exp = d_delta_cache[r].second;
 	} else {
 		int k = r.getKind();
 		switch( k ) {
@@ -97,63 +98,95 @@ int RegExpOpr::delta( Node r ) {
 				break;
 			}
 			case kind::STRING_TO_REGEXP: {
-				if(r[0].isConst()) {
-					if(r[0] == d_emptyString) {
+				Node tmp = Rewriter::rewrite(r[0]);
+				if(tmp.isConst()) {
+					if(tmp == d_emptyString) {
 						ret = 1;
 					} else {
 						ret = 2;
 					}
 				} else {
 					ret = 0;
+					if(tmp.getKind() == kind::STRING_CONCAT) {
+						for(unsigned i=0; i<tmp.getNumChildren(); i++) {
+							if(tmp[i].isConst()) {
+								ret = 2; break;
+							}
+						}
+
+					}
+					if(ret == 0) {
+						exp = r[0].eqNode(d_emptyString);
+					}
 				}
 				break;
 			}
 			case kind::REGEXP_CONCAT: {
 				bool flag = false;
+				std::vector< Node > vec_nodes;
 				for(unsigned i=0; i<r.getNumChildren(); ++i) {
-					int tmp = delta( r[i] );
+					Node exp2;
+					int tmp = delta( r[i], exp2 );
 					if(tmp == 2) {
 						ret = 2;
 						break;
 					} else if(tmp == 0) {
+						vec_nodes.push_back( exp2 );
 						flag = true;
 					}
 				}
-				if(!flag && ret != 2) {
-					ret = 1;
+				if(ret != 2) {
+					if(!flag) {
+						ret = 1;
+					} else {
+						exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+					}
 				}
 				break;
 			}
 			case kind::REGEXP_UNION: {
 				bool flag = false;
+				std::vector< Node > vec_nodes;
 				for(unsigned i=0; i<r.getNumChildren(); ++i) {
-					int tmp = delta( r[i] );
+					Node exp2;
+					int tmp = delta( r[i], exp2 );
 					if(tmp == 1) {
 						ret = 1;
 						break;
 					} else if(tmp == 0) {
+						vec_nodes.push_back( exp2 );
 						flag = true;
 					}
 				}
-				if(!flag && ret != 1) {
-					ret = 2;
+				if(ret != 1) {
+					if(!flag) {
+						ret = 2;
+					} else {
+						exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::OR, vec_nodes);
+					}
 				}
 				break;
 			}
 			case kind::REGEXP_INTER: {
-				bool flag = true;
+				bool flag = false;
+				std::vector< Node > vec_nodes;
 				for(unsigned i=0; i<r.getNumChildren(); ++i) {
-					int tmp = delta( r[i] );
+					Node exp2;
+					int tmp = delta( r[i], exp2 );
 					if(tmp == 2) {
-						ret = 2; flag=false;
+						ret = 2;
 						break;
 					} else if(tmp == 0) {
-						flag=false;
-						break;
+						vec_nodes.push_back( exp2 );
+						flag = true;
 					}
 				}
-				if(flag) {
-					ret = 1;
+				if(ret != 2) {
+					if(!flag) {
+						ret = 1;
+					} else {
+						exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+					}
 				}
 				break;
 			}
@@ -162,7 +195,7 @@ int RegExpOpr::delta( Node r ) {
 				break;
 			}
 			case kind::REGEXP_PLUS: {
-				ret = delta( r[0] );
+				ret = delta( r[0], exp );
 				break;
 			}
 			case kind::REGEXP_OPT: {
@@ -179,9 +212,226 @@ int RegExpOpr::delta( Node r ) {
 				//return Node::null();
 			}
 		}
-		d_delta_cache[r] = ret;
+		if(!exp.isNull()) {
+			exp = Rewriter::rewrite(exp);
+		}
+		std::pair< int, Node > p(ret, exp);
+		d_delta_cache[r] = p;
+	}
+	Trace("regexp-delta") << "RegExp-Delta returns : " << ret << std::endl;
+	return ret;
+}
+
+// 0-unknown, 1-yes, 2-no
+int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
+	Assert( c.size() < 2 );
+	Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
+	
+	int ret = 1;
+	retNode = d_emptyRegexp;
+	
+	PairNodeStr dv = std::make_pair( r, c );
+	if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {
+		retNode = d_deriv_cache[dv].first;
+		ret = d_deriv_cache[dv].second;
+	} else if( c.isEmptyString() ) {
+		Node expNode;
+		ret = delta( r, expNode );
+		if(ret == 0) {
+			retNode = NodeManager::currentNM()->mkNode(kind::ITE, expNode, r, d_emptyRegexp);
+		} else if(ret == 1) {
+			retNode = r;
+		}
+		std::pair< Node, int > p(retNode, ret);
+		d_deriv_cache[dv] = p;
+	} else {
+		switch( r.getKind() ) {
+			case kind::REGEXP_EMPTY: {
+				ret = 2;
+				break;
+			}
+			case kind::REGEXP_SIGMA: {
+				retNode = d_emptySingleton;
+				break;
+			}
+			case kind::STRING_TO_REGEXP: {
+				Node tmp = Rewriter::rewrite(r[0]);
+				if(tmp.isConst()) {
+					if(tmp == d_emptyString) {
+						ret = 2;
+					} else {
+						if(tmp.getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {
+							retNode =  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, 
+								tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );
+						} else {
+							ret = 2;
+						}
+					}
+				} else {
+					ret = 0;
+					Node rest;
+					if(tmp.getKind() == kind::STRING_CONCAT) {
+						Node t2 = tmp[0];
+						if(t2.isConst()) {
+							if(t2.getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {
+								Node n =  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, 
+									tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );
+								std::vector< Node > vec_nodes;
+								vec_nodes.push_back(n);
+								for(unsigned i=1; i<tmp.getNumChildren(); i++) {
+									vec_nodes.push_back(tmp[i]);
+								}
+								retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);
+								ret = 1;
+							} else {
+								ret = 2;
+							}
+						} else {
+							tmp = tmp[0];
+							std::vector< Node > vec_nodes;
+							for(unsigned i=1; i<tmp.getNumChildren(); i++) {
+								vec_nodes.push_back(tmp[i]);
+							}
+							rest = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);
+						}
+					}
+					if(ret == 0) {
+						Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );
+						retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
+						if(!rest.isNull()) {
+							retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
+						}
+						Node exp = tmp.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
+												NodeManager::currentNM()->mkConst(c), sk));
+						retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, exp, retNode, d_emptyRegexp));
+					}
+				}
+				break;
+			}
+			case kind::REGEXP_CONCAT: {
+				std::vector< Node > vec_nodes;
+				std::vector< Node > delta_nodes;
+				Node dnode = d_true;
+				for(unsigned i=0; i<r.getNumChildren(); ++i) {
+					Node dc;
+					Node exp2;
+					int rt = derivativeS(r[i], c, dc);
+					if(rt != 2) {
+						if(rt == 0) {
+							ret = 0;
+						}
+						std::vector< Node > vec_nodes2;
+						if(dc != d_emptySingleton) {
+							vec_nodes2.push_back( dc );
+						}
+						for(unsigned j=i+1; j<r.getNumChildren(); ++j) {
+							if(r[j] != d_emptySingleton) {
+								vec_nodes2.push_back( r[j] );
+							}
+						}
+						Node tmp = vec_nodes2.size()==0 ? d_emptySingleton : 
+							vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 );
+						if(dnode != d_true) {
+							tmp = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, dnode, tmp, d_emptyRegexp));
+							ret = 0;
+						}
+						if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {
+							vec_nodes.push_back( tmp );
+						}
+					}
+					Node exp3;
+					int rt2 = delta( r[i], exp3 );
+					if( rt2 == 0 ) {
+						dnode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, dnode, exp3));
+					} else if( rt2 == 2 ) {
+						break;
+					}
+				}
+				retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
+							( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );
+				if(retNode == d_emptyRegexp) {
+					ret = 2;
+				}
+				break;
+			}
+			case kind::REGEXP_UNION: {
+				std::vector< Node > vec_nodes;
+				for(unsigned i=0; i<r.getNumChildren(); ++i) {
+					Node dc;
+					int rt = derivativeS(r[i], c, dc);
+					if(rt == 0) {
+						ret = 0;
+					}
+					if(rt != 2) {
+						if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {
+							vec_nodes.push_back( dc );
+						}
+					}
+					Trace("regexp-deriv") << "RegExp-deriv OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;
+				}
+				retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
+							( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );
+				if(retNode == d_emptyRegexp) {
+					ret = 2;
+				}
+				break;
+			}
+			case kind::REGEXP_INTER: {
+				bool flag = true;
+				bool flag_sg = false;
+				std::vector< Node > vec_nodes;
+				for(unsigned i=0; i<r.getNumChildren(); ++i) {
+					Node dc;
+					int rt = derivativeS(r[i], c, dc);
+					if(rt == 0) {
+						ret = 0;
+					} else if(rt == 2) {
+						flag = false;
+						break;
+					}
+					if(dc == d_sigma_star) {
+						flag_sg = true;
+					} else {
+						if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {
+							vec_nodes.push_back( dc );
+						}
+					}
+				}
+				if(flag) {
+					if(vec_nodes.size() == 0 && flag_sg) {
+						retNode = d_sigma_star;
+					} else {
+						retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
+									( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes ) );
+						if(retNode == d_emptyRegexp) {
+							ret = 2;
+						}
+					}
+				} else {
+					retNode = d_emptyRegexp;
+					ret = 2;
+				}
+				break;
+			}
+			case kind::REGEXP_STAR: {
+				Node dc;
+				ret = derivativeS(r[0], c, dc);
+				retNode = dc==d_emptyRegexp ? dc : (dc==d_emptySingleton ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r ));
+				break;
+			}
+			default: {
+				Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
+				Assert( false, "Unsupported Term" );
+			}
+		}
+		if(retNode != d_emptyRegexp) {
+			retNode = Rewriter::rewrite( retNode );
+		}
+		std::pair< Node, int > p(retNode, ret);
+		d_deriv_cache[dv] = p;
 	}
-	Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret << std::endl;
+
+	Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode ) << std::endl;
 	return ret;
 }
 
@@ -189,11 +439,12 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 	Assert( c.size() < 2 );
 	Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
 	Node retNode = d_emptyRegexp;
-	PairDvStr dv = std::make_pair( r, c );
+	PairNodeStr dv = std::make_pair( r, c );
 	if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
 		retNode = d_dv_cache[dv];
 	} else if( c.isEmptyString() ){
-		int tmp = delta( r );
+		Node exp;
+		int tmp = delta( r, exp );
 		if(tmp == 0) {
 			// TODO variable
 			retNode = d_emptyRegexp;
@@ -252,8 +503,8 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 							vec_nodes.push_back( tmp );
 						}
 					}
-
-					if( delta( r[i] ) != 1 ) {
+					Node exp;
+					if( delta( r[i], exp ) != 1 ) {
 						break;
 					}
 				}
@@ -444,7 +695,8 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
 				for(unsigned i=0; i<r.getNumChildren(); i++) {
 					firstChars(r[i], cset, vset);
 					Node n = r[i];
-					int r = delta( n );
+					Node exp;
+					int r = delta( n, exp );
 					if(r != 1) {
 						break;
 					}
@@ -585,22 +837,6 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars )
 			}
 		}
 			break;
-			/*
-		case kind::REGEXP_PLUS:
-		{
-			ret = delta( r[0] );
-		}
-			break;
-		case kind::REGEXP_OPT:
-		{
-			ret = 1;
-		}
-			break;
-		case kind::REGEXP_RANGE:
-		{
-			ret = 2;
-		}
-			break;*/
 		default: {
 			Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
 			//AlwaysAssert( false );
@@ -966,23 +1202,30 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
 	}
 }
 
-Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache ) {
+Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag ) {
+	if(spflag) {
+		//TODO: var
+		return Node::null();
+	}
 	std::pair < Node, Node > p(r1, r2);
 	std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p);
 	Node rNode;
 	if(itr != d_inter_cache.end()) {
-		//Trace("regexp-intersect") << "INTERSECT Case 0: Cached " << std::endl;
 		rNode = itr->second;
 	} else {
-		if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {
-		Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl;
+		if(r1 == r2) {
+			rNode = r1;
+		} else if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {
+			Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl;
 			rNode = d_emptyRegexp;
 		} else if(r1 == d_emptySingleton || r2 == d_emptySingleton) {
 			Trace("regexp-intersect") << "INTERSECT Case 2: one empty Singleton" << std::endl;
-			int r = delta(r1 == d_emptySingleton ? r2 : r1);
+			Node exp;
+			int r = delta((r1 == d_emptySingleton ? r2 : r1), exp);
 			if(r == 0) {
 				//TODO: variable
-				AlwaysAssert( false, "Unsupported Yet, 892 REO" );
+				spflag = true;
+				//Assert( false, "Unsupported Yet, 892 REO" );
 			} else if(r == 1) {
 				rNode = d_emptySingleton;
 			} else {
@@ -1012,14 +1255,18 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 							std::map< unsigned, std::set< PairNodes > > cache2(cache);
 							PairNodes p(r1l, r2l);
 							cache2[ *itr ].insert( p );
-							Node rt = intersectInternal(r1l, r2l, cache2);
+							Node rt = intersectInternal(r1l, r2l, cache2, spflag);
+							if(spflag) {
+								//TODO:
+								return Node::null();
+							}
 							rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, 
 								NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
 							vec_nodes.push_back(rt);
 						}
 					}
 					rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :
-							NodeManager::currentNM()->mkNode(kind::OR, vec_nodes);
+							NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
 					rNode = Rewriter::rewrite( rNode );
 				} else {
 					Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl;
@@ -1027,7 +1274,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 				}
 			} else {
 				//TODO: non-empty var set
-				AlwaysAssert( false, "Unsupported Yet, 927 REO" );
+				spflag = true;
+				//Assert( false, "Unsupported Yet, 927 REO" );
 			}
 		}
 		d_inter_cache[p] = rNode;
@@ -1035,9 +1283,9 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 	Trace("regexp-intersect") << "INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
 	return rNode;
 }
-Node RegExpOpr::intersect(Node r1, Node r2) {
+Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
 	std::map< unsigned, std::set< PairNodes > > cache;
-	return intersectInternal(r1, r2, cache);
+	return intersectInternal(r1, r2, cache, spflag);
 }
 //printing
 std::string RegExpOpr::niceChar( Node r ) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 9bd694f5c..fcac28890 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -33,7 +33,7 @@ namespace theory {
 namespace strings {
 
 class RegExpOpr {
-	typedef std::pair< Node, CVC4::String > PairDvStr;
+	typedef std::pair< Node, CVC4::String > PairNodeStr;
 	typedef std::set< Node > SetNodes;
 	typedef std::pair< Node, Node > PairNodes;
 
@@ -55,8 +55,9 @@ private:
 	std::map< PairNodes, Node > d_simpl_cache;
 	std::map< PairNodes, Node > d_simpl_neg_cache;
 	std::map< Node, Node > d_compl_cache;
-	std::map< Node, int > d_delta_cache;
-	std::map< PairDvStr, Node > d_dv_cache;
+	std::map< Node, std::pair< int, Node > > d_delta_cache;
+	std::map< PairNodeStr, Node > d_dv_cache;
+	std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
 	std::map< Node, bool > d_cstre_cache;
 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
 	std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
@@ -69,7 +70,7 @@ private:
 	Node mkAllExceptOne( char c );
 
 	void getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
-	Node intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache );
+	Node intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache, bool &spflag );
 	void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
 
 	//TODO: for intersection
@@ -80,10 +81,11 @@ public:
 
 	bool checkConstRegExp( Node r );
     void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
-	int delta( Node r );
+	int delta( Node r, Node &exp );
+	int derivativeS( Node r, CVC4::String c, Node &retNode );
 	Node derivativeSingle( Node r, CVC4::String c );
 	bool guessLength( Node r, int &co );
-	Node intersect(Node r1, Node r2);
+	Node intersect(Node r1, Node r2, bool &spflag);
 
 	std::string mkString( Node r );
 };
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7998669cf..3f576d4f5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -57,6 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_regexp_ccached(c),
 	d_str_re_map(c),
 	d_inter_cache(c),
+	d_inter_index(c),
 	d_regexp_ant(c),
 	d_input_vars(u),
 	d_input_var_lsum(u),
@@ -1052,6 +1053,37 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 							  NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
 								NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
 				conc = str_in_re;
+			} else if(t_yz.isConst()) {
+				CVC4::String s = t_yz.getConst< CVC4::String >();
+				unsigned size = s.size();
+				std::vector< Node > vconc;
+				for(unsigned len=1; len<=size; len++) {
+					Node y = NodeManager::currentNM()->mkConst(s.substr(0, len));
+					Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len));
+					Node restr = s_zy;
+					Node cc;
+					if(r != d_emptyString) {
+						std::vector< Node > v2(vec_r);
+						v2.insert(v2.begin(), y);
+						v2.insert(v2.begin(), z);
+						restr = mkConcat( z, y );
+						cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) ));
+					} else {
+						cc = Rewriter::rewrite(s_zy.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z, y) ));
+					}
+					if(cc == d_false) {
+						continue;
+					}
+					Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+									NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, 
+										NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
+										NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
+											NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr))));
+					cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 );
+					d_regexp_ant[conc2] = ant;
+					vconc.push_back(cc);
+				}
+				conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc);
 			} else {
 				Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
 				//right
@@ -1082,9 +1114,9 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 			} // normal case
 
 			//set its antecedant to ant, to say when it is relevant
-			d_regexp_ant[str_in_re] = ant;
-			//unroll the str in re constraint once
-			//	unrollStar( str_in_re );
+			if(!str_in_re.isNull()) {
+				d_regexp_ant[str_in_re] = ant;
+			}
 			sendLemma( ant, conc, "LOOP-BREAK" );
 			++(d_statistics.d_loop_lemmas);
 
@@ -2304,31 +2336,57 @@ bool TheoryStrings::checkMemberships() {
 	if(options::stringEIT()) {
 		for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
 			itr_xr != d_str_re_map.end(); ++itr_xr ) {
+			bool spflag = false;
+			Node x = (*itr_xr).first;
 			NodeList* lst = (*itr_xr).second;
-			if(lst->size() > 1) {
-				Node r = (*lst)[0];
-				NodeList::const_iterator itr_lst = lst->begin();
-				++itr_lst;
-				for(;itr_lst != lst->end(); ++itr_lst) {
-					Node r2 = *itr_lst;
-					r = d_regexp_opr.intersect(r, r2);
-					if(r == d_emptyRegexp) {
-						std::vector< Node > vec_nodes;
-						Node x = (*itr_xr).first;
+			if(d_inter_index.find(x) == d_inter_index.end()) {
+				d_inter_index[x] = 0;
+			}
+			int cur_inter_idx = d_inter_index[x];
+			if(cur_inter_idx != (int)lst->size()) {
+				if(lst->size() == 1) {
+					d_inter_cache[x] = (*lst)[0];
+					d_inter_index[x] = 1;
+				} else if(lst->size() > 1) {
+					Node r;
+					if(d_inter_cache.find(x) != d_inter_cache.end()) {
+						r = d_inter_cache[x];
+					}
+					if(r.isNull()) {
+						r = (*lst)[0];
+						cur_inter_idx = 1;
+					}
+					NodeList::const_iterator itr_lst = lst->begin();
+					for(int i=0; i<cur_inter_idx; i++) {
 						++itr_lst;
-						for(NodeList::const_iterator itr2 = lst->begin();
-							itr2 != itr_lst; ++itr2) {
-							Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
-							vec_nodes.push_back( n );
+					}
+					for(;itr_lst != lst->end(); ++itr_lst) {
+						Node r2 = *itr_lst;
+						r = d_regexp_opr.intersect(r, r2, spflag);
+						if(spflag) {
+							break;
+						} else if(r == d_emptyRegexp) {
+							std::vector< Node > vec_nodes;
+							++itr_lst;
+							for(NodeList::const_iterator itr2 = lst->begin();
+								itr2 != itr_lst; ++itr2) {
+								Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
+								vec_nodes.push_back( n );
+							}
+							Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+							Node conc;
+							sendLemma(antec, conc, "INTERSEC CONFLICT");
+							addedLemma = true;
+							break;
+						}
+						if(d_conflict) {
+							break;
 						}
-						Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
-						Node conc;
-						sendLemma(antec, conc, "INTERSEC CONFLICT");
-						addedLemma = true;
-						break;
 					}
-					if(d_conflict) {
-						break;
+					//updates
+					if(!d_conflict && !spflag) {
+						d_inter_cache[x] = r;
+						d_inter_index[x] = (int)lst->size();
 					}
 				}
 			}
@@ -2515,16 +2573,30 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
 		}
 	}*/
 	if(areEqual(x, d_emptyString)) {
-		int rdel = d_regexp_opr.delta(r);
-		if(rdel == 1) {
-			d_regexp_ccached.insert(atom);
-		} else if(rdel == 2) {
-			Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
-			Node conc = Node::null();
-			sendLemma(antec, conc, "RegExp Delta CONFLICT");
-			addedLemma = true;
-			d_regexp_ccached.insert(atom);
-			return false;
+		Node exp;
+		switch(d_regexp_opr.delta(r, exp)) {
+			case 0: {
+				Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+				sendLemma(antec, exp, "RegExp Delta");
+				addedLemma = true;
+				d_regexp_ccached.insert(atom);
+				return false;
+			}
+			case 1: {
+				d_regexp_ccached.insert(atom);
+				break;
+			}
+			case 2: {
+				Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+				Node conc = Node::null();
+				sendLemma(antec, conc, "RegExp Delta CONFLICT");
+				addedLemma = true;
+				d_regexp_ccached.insert(atom);
+				return false;
+			}
+			default: 
+				//Impossible
+				break;
 		}
 	} else {
 		Node xr = getRepresentative( x );
@@ -2720,7 +2792,7 @@ bool TheoryStrings::addMembershipLength(Node atom) {
 bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 	// TODO cstr in vre
 	Assert(x != d_emptyString);
-	Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+	Trace("regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
 	//if(x.isConst()) {
 	//	Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
 	//	Node r = Rewriter::rewrite( n );
@@ -2736,8 +2808,11 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 		bool flag = true;
 		for(unsigned i=0; i<s.size(); ++i) {
 			CVC4::String c = s.substr(i, 1);
-			dc = d_regexp_opr.derivativeSingle(dc, c);
-			if(dc == d_emptyRegexp) {
+			Node dc2;
+			int rt = d_regexp_opr.derivativeS(dc, c, dc2);
+			if(rt == 0) {
+				//TODO
+			} else if(rt == 2) {
 				// CONFLICT
 				flag = false;
 				break;
@@ -2799,16 +2874,6 @@ void TheoryStrings::addMembership(Node assertion) {
 				}
 			}
 			lst->push_back( r );
-			//TODO: make it smarter
-			/*
-			unsigned size = lst->size();
-			if(size == 1) {
-				d_inter_cache[x] = r;
-			} else {
-				Node r1 = (*lst)[size - 2];
-				Node rr = d_regexp_opr.intersect(r1, r);
-				d_inter_cache[x] = rr;
-			}*/
 		}
 	}
 }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 355c536dd..9f99012df 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -311,6 +311,7 @@ private:
 	// intersection
 	NodeListMap d_str_re_map;
 	NodeNodeMap d_inter_cache;
+	NodeIntMap d_inter_index;
 	// antecedant for why regexp membership must be true
 	NodeNodeMap d_regexp_ant;
 	// membership length
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 512c2eff0..8c4a3922d 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -307,18 +307,14 @@ public:
   String substr(unsigned i) const {
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
-    //for(unsigned k=0; k<i; k++) ++itr;
     ret_vec.insert(ret_vec.end(), itr, d_str.end());
-      return String(ret_vec);
+    return String(ret_vec);
   }
   String substr(unsigned i, unsigned j) const {
     std::vector<unsigned int> ret_vec;
     std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
-    //for(unsigned k=0; k<i; k++) ++itr;
-    //std::vector<unsigned int>::const_iterator itr2 = itr;
-    //for(unsigned k=0; k<j; k++) ++itr2;
     ret_vec.insert( ret_vec.end(), itr, itr + j );
-      return String(ret_vec);
+    return String(ret_vec);
   }
   bool isNumber() const {
 	 if(d_str.size() == 0) return false;