From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 12 Feb 2014 22:10:07 +0000 (-0600)
Subject: bug fix for reverse check
X-Git-Tag: cvc5-1.0.0~7091
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e1d725478eb24433eaf0f70822550966ef53d3d;p=cvc5.git

bug fix for reverse check
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e75f1f34e..f1b6c133a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -980,9 +980,10 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
 				vec_r.insert(vec_r.begin(), sk_z);
 				Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
 				Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
+				Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
 				str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
 								NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
-									NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) );
+									NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, restr ) ) );
 
 				//Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y );
 				//Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString));
@@ -1257,8 +1258,12 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
 						int index_k = r==0 ? index_i : index_j;
 						int k = r==0 ? i : j;
 						std::vector< Node > eqnc;
-						for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
-							eqnc.push_back( normal_forms[k][index_l] );
+						for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
+							if(isRev) {
+								eqnc.insert(eqnc.begin(), normal_forms[k][index_l] );
+							} else {
+								eqnc.push_back( normal_forms[k][index_l] );
+							}
 						}
 						eqn.push_back( mkConcat( eqnc ) );
 					}
@@ -1957,6 +1962,19 @@ bool TheoryStrings::checkNormalForms() {
   } while ( !d_conflict && d_lemma_cache.empty() && addedFact );
 
   //process disequalities between equivalence classes
+  checkDeqNF();
+
+  Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
+  //flush pending lemmas
+  if( !d_lemma_cache.empty() ){
+	doPendingLemmas();
+	return true;
+  }else{
+	return false;
+  }
+}
+
+void TheoryStrings::checkDeqNF() {
   if( !d_conflict && d_lemma_cache.empty() ){
 	  std::vector< Node > eqcs;
 	  getEquivalenceClasses( eqcs );
@@ -1972,9 +1990,10 @@ bool TheoryStrings::checkNormalForms() {
 			//must ensure that normal forms are disequal
 			for( unsigned j=0; j<cols[i].size(); j++ ){
 				for( unsigned k=(j+1); k<cols[i].size(); k++ ){
+					Assert( !d_conflict );
 					if( !areDisequal( cols[i][j], cols[i][k] ) ){
 						sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
-						break;
+						return;
 					}else{
 						Trace("strings-solve") << "- Compare ";
 						printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
@@ -1982,21 +2001,13 @@ bool TheoryStrings::checkNormalForms() {
 						printConcat( d_normal_forms[cols[i][k]], "strings-solve" );
 						Trace("strings-solve")  << "..." << std::endl;
 						if( processDeq( cols[i][j], cols[i][k] ) ){
-							break;
+							return;
 						}
 					}
 				}
 			}
 		}
-	  }
-  }
-
-  //flush pending lemmas
-  if( !d_lemma_cache.empty() ){
-	doPendingLemmas();
-	return true;
-  }else{
-	return false;
+	 }
   }
 }
 
@@ -2050,11 +2061,12 @@ bool TheoryStrings::checkCardinality() {
   for( unsigned i = 0; i<cols.size(); ++i ){
     Node lr = lts[i];
     Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
-    // size > c^k
-    double k = (int)cols[i].size() < cardinality ? 0.0 : (std::log((double) cols[i].size() ) / log((double) cardinality));
-    unsigned int int_k = (unsigned int) k;
-    //double c_k = pow ( (double)cardinality, (double)lr );
     if( cols[i].size() > 1 ) {
+		// size > c^k
+		double k = 1.0 + std::log((double) cols[i].size() - 1) / log((double) cardinality);
+		unsigned int int_k = (unsigned int) k;
+		//double c_k = pow ( (double)cardinality, (double)lr );
+
         bool allDisequal = true;
         for( std::vector< Node >::iterator itr1 = cols[i].begin();
               itr1 != cols[i].end(); ++itr1) {
@@ -2088,7 +2100,7 @@ bool TheoryStrings::checkCardinality() {
                 }
                 Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node );
                 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
-                Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node );
+                Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node );
 				/*
 				sendLemma( antc, cons, "Cardinality" );
 				ei->d_cardinality_lem_k.set( int_k+1 );
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5d8ff016f..3143d6e89 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -224,6 +224,7 @@ private:
 
 	bool checkSimple();
     bool checkNormalForms();
+	void checkDeqNF();
 	bool checkLengthsEqc();
     bool checkCardinality();
     bool checkInductiveEquations();