Strengthen str.indexof rewriterewIndexOf

2 files changed, 41 insertions, 18 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 4ab81da7c..884e9ed86 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1989,24 +1989,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
           return returnRewrite(node, ret, "idof-def-ctn");
         }
       }
-
-      // strip symbolic length
-      Node new_len = node[2];
-      std::vector<Node> nr;
-      if (stripSymbolicLength(children0, nr, 1, new_len))
-      {
-        // For example:
-        // z>str.len( x1 ) and str.contains( x2, y )-->true
-        // implies
-        // str.indexof( str.++( x1, x2 ), y, z ) --->
-        // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
-        Node nn = mkConcat(kind::STRING_CONCAT, children0);
-        Node ret =
-            nm->mkNode(kind::PLUS,
-                       nm->mkNode(kind::MINUS, node[2], new_len),
-                       nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
-        return returnRewrite(node, ret, "idof-strip-sym-len");
-      }
     }
     else
     {
@@ -2016,6 +1998,24 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
     }
   }
 
+  // strip symbolic length
+  Node new_len = node[2];
+  std::vector<Node> nr;
+  if (stripSymbolicLength(children0, nr, 1, new_len))
+  {
+    // For example:
+    // z>str.len( x1 )
+    // implies
+    // str.indexof( str.++( x1, x2 ), y, z ) --->
+    // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
+    Node nn = mkConcat(kind::STRING_CONCAT, children0);
+    Node ret =
+        nm->mkNode(kind::PLUS,
+                   nm->mkNode(kind::MINUS, node[2], new_len),
+                   nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
+    return returnRewrite(node, ret, "idof-strip-sym-len");
+  }
+
   if (node[2].isConst() && node[2].getConst<Rational>().sgn()==0)
   {
     std::vector<Node> cb;
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index acee9754b..e2ab390b9 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -245,4 +245,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr);
     TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr);
   }
+
+  void testRewriteIndexOf()
+  {
+    TypeNode strType = d_nm->stringType();
+
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node x = d_nm->mkVar("x", strType);
+    Node one = d_nm->mkConst(Rational(1));
+
+    // Same normal form for:
+    //
+    // (str.to.int (str.indexof "A" x 1))
+    //
+    // (str.to.int (str.indexof "B" x 1))
+    Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one);
+    Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x);
+    Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one);
+    Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x);
+    Node res_itos_a_idof_x = Rewriter::rewrite(itos_a_idof_x);
+    Node res_itos_b_idof_x = Rewriter::rewrite(itos_b_idof_x);
+    TS_ASSERT_EQUALS(res_itos_a_idof_x, res_itos_b_idof_x);
+  }
 };