From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 25 Mar 2014 06:08:29 +0000 (-0500)
Subject: adds intersection
X-Git-Tag: cvc5-1.0.0~6995^2~1^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b76076872f3a0a97eef52f5ee97f10dada027c79;p=cvc5.git

adds intersection
---

diff --git a/src/theory/strings/options b/src/theory/strings/options
index fb28f7e32..f6d765fc4 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -14,6 +14,9 @@ option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_eq
 option stringFMF strings-fmf --strings-fmf bool :default false :read-write
  the finite model finding used by the theory of strings
 
+option stringEIT strings-eit --strings-eit bool :default false
+ the eager intersection used by the theory of strings
+
 expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 9d5c1c7e4..743130727 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -20,9 +20,9 @@
  
  **
  
- ** \brief Regular Expresion Operations
+ ** \brief Symbolic Regular Expresion Operations
  **
- ** Regular Expresion Operations
+ ** Symbolic Regular Expresion Operations
  **/
 
 #include "theory/strings/regexp_operation.h"
@@ -38,6 +38,7 @@ RegExpOpr::RegExpOpr() {
     d_false = NodeManager::currentNM()->mkConst( false );
 	d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 	d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+	d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
 	std::vector< Node > nvec;
     d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
 	// All Charactors = all printable ones 32-126
@@ -46,6 +47,7 @@ RegExpOpr::RegExpOpr() {
 	//d_sigma = mkAllExceptOne( '\0' );
 	d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );
 	d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
+	d_card = 256;
 }
 
 int RegExpOpr::gcd ( int a, int b ) {
@@ -185,7 +187,7 @@ int RegExpOpr::delta( Node r ) {
 
 Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 	Assert( c.size() < 2 );
-	Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
+	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 );
 	if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
@@ -268,7 +270,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 " << mkString(dc) << std::endl;
+					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 ) );
@@ -326,7 +328,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 		}
 		d_dv_cache[dv] = retNode;
 	}
-	Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode ) << std::endl;
+	Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode ) << std::endl;
 	return retNode;
 }
 
@@ -400,16 +402,89 @@ bool RegExpOpr::guessLength( Node r, int &co ) {
 	}
 }
 
-void RegExpOpr::firstChar( Node r ) {
-	Trace("strings-regexp-firstchar") << "Head characters: ";
-	for(char ch = d_char_start; ch <= d_char_end; ++ch) {
-		CVC4::String c(ch);
-		Node dc = derivativeSingle(r, ch);
-		if(!dc.isNull()) {
-			Trace("strings-regexp-firstchar") << c << " (" << mkString(dc) << ")" << std::endl;
+void RegExpOpr::firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
+	std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
+	if(itr != d_fset_cache.end()) {
+		pcset.insert((itr->second).first.begin(), (itr->second).first.end());
+		pvset.insert((itr->second).second.begin(), (itr->second).second.end());
+	} else {
+		std::set<unsigned> cset;
+		SetNodes vset;
+		int k = r.getKind();
+		switch( k ) {
+			case kind::REGEXP_EMPTY: {
+				break;
+			}
+			case kind::REGEXP_SIGMA: {
+				for(unsigned i=0; i<d_card; i++) {
+					cset.insert(i);
+				}
+				break;
+			}
+			case kind::STRING_TO_REGEXP: {
+				Node st = Rewriter::rewrite(r[0]);
+				if(st.isConst()) {
+					CVC4::String s = st.getConst< CVC4::String >();
+					if(s.size() != 0) {
+						cset.insert(s[0]);
+					}
+				} else if(st.getKind() == kind::VARIABLE) {
+					vset.insert( st );
+				} else {
+					if(st[0].isConst()) {
+						CVC4::String s = st[0].getConst< CVC4::String >();
+						cset.insert(s[0]);
+					} else {
+						vset.insert( st[0] );
+					}
+				}
+				break;
+			}
+			case kind::REGEXP_CONCAT: {
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					firstChars(r[i], cset, vset);
+					Node n = r[i];
+					int r = delta( n );
+					if(r != 1) {
+						break;
+					}
+				}
+				break;
+			}
+			case kind::REGEXP_UNION: {
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					firstChars(r[i], cset, vset);
+				}
+				break;
+			}
+			case kind::REGEXP_INTER: {
+				//TODO: Overapproximation for now
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					firstChars(r[i], cset, vset);
+				}
+				break;
+			}
+			case kind::REGEXP_STAR: {
+				firstChars(r[0], cset, vset);
+				break;
+			}
+			default: {
+				Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
+				Assert( false, "Unsupported Term" );
+			}
 		}
+		pcset.insert(cset.begin(), cset.end());
+		pvset.insert(vset.begin(), vset.end());
+		std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
+		d_fset_cache[r] = p;
+
+		Trace("regexp-fset") << "FSET( " << mkString(r) << " ) = { ";
+		for(std::set<unsigned>::const_iterator itr = cset.begin();
+			itr != cset.end(); itr++) {
+				Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr) << ",";
+			}
+		Trace("regexp-fset") << " }" << std::endl;
 	}
