From f4b167eb29e2716e996450d844a8bd4de626d7f6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Feb 2022 12:17:13 -0600
Subject: [PATCH] Fix indexof_re reduction (#8065)

Fixes https://github.com/cvc5/cvc5/issues/6654.

Note that this regression now answers unknown with `--ext-rewrite-quant`; the regression without this option is added.
---
 src/theory/strings/theory_strings_preprocess.cpp | 16 ++++++++++------
 test/regress/CMakeLists.txt                      |  1 +
 .../strings/issue6654-indexof_re_red.smt2        |  8 ++++++++
 3 files changed, 19 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress1/strings/issue6654-indexof_re_red.smt2

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 97dbd2b3f..56dcbe25c 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -298,11 +298,14 @@ Node StringsPreprocess::reduce(Node t,
         validLen,
         nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, s, skk, l), r));
     // skk != -1 =>
-    //   exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l), r))
-    Node match =
-        nm->mkNode(OR,
-                   retNegOne,
-                   utils::mkForallInternal(bvll, matchBody.negate()).negate());
+    //   skk >= n ^ exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l),
+    //   r))
+    Node match = nm->mkNode(
+        OR,
+        retNegOne,
+        nm->mkNode(AND,
+                   nm->mkNode(GEQ, skk, n),
+                   utils::mkForallInternal(bvll, matchBody.negate()).negate()));
 
     // assert:
     // IF:   n > len(s) OR 0 > n
@@ -313,7 +316,8 @@ Node StringsPreprocess::reduce(Node t,
     //         n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
     //           ~in_re(substr(s, i, l), r)) ^
     //       (skk != -1 =>
-    //          exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r))
+    //          skk >= n ^ exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s,
+    //          skk, l), r))
     //
     // Note that this reduction relies on eager reduction lemmas being sent to
     // properly limit the range of skk.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1d231ea88..7698b19aa 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2404,6 +2404,7 @@ set(regress_1_tests
   regress1/strings/issue6653-4-rre.smt2
   regress1/strings/issue6653-rre.smt2
   regress1/strings/issue6653-rre-small.smt2
+  regress1/strings/issue6654-indexof_re_red.smt2
   regress1/strings/issue6766-re-elim-bv.smt2
   regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/issue6913.smt2
diff --git a/test/regress/regress1/strings/issue6654-indexof_re_red.smt2 b/test/regress/regress1/strings/issue6654-indexof_re_red.smt2
new file mode 100644
index 000000000..73607e424
--- /dev/null
+++ b/test/regress/regress1/strings/issue6654-indexof_re_red.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (= b (str.replace_re a (str.to_re "A") "A")))
+(assert (not (str.prefixof (str.++ b b) a)))
+(check-sat)
-- 
2.30.2