diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-27 15:42:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 22:42:10 +0000 |
| commit | 29f0b8f378377ed836bddaaf88883d0b2eeb545d (patch) | |
| tree | 5d9edb57c60ab8c8a07dab52f18b72dd441d4fdf /src/theory/strings/rewrites.h | |
| parent | 631032b15327c28c44b51490dceb434a38f3419a (diff) | |
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.
Diffstat (limited to 'src/theory/strings/rewrites.h')
| -rw-r--r-- | src/theory/strings/rewrites.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 482666faa..5e63c55c8 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -73,6 +73,10 @@ enum class Rewrite : uint32_t IDOF_PULL_ENDPT, IDOF_STRIP_CNST_ENDPTS, IDOF_STRIP_SYM_LEN, + INDEXOF_RE_EMP_RE, + INDEXOF_RE_EVAL, + INDEXOF_RE_INVALID_INDEX, + INDEXOF_RE_MAX_INDEX, ITOS_EVAL, RE_AND_EMPTY, RE_ANDOR_FLATTEN, |