minor printer fix; intersection fix

3 files changed, 40 insertions, 50 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 528436033..d719b4e1a 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1217,66 +1217,53 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 		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;

 			Node exp;

 			int r = delta((r1 == d_emptySingleton ? r2 : r1), exp);

 			if(r == 0) {

 				//TODO: variable

 				spflag = true;

-				//Assert( 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;

+			std::set< Node > vset, vset2;

 			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, 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);

+			getCharSet(r2, cset2, vset2);

+			if(vset.empty() && vset2.empty()) {

+				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, 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::REGEXP_UNION, vec_nodes);

-					rNode = Rewriter::rewrite( rNode );

-				} else {

-					Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl;

-					rNode = d_emptyRegexp;

 				}

+				rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :

+						NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);

+				rNode = Rewriter::rewrite( rNode );

 			} else {

 				//TODO: non-empty var set

 				spflag = true;

-				//Assert( false, "Unsupported Yet, 927 REO" );

 			}

 		}

 		d_inter_cache[p] = rNode;

@@ -1307,7 +1294,6 @@ Node RegExpOpr::complement(Node r, int &ret) {
 			std::set<unsigned> cset;

 			SetNodes vset;

 			firstChars(r, cset, vset);

-			Assert(!vset.empty(), "Regexp 1298 Error");

 			std::vector< Node > vec_nodes;

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

 				CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);

@@ -1330,6 +1316,7 @@ Node RegExpOpr::complement(Node r, int &ret) {
 			rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :

 						NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);

 		}

+		rNode = Rewriter::rewrite(rNode);

 		std::pair< Node, int > p(rNode, ret);

 		d_compl_cache[r] = p;

 	}

@@ -1340,9 +1327,10 @@ Node RegExpOpr::complement(Node r, int &ret) {
 std::string RegExpOpr::niceChar( Node r ) {

 	if(r.isConst()) {

 		std::string s = r.getConst<CVC4::String>().toString() ;

-		return s == "" ? "{E}" : ( s == " " ? "{ }" : s );

+		return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s );

 	} else {

-		return r.toString();

+		std::string ss = "$" + r.toString();

+		return ss;

 	}

 }

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

@@ -1365,12 +1353,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 += ".";

 					retStr += mkString( r[i] );

 				}

-				//retStr += ")";

+				retStr += ")";

 				break;

 			}

 			case kind::REGEXP_UNION: {

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a19d35d4b..9ed52e94a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2333,7 +2333,7 @@ bool TheoryStrings::checkMemberships() {
 	std::vector< Node > processed;
 	std::vector< Node > cprocessed;
 
-	if(options::stringEIT()) {
+	//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;
@@ -2391,7 +2391,7 @@ bool TheoryStrings::checkMemberships() {
 				}
 			}
 		}
-	}
+	//}
 
 	if(!addedLemma) {
 	  for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
@@ -2871,8 +2871,7 @@ void TheoryStrings::addMembership(Node assertion) {
 			}
 		}
 		lst->push_back( r );
-		d_regexp_memberships.push_back( assertion );
-	} else {
+	}/* else {
 		if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
 			int rt;
 			Node r2 = d_regexp_opr.complement(r, rt);
@@ -2881,7 +2880,8 @@ void TheoryStrings::addMembership(Node assertion) {
 		} else {
 			d_regexp_memberships.push_back( assertion );
 		}
-	}
+	}*/
+	d_regexp_memberships.push_back( assertion );
 }
 
 //// Finite Model Finding
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index fd5dff994..b6db624d5 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -56,7 +56,9 @@ std::string String::toString() const {
 			default  : {

 				std::stringstream ss;

 				ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);

-				s = "\\x" + ss.str();

+				std::string t = ss.str();

+				t = t.substr(t.size()-2, 2);

+				s = "\\x" + t;

 				//std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();

 			}

 		  }