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 125c1292a45ba157fb19431068be7bce31ec4c0a..96d880a8a47d88a6255e3a240b7566f455f70578 100644 (file)
--- 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 20c5e90f73dc6ac0e63411f9f0e09ded31708e91..7da24bb64f76907d0875dcb25a1554b193557582 100644 (file)
--- 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 );