From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 23 Jan 2014 22:59:58 +0000 (-0600)
Subject: fix: constants are inferred to be the same
X-Git-Tag: cvc5-1.0.0~7130
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b68af471e96ba36ddd1bd135608fe5a6239bfc22;p=cvc5.git

fix: constants are inferred to be the same
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 125c1292a..96d880a8a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1050,6 +1050,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 							} else if( areEqual(length_term_i, length_term_j) ) {
 								Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl;
 								Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
+								eq = Rewriter::rewrite( eq );
 								Node length_eq = length_term_i.eqNode( length_term_j );
 								std::vector< Node > temp_exp;
 								temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
@@ -1057,10 +1058,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
 								Node eq_exp = temp_exp.empty() ? d_true :
 												temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp );
 								Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
-								d_pending.push_back( eq );
-								d_pending_exp[eq] = eq_exp;
-								d_infer.push_back(eq);
-								d_infer_exp.push_back(eq_exp);
+								sendInfer( eq_exp, eq, "LengthEq" );
 								return true;
 							} else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
 									  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) {
@@ -1471,6 +1469,18 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
 	}
 }
 
+void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
+	eq = Rewriter::rewrite( eq );
+	if( eq==d_false ){
+		sendLemma( eq_exp, eq, c );
+	}else{
+		d_pending.push_back( eq );
+		d_pending_exp[eq] = eq_exp;
+		d_infer.push_back(eq);
+		d_infer_exp.push_back(eq_exp);
+	}
+}
+
 void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) {
 	Node eq = a.eqNode( b );
 	eq = Rewriter::rewrite( eq );
@@ -1721,12 +1731,8 @@ bool TheoryStrings::checkNormalForms() {
 				//two equivalence classes have same normal form, merge
 				Node eq_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ) );
 				Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] );
-				Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl;
+				sendInfer( eq_exp, eq, "Normal_Form" );
 				//d_equalityEngine.assertEquality( eq, true, eq_exp );
-				d_pending.push_back( eq );
-				d_pending_exp[eq] = eq_exp;
-				d_infer.push_back(eq);
-				d_infer_exp.push_back(eq_exp);
 			}else{
 				nf_to_eqc[nf_term] = eqc;
 				eqc_to_exp[eqc] = nf_term_exp;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 20c5e90f7..7da24bb64 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -246,6 +246,7 @@ protected:
 	void doPendingLemmas();
 
 	void sendLemma( Node ant, Node conc, const char * c );
+	void sendInfer( Node eq_exp, Node eq, const char * c );
 	void sendSplit( Node a, Node b, const char * c, bool preq = true );
 	/** mkConcat **/
 	Node mkConcat( Node n1, Node n2 );