From 48a1854491c99d61d21482115e18399195d4d365 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Aug 2021 10:21:48 -0500 Subject: [PATCH] Fix policy for rewriting string equalities (#6916) This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default. This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true. This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting. Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well. --- src/theory/strings/extf_solver.cpp | 2 +- src/theory/strings/sequences_rewriter.cpp | 96 +++++++++---------- src/theory/strings/sequences_rewriter.h | 19 ++-- src/theory/strings/strings_entail.cpp | 4 + src/theory/strings/theory_strings.cpp | 9 ++ src/theory/theory_inference_manager.cpp | 2 + test/regress/CMakeLists.txt | 6 +- .../regress/regress1/strings/issue6101-2.smt2 | 6 ++ test/regress/regress1/strings/issue6101.smt2 | 9 ++ test/regress/regress1/strings/issue6913.smt2 | 8 ++ 10 files changed, 101 insertions(+), 60 deletions(-) create mode 100644 test/regress/regress1/strings/issue6101-2.smt2 create mode 100644 test/regress/regress1/strings/issue6101.smt2 create mode 100644 test/regress/regress1/strings/issue6913.smt2 diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 98f7d7d7c..32726f4ae 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -228,7 +228,7 @@ void ExtfSolver::checkExtfReductions(int effort) for (const Node& n : extf) { Assert(!d_state.isInConflict()); - Trace("strings-process") + Trace("strings-extf-debug") << " check " << n << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl; bool ret = doReduction(effort, n); diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index d3360403e..7885c857e 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -55,15 +55,44 @@ Node SequencesRewriter::rewriteEquality(Node node) Node ret = NodeManager::currentNM()->mkConst(false); return returnRewrite(node, ret, Rewrite::EQ_CONST_FALSE); } + // standard ordering + if (node[0] > node[1]) + { + Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]); + return returnRewrite(node, ret, Rewrite::EQ_SYM); + } + return node; +} +Node SequencesRewriter::rewriteEqualityExt(Node node) +{ + Assert(node.getKind() == EQUAL); + TypeNode tn = node[0].getType(); + if (tn.isInteger()) + { + return rewriteArithEqualityExt(node); + } + if (tn.isStringLike()) + { + return rewriteStrEqualityExt(node); + } + return node; +} + +Node SequencesRewriter::rewriteStrEqualityExt(Node node) +{ + Assert(node.getKind() == EQUAL && node[0].getType().isStringLike()); + TypeNode stype = node[0].getType(); + + NodeManager* nm = NodeManager::currentNM(); // ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false ) for (unsigned r = 0; r < 2; r++) { // must call rewrite contains directly to avoid infinite loop - // we do a fix point since we may rewrite contains terms to simpler - // contains terms. - Node ctn = d_stringsEntail.checkContains(node[r], node[1 - r], false); - if (!ctn.isNull()) + Node ctn = nm->mkNode(STRING_CONTAINS, node[r], node[1 - r]); + ctn = rewriteContains(ctn); + Assert(!ctn.isNull()); + if (ctn.isConst()) { if (!ctn.getConst()) { @@ -126,41 +155,7 @@ Node SequencesRewriter::rewriteEquality(Node node) } } - // standard ordering - if (node[0] > node[1]) - { - Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]); - return returnRewrite(node, ret, Rewrite::EQ_SYM); - } - return node; -} - -Node SequencesRewriter::rewriteEqualityExt(Node node) -{ - Assert(node.getKind() == EQUAL); - if (node[0].getType().isInteger()) - { - return rewriteArithEqualityExt(node); - } - if (node[0].getType().isStringLike()) - { - return rewriteStrEqualityExt(node); - } - return node; -} - -Node SequencesRewriter::rewriteStrEqualityExt(Node node) -{ - Assert(node.getKind() == EQUAL && node[0].getType().isStringLike()); - TypeNode stype = node[0].getType(); - - NodeManager* nm = NodeManager::currentNM(); - std::vector c[2]; Node new_ret; - for (unsigned i = 0; i < 2; i++) - { - utils::getConcat(node[i], c[i]); - } // ------- equality unification bool changed = false; for (unsigned i = 0; i < 2; i++) @@ -213,7 +208,8 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // original node was an equality but we may be able to do additional // rewriting here, e.g., // x++y = "" --> x = "" and y = "" - return returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY, true); + new_ret = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY); + return rewriteStrEqualityExt(new_ret); } } @@ -292,7 +288,8 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // original node was an equality but we may be able to do additional // rewriting here. new_ret = lhs.eqNode(ss); - return returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST, true); + new_ret = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST); + return rewriteStrEqualityExt(new_ret); } } } @@ -544,7 +541,6 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) } } } - return node; } @@ -1555,6 +1551,9 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) << std::endl; if (node != retNode) { + // also post process the rewrite, which may apply extended rewriting to + // equalities, if we rewrite to an equality from a non-equality + retNode = postProcessRewrite(node, retNode); Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite " << node << " to " << retNode << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, retNode); @@ -3482,21 +3481,20 @@ Node SequencesRewriter::rewriteSeqUnit(Node node) return node; } -Node SequencesRewriter::returnRewrite(Node node, - Node ret, - Rewrite r, - bool rewriteEqAgain) +Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r << "." << std::endl; - - NodeManager* nm = NodeManager::currentNM(); - if (d_statistics != nullptr) { (*d_statistics) << r; } + return ret; +} +Node SequencesRewriter::postProcessRewrite(Node node, Node ret) +{ + NodeManager* nm = NodeManager::currentNM(); // standard post-processing // We rewrite (string) equalities immediately here. This allows us to forego // the standard invariant on equality rewrites (that s=t must rewrite to one @@ -3529,7 +3527,7 @@ Node SequencesRewriter::returnRewrite(Node node, { ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0])); } - else if (retk == EQUAL && (rewriteEqAgain || node.getKind() != EQUAL)) + else if (retk == EQUAL && node.getKind() != EQUAL) { Trace("strings-rewrite") << "Apply extended equality rewrite on " << ret << std::endl; diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 9127637aa..0068c72c1 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -116,16 +116,8 @@ class SequencesRewriter : public TheoryRewriter * * The rewrite r indicates the justification for the rewrite, which is printed * by this function for debugging. - * - * If node is not an equality (or rewriteEq is true) and ret is an equality, - * this method applies an additional rewrite step (rewriteEqualityExt) that - * performs additional rewrites on ret, after which we return the result of - * this call. Otherwise, this method simply returns ret. */ - Node returnRewrite(Node node, - Node ret, - Rewrite r, - bool rewriteEqAgain = false); + Node returnRewrite(Node node, Node ret, Rewrite r); public: RewriteResponse postRewrite(TNode node) override; @@ -298,6 +290,15 @@ class SequencesRewriter : public TheoryRewriter */ static Node canonicalStrForSymbolicLength(Node n, TypeNode stype); + /** + * post-process rewrite + * + * If node is not an equality and ret is an equality, + * this method applies an additional rewrite step (rewriteEqualityExt) that + * performs additional rewrites on ret, after which we return the result of + * this call. Otherwise, this method simply returns ret. + */ + Node postProcessRewrite(Node node, Node ret); /** Reference to the rewriter statistics. */ HistogramStat* d_statistics; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 3fa11cc24..3c7800f8f 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -688,6 +688,10 @@ Node StringsEntail::checkContains(Node a, Node b, bool fullRewriter) { prev = ctn; ctn = d_rewriter.rewriteContains(ctn); + if (ctn != prev) + { + ctn = d_rewriter.postProcessRewrite(prev, ctn); + } } while (prev != ctn && ctn.getKind() == STRING_CONTAINS); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8912bad3b..c526decf1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -993,6 +993,15 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + if (atom.getKind() == EQUAL) + { + // always apply aggressive equality rewrites here + Node ret = d_rewriter.rewriteEqualityExt(atom); + if (ret != atom) + { + return TrustNode::mkTrustRewrite(atom, ret, nullptr); + } + } if (atom.getKind() == STRING_FROM_CODE) { // str.from_code(t) ---> diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index bad90f061..1c47c00c4 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -259,6 +259,8 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, d_lemmaIdStats << id; smt::currentResourceManager()->spendResource(id); Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; + // shouldn't send trivially true or false lemmas + Assert(!Rewriter::rewrite(tlem.getProven()).isConst()); d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); return true; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2f807d939..83d240b6b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1204,7 +1204,6 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/parser-syms.cvc - regress0/strings/quad-028-2-2-unsat.smt2 regress0/strings/re_diff.smt2 regress0/strings/re-in-rewrite.smt2 regress0/strings/re-syntax.smt2 @@ -2152,6 +2151,8 @@ set(regress_1_tests regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 regress1/strings/issue6072-inc-no-const-reg.smt2 regress1/strings/issue6075-repl-len-one-rr.smt2 + regress1/strings/issue6101.smt2 + regress1/strings/issue6101-2.smt2 regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/issue6191-replace-all.smt2 @@ -2174,6 +2175,7 @@ set(regress_1_tests regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 + regress1/strings/issue6913.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -2654,6 +2656,8 @@ set(regression_disabled_tests regress0/auflia/fuzz01.smtv1.smt2 ### regress0/bv/test00.smtv1.smt2 + # timeout after changes to equality rewriting policy in strings + regress0/strings/quad-028-2-2-unsat.smt2 # FIXME #1649 regress0/datatypes/datatype-dump.cvc # no longer support overloaded symbols across multiple parametric datatypes diff --git a/test/regress/regress1/strings/issue6101-2.smt2 b/test/regress/regress1/strings/issue6101-2.smt2 new file mode 100644 index 000000000..782558cd4 --- /dev/null +++ b/test/regress/regress1/strings/issue6101-2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(declare-fun x () String) +(assert (not (= x (str.replace x (str.replace "B" (str.replace x (str.replace x "A" "B") "B") "B") "B")))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6101.smt2 b/test/regress/regress1/strings/issue6101.smt2 new file mode 100644 index 000000000..532c6b1e0 --- /dev/null +++ b/test/regress/regress1/strings/issue6101.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) +(assert (= (= x (str.replace x (str.replace "B" (str.replace x (str.replace x "A" "B") "B") "B") "B")) (not (= +(not (not (= (= "A" (str.replace x "A" "B")) false))) (not (not (= (= "A" (str.replace x "A" "B")) false))))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6913.smt2 b/test/regress/regress1/strings/issue6913.smt2 new file mode 100644 index 000000000..35626f227 --- /dev/null +++ b/test/regress/regress1/strings/issue6913.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () String) +(assert + (= (str.++ a "0" (str.at (str.substr (str.++ a a a) 0 3) (str.len a)) "A") + (str.++ "0" (str.from_code (str.len a)) (str.replace "AA" (str.++ a "AA") a)))) +(check-sat) -- 2.30.2