[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.

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 6e67352b3620728996b29770a5ac897312913a9f..d3360403e342b419409a2a17b3ecb1840c57ca14 100644 (file)
--- 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 37ed787860858ab329ade53da46224a6d9855e7d..9127637aa3b349f6d790899bafa8d3ecbf97034e 100644 (file)
--- 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 00a50a69c5c1b1efbef820c2b12375a88b009350..18e9d9864be61cffc653c714451794e68e55d2a9 100644 (file)
--- 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 (file)
index 0000000..e2579ac
--- /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)