From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 6 Nov 2013 23:18:31 +0000 (-0600)
Subject: bug fix
X-Git-Tag: cvc5-1.0.0~7267^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78f1deb6dcb2492275642ff3a52b5611b95fecbb;p=cvc5.git

bug fix
---

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0a7701862..fa686dd9f 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -31,6 +31,7 @@ RegExpOpr::RegExpOpr() {
 }
 
 bool RegExpOpr::checkConstRegExp( Node r ) {
+	Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
 	bool ret = true;
 	if( d_cstre_cache.find( r ) != d_cstre_cache.end() ) {
 		ret = d_cstre_cache[r];
@@ -159,7 +160,7 @@ int RegExpOpr::delta( Node r ) {
 //null - no solution
 Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 	Assert( c.size() < 2 );
-	Trace("strings-regexp-derivative") << "RegExp-derivative starts with " << mkString( r ) << ", c=" << c << std::endl;
+	Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
 	Node retNode = Node::null();
 	PairDvStr dv = std::make_pair( r, c );
 	if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
@@ -236,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;
 				}
 				retNode = vec_nodes.size() == 0 ? Node::null() :
 							( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
@@ -296,16 +297,16 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 				break;
 			case kind::REGEXP_OPT:
 			{
-				return derivativeSingle(r[0], c);
+				retNode = derivativeSingle(r[0], c);
 			}
 				break;
 			case kind::REGEXP_RANGE:
 			{
 				char ch = c.getFirstChar();
 				if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {
-					return d_emptyString;
+					retNode = d_emptyString;
 				} else {
-					return Node::null();
+					retNode = Node::null();
 				}
 			}
 				break;
@@ -315,6 +316,9 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
 				//AlwaysAssert( false );
 				//return Node::null();
 		}
+		if(!retNode.isNull()) {
+			retNode = Rewriter::rewrite( retNode );
+		}
 		d_dv_cache[dv] = retNode;
 	}
 	Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) )  << std::endl;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e5ce2d6d3..fc4b3ba9c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1017,17 +1017,19 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											//d_pending_req_phase[ x_empty ] = true;
 											if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
 												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
-												sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" );
+												sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty x" );
 												return true;
-											} else if( !areDisequal( t_yz, d_emptyString ) ) {
+											} else if( !areDisequal( t_yz, d_emptyString ) && t_yz.getKind()!=kind::CONST_STRING  ) {
 												//TODO...........
 												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
-												sendSplit( t_yz, d_emptyString, "Loop Empty" );
+												sendSplit( t_yz, d_emptyString, "Loop Empty yz" );
 												return true;
 											} else {
 												//need to break
 												antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
-												antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+												if( t_yz.getKind()!=kind::CONST_STRING ){
+													antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
+												}
 												Node ant = mkExplain( antec, antec_new_lits );
 												Node str_in_re;
 												if( s_zy == t_yz &&
@@ -1977,7 +1979,6 @@ bool TheoryStrings::checkMemberships() {
 				Assert( atom.getKind()==kind::STRING_IN_REGEXP );
 				Node x = atom[0];
 				Node r = atom[1];
-				//TODO
 				Assert( r.getKind()==kind::REGEXP_STAR );
 				if( !areEqual( x, d_emptyString ) ){
 					//if(splitRegExp( x, r, atom )) {
@@ -2039,11 +2040,11 @@ bool TheoryStrings::checkMemberships() {
 }
 
 CVC4::String TheoryStrings::getHeadConst( Node x ) {
-	if( x.isConst() && x != d_emptyString ) {
+	if( x.isConst() ) {
 		return x.getConst< String >();
 	} else if( x.getKind() == kind::STRING_CONCAT ) {
-		if( x[0].isConst() && x[0] != d_emptyString ) {
-			return x.getConst< String >();
+		if( x[0].isConst() ) {
+			return x[0].getConst< String >();
 		} else {
 			return d_emptyString.getConst< String >();
 		}
@@ -2053,47 +2054,65 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) {
 }
 
 bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
-	x =  Rewriter::rewrite( x );
-	if(x == d_emptyString) {
-		if(d_regexp_opr.delta( r ) == 1) {
-		}
-		return false;
-	} else {
-		CVC4::String s = getHeadConst( x );
-		if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
-			Node conc = Node::null();
-			Node dc = r;
-			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.isNull()) {
-					// CONFLICT
-					flag = false;
-					break;
-				}
+	// TODO cstr in vre
+	Assert(x != d_emptyString);
+	Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+	CVC4::String s = getHeadConst( x );
+	if( !s.isEmptyString() && d_regexp_opr.checkConstRegExp( r ) ) {
+		Node conc = Node::null();
+		Node dc = r;
+		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.isNull()) {
+				// CONFLICT
+				flag = false;
+				break;
 			}
-			// send lemma
-			if(flag) {
-				Node left = Node::null();
-				if(x.isConst()) {
-					left = d_emptyString;
-					if(d_regexp_opr.delta(dc)) {
-						//TODO yes
-					} else {
-						// TODO conflict
-					}
+		}
+		// send lemma
+		if(flag) {
+			if(x.isConst()) {
+				/*
+				left = d_emptyString;
+				if(d_regexp_opr.delta(dc) == 1) {
+					//TODO yes possible?
+				} else if(d_regexp_opr.delta(dc) == 0) {
+					//TODO possible?
 				} else {
-					//TODO find x rest
-					conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, dc );
+					// TODO conflict possible?
+				}*/
+				Assert(false, "Impossible: TheoryStrings::splitRegExp: const string in const regular expression.");
+				return false;
+			} else {
+				Assert( x.getKind() == kind::STRING_CONCAT );
+				std::vector< Node > vec_nodes;
+				for(unsigned int i=1; i<x.getNumChildren(); ++i ) {
+					vec_nodes.push_back( x[i] );
 				}
+				Node left = vec_nodes.size() == 1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec_nodes );
+				left = Rewriter::rewrite( left );
+				conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
+
+				std::vector< Node > sdc;
+				sdc.push_back( conc );
+
+				StringsPreprocess spp;
+				spp.simplify( sdc );
+				for( unsigned i=1; i<sdc.size(); i++ ){
+					//add the others as lemmas
+					sendLemma( d_true, sdc[i], "RegExp Definition");
+				}
+				
+				conc = sdc[0];
 			}
-			sendLemma(ant, conc, "RegExp Const Split");
-		} else {
-			return false;
 		}
+		sendLemma(ant, conc, "RegExp Const Split");
+		return true;
+	} else {
+		return false;
 	}
-	return false;
 }
 
 Node TheoryStrings::getNextDecisionRequest() {