Fix length assumption for deq norm emp rule (#5623)

There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.

Fixes #5611.

Note this inference was not previously covered in our coverage build.

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 48116bc240a5d09e7f209559999d940c6765f41a..dc7b111444a0c40b3051c7f9841ea36c2f3a04c9 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -525,6 +525,7 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
       ++eqc_i;
     }
     curr.pop_back();
+    Trace("strings-eqc") << "* add string eqc: " << eqc << std::endl;
     //now we can add it to the list of equivalence classes
     d_strings_eqc.push_back( eqc );
   }else{
@@ -651,8 +652,7 @@ void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype)
     d_normal_form[eqc] = normal_forms[nf_index];
     Trace("strings-process-debug")
         << "Return process equivalence class " << eqc
-        << " : returned, size = " << d_normal_form[eqc].d_nf.size()
-        << std::endl;
+        << " : returned = " << d_normal_form[eqc].d_nf << std::endl;
   }
 }
 
@@ -896,7 +896,9 @@ void CoreSolver::getNormalForms(Node eqc,
             // get the normal form for the component
             NormalForm& nfr = getNormalForm(nr);
             std::vector<Node>& nfrv = nfr.d_nf;
-            Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = "  << nr << std::endl;
+            Trace("strings-process-debug")
+                << "Normalizing subterm " << n[i] << " = " << nr
+                << ", which is " << nfrv << std::endl;
             unsigned orig_size = nf_curr.d_nf.size();
             unsigned add_size = nfrv.size();
             //if not the empty string, add to current normal form
@@ -993,6 +995,12 @@ void CoreSolver::getNormalForms(Node eqc,
         eqc_non_c = n;
       }
     }
+    else
+    {
+      Trace("strings-process-debug")
+          << "Get Normal Form : term " << n << " in eqc " << eqc
+          << " is congruent" << std::endl;
+    }
     ++eqc_i;
   }
 
@@ -1359,6 +1367,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         }
         eqn[r] = utils::mkNConcat(eqnc, stype);
       }
+      Trace("strings-solve-debug")
+          << "Endpoint eq check: " << eqn[0] << " " << eqn[1] << std::endl;
       if (!d_state.areEqual(eqn[0], eqn[1]))
       {
         std::vector<Node> antec;
@@ -2251,10 +2261,16 @@ bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi,
       //      x = "" ^ ...
       Trace("strings-solve-debug")
           << "Disequality normalize empty" << std::endl;
+      // the antecedant
       std::vector<Node> ant;
+      // the antecedant that is not explainable in this context
+      std::vector<Node> antn;
       Node niLenTerm = d_state.getLengthExp(ni, ant, nfni.d_base);
       Node njLenTerm = d_state.getLengthExp(nj, ant, nfnj.d_base);
-      ant.push_back(niLenTerm.eqNode(njLenTerm));
+      // length is not guaranteed to hold
+      Node leq = niLenTerm.eqNode(njLenTerm);
+      ant.push_back(leq);
+      antn.push_back(leq);
       ant.insert(ant.end(), nfni.d_exp.begin(), nfni.d_exp.end());
       ant.insert(ant.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
       std::vector<Node> cc;
@@ -2266,7 +2282,7 @@ bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi,
       Node conc = cc.size() == 1
                       ? cc[0]
                       : NodeManager::currentNM()->mkNode(kind::AND, cc);
-      d_im.sendInference(ant, conc, Inference::DEQ_NORM_EMP, isRev, true);
+      d_im.sendInference(ant, antn, conc, Inference::DEQ_NORM_EMP, isRev, true);
       return true;
     }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 063c4b6e2edebe6a213d11766512364594c92e23..304ea2290bfa112c7db72c4c10928d750405400a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1973,6 +1973,7 @@ set(regress_1_tests
   regress1/strings/issue5483-pp-leq.smt2
   regress1/strings/issue5510-re-consume.smt2
   regress1/strings/issue5520-re-consume.smt2
+  regress1/strings/issue5611-deq-norm-emp.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2
new file mode 100644 (file)
index 0000000..3b3e2cf
--- /dev/null
+++ b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -i --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun str7 () String)
+(declare-fun str8 () String)
+(declare-fun str9 () String)
+(assert (not (= str8 (str.replace_re_all (str.++ str9 str8 str7) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9))))
+(push)
+(assert (and (str.in_re str8 (str.to_re str7)) (not (= str9 (str.replace_re_all (str.++ str8 str8) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9)))))
+(check-sat)