-	Trace("strings-regexp-firstchar") << std::endl;
 }
 
 bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars ) {
@@ -567,7 +642,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
 	std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_neg_cache.find(p);
 	if(itr != d_simpl_neg_cache.end()) {
 		new_nodes.push_back( itr->second );
-		return;
 	} else {
 		int k = r.getKind();
 		Node conc;
@@ -701,7 +775,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
 	std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_cache.find(p);
 	if(itr != d_simpl_cache.end()) {
 		new_nodes.push_back( itr->second );
-		return;
 	} else {
 		int k = r.getKind();
 		Node conc;
@@ -813,6 +886,159 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
 	}
 }
 
+void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset ) {
+	std::map< Node, std::pair< std::set<unsigned>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
+	if(itr != d_cset_cache.end()) {
+		pcset.insert((itr->second).first.begin(), (itr->second).first.end());
+		pvset.insert((itr->second).second.begin(), (itr->second).second.end());
+	} else {
+		std::set<unsigned> cset;
+		SetNodes vset;
+		int k = r.getKind();
+		switch( k ) {
+			case kind::REGEXP_EMPTY: {
+				break;
+			}
+			case kind::REGEXP_SIGMA: {
+				for(unsigned i=0; i<d_card; i++) {
+					cset.insert(i);
+				}
+				break;
+			}
+			case kind::STRING_TO_REGEXP: {
+				Node st = Rewriter::rewrite(r[0]);
+				if(st.isConst()) {
+					CVC4::String s = st.getConst< CVC4::String >();
+					s.getCharSet( cset );
+				} else if(st.getKind() == kind::VARIABLE) {
+					vset.insert( st );
+				} else {
+					for(unsigned i=0; i<st.getNumChildren(); i++) {
+						if(st[i].isConst()) {
+							CVC4::String s = st[i].getConst< CVC4::String >();
+							s.getCharSet( cset );
+						} else {
+							vset.insert( st[i] );
+						}
+					}
+				}
+				break;
+			}
+			case kind::REGEXP_CONCAT: {
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					getCharSet(r[i], cset, vset);
+				}
+				break;
+			}
+			case kind::REGEXP_UNION: {
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					getCharSet(r[i], cset, vset);
+				}
+				break;
+			}
+			case kind::REGEXP_INTER: {
+				//TODO: Overapproximation for now
+				for(unsigned i=0; i<r.getNumChildren(); i++) {
+					getCharSet(r[i], cset, vset);
+				}
+				break;
+			}
+			case kind::REGEXP_STAR: {
+				getCharSet(r[0], cset, vset);
+				break;
+			}
+			default: {
+				Trace("strings-regexp") << "Unsupported term: " << r << " in getCharSet." << std::endl;
+				Assert( false, "Unsupported Term" );
+			}
+		}
+		pcset.insert(cset.begin(), cset.end());
+		pvset.insert(vset.begin(), vset.end());
+		std::pair< std::set<unsigned>, SetNodes > p(cset, vset);
+		d_cset_cache[r] = p;
+
+		Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
+		for(std::set<unsigned>::const_iterator itr = cset.begin();
+			itr != cset.end(); itr++) {
+				Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr) << ",";
+			}
+		Trace("regexp-cset") << " }" << std::endl;
+	}
+}
+
+Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::set< PairNodes > > cache ) {
+	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;
+			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);
+			if(r == 0) {
+				//TODO: variable
+				AlwaysAssert( false, "Unsupported Yet, 892 REO" );
+			} else if(r == 1) {
+				rNode = d_emptySingleton;
+			} else {
+				rNode = d_emptyRegexp;
+			}
+		} else {
+			Trace("regexp-intersect") << "INTERSECT Case 3: must compare" << std::endl;
+			std::set< unsigned > cset, cset2;
+			std::vector< unsigned > cdiff;
+			std::set< Node > vset;
+			getCharSet(r1, cset, vset);
+			getCharSet(r2, cset2, vset);
+			if(vset.empty()) {
+				std::set_symmetric_difference(cset.begin(), cset.end(), cset2.begin(), cset2.end(), std::back_inserter(cdiff));
+				if(cdiff.empty()) {
+					Trace("regexp-intersect") << "INTERSECT Case 3.1: compare" << std::endl;
+					cset.clear();
+					firstChars(r1, cset, vset);
+					std::vector< Node > vec_nodes;
+					for(std::set<unsigned>::const_iterator itr = cset.begin();
+						itr != cset.end(); itr++) {
+						CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+						std::pair< Node, Node > p(r1, r2);
+						if(cache[ *itr ].find(p) == cache[ *itr ].end()) {
+							Node r1l = derivativeSingle(r1, c);
+							Node r2l = derivativeSingle(r2, c);
+							std::map< unsigned, std::set< PairNodes > > cache2(cache);
+							PairNodes p(r1l, r2l);
+							cache2[ *itr ].insert( p );
+							Node rt = intersectInternal(r1l, r2l, cache2);
+							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);
+					rNode = Rewriter::rewrite( rNode );
+				} else {
+					Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl;
+					rNode = d_emptyRegexp;
+				}
+			} else {
+				//TODO: non-empty var set
+				AlwaysAssert( false, "Unsupported Yet, 927 REO" );
+			}
+		}
+		d_inter_cache[p] = rNode;
+	}
+	Trace("regexp-intersect") << "INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
+	return rNode;
+}
+Node RegExpOpr::intersect(Node r1, Node r2) {
+	std::map< unsigned, std::set< PairNodes > > cache;
+	return intersectInternal(r1, r2, cache);
+}
 //printing
 std::string RegExpOpr::niceChar( Node r ) {
 	if(r.isConst()) {
@@ -842,12 +1068,12 @@ std::string RegExpOpr::mkString( Node r ) {
 				break;
 			}
 			case kind::REGEXP_CONCAT: {
-				retStr += "(";
+				//retStr += "(";
 				for(unsigned i=0; i<r.getNumChildren(); ++i) {
-					if(i != 0) retStr += ".";
+					//if(i != 0) retStr += ".";
 					retStr += mkString( r[i] );
 				}
-				retStr += ")";
+				//retStr += ")";
 				break;
 			}
 			case kind::REGEXP_UNION: {
@@ -897,7 +1123,7 @@ std::string RegExpOpr::mkString( Node r ) {
 			}
 			default:
 				Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
-				//AlwaysAssert( false );
+				//Assert( false );
 				//return Node::null();
 		}
 	}
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 7b41c1764..9bd694f5c 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -1,17 +1,17 @@
-/*********************                                                        */
-/*! \file regexp_operation.h
- ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Regular Expression Operations
+/*********************                                                        */
+/*! \file regexp_operation.h
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
  **
- ** Regular Expression Operations
+ ** \brief Symbolic Regular Expresion Operations
+ **
+ ** Symbolic Regular Expression Operations
  **/
 
 #include "cvc4_private.h"
@@ -20,7 +20,10 @@
 #define __CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
 
 #include <vector>
+#include <set>
+#include <algorithm>
 #include "util/hash.h"
+#include "util/regexp.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
 //#include "context/cdhashmap.h"
@@ -31,11 +34,15 @@ namespace strings {
 
 class RegExpOpr {
 	typedef std::pair< Node, CVC4::String > PairDvStr;
+	typedef std::set< Node > SetNodes;
+	typedef std::pair< Node, Node > PairNodes;
 
 private:
+	unsigned d_card;
     Node d_emptyString;
     Node d_true;
     Node d_false;
+	Node d_emptySingleton;
 	Node d_emptyRegexp;
 	Node d_zero;
 	Node d_one;
@@ -45,12 +52,15 @@ private:
 	Node d_sigma;
 	Node d_sigma_star;
 	
-	std::map< std::pair< Node, Node >, Node > d_simpl_cache;
-	std::map< std::pair< Node, Node >, Node > d_simpl_neg_cache;
+	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, 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;
+	std::map< PairNodes, Node > d_inter_cache;
 	//bool checkStarPlus( Node t );
 	void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );
 	void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
@@ -58,6 +68,13 @@ private:
 	int gcd ( int a, int b );
 	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 );
+	void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
+
+	//TODO: for intersection
+	bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
+
 public:
 	RegExpOpr();
 
@@ -66,8 +83,8 @@ public:
 	int delta( Node r );
 	Node derivativeSingle( Node r, CVC4::String c );
 	bool guessLength( Node r, int &co );
-	void firstChar( Node r );
-	bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
+	Node intersect(Node r1, Node r2);
+
 	std::string mkString( Node r );
 };
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c44d2d334..7998669cf 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -55,6 +55,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	d_regexp_memberships(c),
 	d_regexp_ucached(u),
 	d_regexp_ccached(c),
