From 49215e6948aba1d6b762e28a7293581e25c2df8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Dec 2020 15:04:35 -0600 Subject: [PATCH] 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. --- src/theory/strings/core_solver.cpp | 26 +++++++++++++++---- test/regress/CMakeLists.txt | 1 + .../strings/issue5611-deq-norm-emp.smt2 | 10 +++++++ 3 files changed, 32 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 48116bc24..dc7b11144 100644 --- 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& 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 antec; @@ -2251,10 +2261,16 @@ bool CoreSolver::processSimpleDeq(std::vector& nfi, // x = "" ^ ... Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl; + // the antecedant std::vector ant; + // the antecedant that is not explainable in this context + std::vector 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 cc; @@ -2266,7 +2282,7 @@ bool CoreSolver::processSimpleDeq(std::vector& 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 063c4b6e2..304ea2290 100644 --- 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 index 000000000..3b3e2cfab --- /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) -- 2.30.2