From adf5216eff4e75dd9c5d08fce3bfc2161250c86e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 5 Jul 2021 06:29:09 -0700 Subject: [PATCH] [Strings] Fix incorrect rewrite (#6837) Fixes #6834. There were two cases in our extended rewriter for string equalities that were modifying the node without returning and without updating information computed from the original node. This mismatch led to incorrect rewrites. This commit fixes the issue by adding a flag to returnRewrite() that determines whether node that was an equality before and after the rewrite should be rewritten again with the extended rewriter. We generally do not do that (we'd run in danger of rewriting equality nodes with the extended rewriter even though we shouldn't) but for the rewrites that were previously continuing to rewrite the node, we set this flag and return. This ensures that we do not have an issue with information being out of date. The commit additionally fixes an issue where we would apply the rewrite STR_EQ_UNIFY even though the node hadn't changed. --- src/theory/strings/sequences_rewriter.cpp | 24 +++++++++++++++---- src/theory/strings/sequences_rewriter.h | 15 +++++++----- test/regress/CMakeLists.txt | 1 + .../issue6834-str-eq-const-nhomog.smt2 | 5 ++++ 4 files changed, 34 insertions(+), 11 deletions(-) create mode 100644 test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 6e67352b3..d3360403e 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -206,8 +206,15 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y Node s1 = utils::mkConcat(c[0], stype); Node s2 = utils::mkConcat(c[1], stype); - new_ret = s1.eqNode(s2); - node = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY); + if (s1 != node[0] || s2 != node[1]) + { + new_ret = s1.eqNode(s2); + // We generally don't apply the extended equality rewriter if the + // 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); + } } // ------- homogeneous constants @@ -280,8 +287,12 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // e.g. // "AA" = y ++ x ---> "AA" = x ++ y if x < y // "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z + // + // We generally don't apply the extended equality rewriter if the + // original node was an equality but we may be able to do additional + // rewriting here. new_ret = lhs.eqNode(ss); - node = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST); + return returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST, true); } } } @@ -3471,7 +3482,10 @@ Node SequencesRewriter::rewriteSeqUnit(Node node) return node; } -Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) +Node SequencesRewriter::returnRewrite(Node node, + Node ret, + Rewrite r, + bool rewriteEqAgain) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r << "." << std::endl; @@ -3515,7 +3529,7 @@ Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) { ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0])); } - else if (retk == EQUAL && node.getKind() != EQUAL) + else if (retk == EQUAL && (rewriteEqAgain || 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 37ed78786..9127637aa 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -117,12 +117,15 @@ 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 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); + * 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); public: RewriteResponse postRewrite(TNode node) override; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 00a50a69c..18e9d9864 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1178,6 +1178,7 @@ set(regress_0_tests regress0/strings/issue6604-re-elim.smt2 regress0/strings/issue6643-ctn-decompose-conflict.smt2 regress0/strings/issue6681-split-eq-strip-l.smt2 + regress0/strings/issue6834-str-eq-const-nhomog.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 b/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 new file mode 100644 index 000000000..e2579acf5 --- /dev/null +++ b/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_SLIA) +(declare-fun a () Int) +(assert (= (str.++ (str.substr "A" 0 a) "B" (str.substr "A" 0 a)) "B")) +(set-info :status sat) +(check-sat) -- 2.30.2