+	d_str_re_map(c),
+	d_inter_cache(c),
 	d_regexp_ant(c),
 	d_input_vars(u),
 	d_input_var_lsum(u),
@@ -552,7 +554,7 @@ void TheoryStrings::check(Effort e) {
     atom = polarity ? fact : fact[0];
 	//must record string in regular expressions
 	if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-		d_regexp_memberships.push_back( assertion );
+		addMembership(assertion);
 		//d_equalityEngine.assertPredicate(atom, polarity, fact);
 	} else if (atom.getKind() == kind::STRING_STRCTN) {
 		if(polarity) {
@@ -2298,7 +2300,43 @@ bool TheoryStrings::checkMemberships() {
 	bool addedLemma = false;
 	std::vector< Node > processed;
 	std::vector< Node > cprocessed;
-	for( unsigned i=0; i<d_regexp_memberships.size(); i++ ){
+
+	if(options::stringEIT()) {
+		for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
+			itr_xr != d_str_re_map.end(); ++itr_xr ) {
+			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;
+						++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;
+					}
+				}
+			}
+		}
+	}
+
+	if(!addedLemma) {
+	  for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
 		//check regular expression membership
 		Node assertion = d_regexp_memberships[i];
 		if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
@@ -2449,6 +2487,7 @@ bool TheoryStrings::checkMemberships() {
 		if(d_conflict) {
 			break;
 		}
+	  }
 	}
 	if( addedLemma ){
 		if( !d_conflict ){
@@ -2735,6 +2774,45 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
 	}
 }
 
