Fix indexof_re reduction (#8065)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Feb 2022 18:17:13 +0000 (12:17 -0600)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 18:17:13 +0000 (18:17 +0000)
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
test/regress/CMakeLists.txt
test/regress/regress1/strings/issue6654-indexof_re_red.smt2 [new file with mode: 0644]

index 97dbd2b3fbe363888c4a3c09e5259db495c496b5..56dcbe25cc3592bc3aabcb772ba10e88b949bcf9 100644 (file)
@@ -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.
index 1d231ea884ce2960b2973725e275bb39065166ee..7698b19aab08ba64cfb68251113f4f95b741232b 100644 (file)
@@ -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 (file)
index 0000000..73607e4
--- /dev/null
@@ -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)