From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 28 Mar 2014 20:17:22 +0000 (-0500)
Subject: minor printer fix; intersection fix
X-Git-Tag: cvc5-1.0.0~6994
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=efe23f3a0b6b9e42927420a27198d06dd02766ba;p=cvc5.git

minor printer fix; intersection fix
---

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();
 			}
 		  }