+void TheoryStrings::addMembership(Node assertion) {
+	d_regexp_memberships.push_back( assertion );
+
+	if(options::stringEIT()) {
+		bool polarity = assertion.getKind() != kind::NOT;
+		if(polarity) {
+			TNode atom = polarity ? assertion : assertion[0];
+			Node x = atom[0];
+			Node r = atom[1];
+			NodeList* lst;
+			NodeListMap::iterator itr_xr = d_str_re_map.find( x );
+			if( itr_xr == d_str_re_map.end() ){
+			  lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+																	ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+			  d_str_re_map.insertDataFromContextMemory( x, lst );
+			} else {
+			  lst = (*itr_xr).second;
+			}
+			//check
+		    for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) {
+				if( r == *itr ) {
+					return;
+				}
+			}
+			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;
+			}*/
+		}
+	}
+}
+
 //// Finite Model Finding
 
 Node TheoryStrings::getNextDecisionRequest() {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index e07c61a19..355c536dd 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -118,12 +118,6 @@ private:
 	 */
 	Node d_ufSubstr;
 
-	/**
-	 * Function symbol used to implement uninterpreted undefined string
-	 * semantics.  Needed to deal with partial str2int function.
-	 */
-	Node d_ufS2I;
-
 	// Constants
     Node d_emptyString;
 	Node d_emptyRegexp;
@@ -308,12 +302,15 @@ private:
 	NodeSet d_pos_ctn_cached;
 	NodeSet d_neg_ctn_cached;
 
-	// Regular Expression
+	// Symbolic Regular Expression
 private:
 	// regular expression memberships
 	NodeList d_regexp_memberships;
 	NodeSet d_regexp_ucached;
 	NodeSet d_regexp_ccached;
+	// intersection
+	NodeListMap d_str_re_map;
+	NodeNodeMap d_inter_cache;
 	// antecedant for why regexp membership must be true
 	NodeNodeMap d_regexp_ant;
 	// membership length
@@ -324,6 +321,7 @@ private:
 	CVC4::String getHeadConst( Node x );
 	bool splitRegExp( Node x, Node r, Node ant );
 	bool addMembershipLength(Node atom);
+	void addMembership(Node assertion);
 
 
 	// Finite Model Finding
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 684a480fb..fd5dff994 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -23,6 +23,13 @@ using namespace std;
 
 namespace CVC4 {
 
+void String::getCharSet(std::set<unsigned int> &cset) const {
+	for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
+		itr != d_str.end(); itr++) {
+			cset.insert( *itr );
+		}
+}
+
 std::string String::toString() const {
 	std::string str;
 	for(unsigned int i=0; i<d_str.size(); ++i) {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 7985f4072..512c2eff0 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -23,6 +23,7 @@
 #include <iostream>
 #include <iomanip>
 #include <string>
+#include <set>
 #include <sstream>
 #include "util/exception.h"
 //#include "util/integer.h"
@@ -31,7 +32,6 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC String {
-
 public:
   static unsigned int convertCharToUnsignedInt( char c ) {
 	int i = (int)c;
@@ -342,6 +342,7 @@ public:
 		 return -1;
 	 }
   }
+  void getCharSet(std::set<unsigned int> &cset) const;
 };/* class String */
 
 namespace strings {