From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 7 Nov 2013 17:04:31 +0000 (-0600)
Subject: Adds the header file into makefile, solving building error; adds cache for derivative... 
X-Git-Tag: cvc5-1.0.0~7267^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4659954ecdafb95d093e85cdf5c89815845488ed;p=cvc5.git

Adds the header file into makefile, solving building error; adds cache for derivative; disables loop detection when finite model finding is enabled.
---

diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
index f7a6fa0a2..d5e5d1a23 100644
--- a/src/theory/strings/Makefile.am
+++ b/src/theory/strings/Makefile.am
@@ -14,6 +14,7 @@ libstrings_la_SOURCES = \
 	type_enumerator.h \
 	theory_strings_preprocess.h \
 	theory_strings_preprocess.cpp \
+	regexp_operation.h \
 	regexp_operation.cpp
 
 EXTRA_DIST = \
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fc4b3ba9c..5bc0e5cbe 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -48,6 +48,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
 	//d_lit_to_decide_index( c, 0 ),
 	//d_lit_to_decide( c ),
 	d_reg_exp_mem( c ),
+	//d_reg_exp_deriv( c ),
 	d_curr_cardinality( c, 0 )
 {
     // The kinds we are treating as function application in congruence
@@ -919,20 +920,22 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 										//check for loops
 										//Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl;
 										int has_loop[2] = { -1, -1 };
-										for( unsigned r=0; r<2; r++ ){
-											int index = (r==0 ? index_i : index_j);
-											int other_index = (r==0 ? index_j : index_i );
-											int n_index = (r==0 ? i : j);
-											int other_n_index = (r==0 ? j : i);
-											if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
-												for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
-													if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
-														has_loop[r] = lp;
-														break;
+										//if( !options::stringFMF() ) {
+											for( unsigned r=0; r<2; r++ ){
+												int index = (r==0 ? index_i : index_j);
+												int other_index = (r==0 ? index_j : index_i );
+												int n_index = (r==0 ? i : j);
+												int other_n_index = (r==0 ? j : i);
+												if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) {
+													for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){
+														if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
+															has_loop[r] = lp;
+															break;
+														}
 													}
 												}
 											}
-										}
+										//}
 										if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
 											int loop_n_index = has_loop[0]!=-1 ? i : j;
 											int other_n_index = has_loop[0]!=-1 ? j : i;
@@ -1373,6 +1376,9 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 		d_conflict = true;
 	}else{
 		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
+		if( ant == d_true ) {
+			lem = conc;
+		}
 		Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
 		d_lemma_cache.push_back( lem );
 	}
@@ -1974,29 +1980,36 @@ bool TheoryStrings::checkMemberships() {
 		Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
 		Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
 		bool polarity = assertion.getKind()!=kind::NOT;
-		if( polarity ){
-			if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){
-				Assert( atom.getKind()==kind::STRING_IN_REGEXP );
-				Node x = atom[0];
-				Node r = atom[1];
-				Assert( r.getKind()==kind::REGEXP_STAR );
-				if( !areEqual( x, d_emptyString ) ){
-					//if(splitRegExp( x, r, atom )) {
-					//	addedLemma = true;
-					//} else 
-					if( unrollStar( atom ) ) {
-						addedLemma = true;
-					} else {
-						Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl;
-						is_unk = true;
+		if( polarity ) {
+			Assert( atom.getKind()==kind::STRING_IN_REGEXP );
+			Node x = atom[0];
+			Node r = atom[1];
+			Assert( r.getKind()==kind::REGEXP_STAR );
+			if( !areEqual( x, d_emptyString ) ) {
+				bool flag = true;
+				if( d_reg_exp_deriv.find(atom)==d_reg_exp_deriv.end() ) {
+					if(splitRegExp( x, r, atom )) {
+						addedLemma = true; flag = false;
+						d_reg_exp_deriv[ atom ] = true;
 					}
-				}else{
-					Trace("strings-regexp") << "...is satisfied." << std::endl;
+				} else {
+					flag = false;
+					Trace("strings-regexp-derivative") << "... is processed by deriv." << std::endl;
 				}
-			}else{
-				Trace("strings-regexp") << "...Already unrolled." << std::endl;
+				if( flag && d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ) {
+						if( unrollStar( atom ) ) {
+							addedLemma = true;
+						} else {
+							Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl;
+							is_unk = true;
+						}
+				} else {
+					Trace("strings-regexp") << "...is already unrolled or splitted." << std::endl;
+				}
+			} else {
+				Trace("strings-regexp") << "...is satisfied." << std::endl;
 			}
-		}else{
+		} else {
 			//TODO: negative membership
 			//Node r = Rewriter::rewrite( atom[1] );
 			//r = d_regexp_opr.complement( r );
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index df31dcff7..7d4b740e4 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -154,6 +154,7 @@ class TheoryStrings : public Theory {
   NodeList d_reg_exp_mem;
   std::map< Node, bool > d_reg_exp_unroll;
   std::map< Node, int > d_reg_exp_unroll_depth;
+  std::map< Node, bool > d_reg_exp_deriv;
   //antecedant for why reg exp membership must be true
   std::map< Node, Node > d_reg_exp_ant;