Fix `str.replace_re` and `str.replace_re_all` (#6615)

Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.

1 files changed, 18 insertions, 0 deletions

diff --git a/test/regress/regress0/strings/indexof_re.smt2 b/test/regress/regress0/strings/indexof_re.smt2
new file mode 100644
index 000000000..72c5d7ee7
--- /dev/null
+++ b/test/regress/regress0/strings/indexof_re.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-const x String)
+(assert (or
+  (not (= (str.indexof_re "abc" re.allchar (- 1)) (- 1)))
+  (not (= (str.indexof_re "abc" re.allchar (- 2)) (- 1)))
+  (not (= (str.indexof_re "abc" re.allchar 5) (- 1)))
+  (not (= (str.indexof_re "abc" re.allchar 0) 0))
+  (not (= (str.indexof_re "abc" re.allchar 1) 1))
+  (not (= (str.indexof_re "abc" re.allchar 2) 2))
+  (not (= (str.indexof_re "abc" re.allchar 3) (- 1)))
+  (not (= (str.indexof_re "abc" (re.++ re.allchar re.allchar) 2) (- 1)))
+  (not (= (str.indexof_re "abc" (re.union (str.to_re "") re.allchar) 3) 3))
+  (not (= (str.indexof_re (str.++ "abc" x) (re.union (str.to_re "") re.allchar) 3) 3))
+  (not (= (str.indexof_re "cbabc" (re.union (str.to_re "a") (str.to_re "bab")) 0) 1))
+))
+(set-info :status unsat)
+(check-sat)