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/kinds | |
| 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/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 1353ca964..743a5c006 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -21,13 +21,12 @@ operator STRING_CHARAT 2 "string charat" operator STRING_STRCTN 2 "string contains" operator STRING_LT 2 "string less than" operator STRING_LEQ 2 "string less than or equal" -operator STRING_STRIDOF 3 "string indexof" +operator STRING_STRIDOF 3 "string index of substring" +operator STRING_INDEXOF_RE 3 "string index of regular expression match" operator STRING_STRREPL 3 "string replace" operator STRING_STRREPLALL 3 "string replace all" operator STRING_REPLACE_RE 3 "string replace regular expression match" operator STRING_REPLACE_RE_ALL 3 "string replace all regular expression matches" -typerule STRING_REPLACE_RE "SimpleTypeRule<RString, AString, ARegExp, AString>" -typerule STRING_REPLACE_RE_ALL "SimpleTypeRule<RString, AString, ARegExp, AString>" operator STRING_PREFIX 2 "string prefixof" operator STRING_SUFFIX 2 "string suffixof" operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit" @@ -152,8 +151,11 @@ typerule STRING_UPDATE ::cvc5::theory::strings::StringUpdateTypeRule typerule STRING_CHARAT ::cvc5::theory::strings::StringAtTypeRule typerule STRING_STRCTN ::cvc5::theory::strings::StringRelationTypeRule typerule STRING_STRIDOF ::cvc5::theory::strings::StringIndexOfTypeRule +typerule STRING_INDEXOF_RE "SimpleTypeRule<RInteger, AString, ARegExp, AInteger>" typerule STRING_STRREPL ::cvc5::theory::strings::StringReplaceTypeRule typerule STRING_STRREPLALL ::cvc5::theory::strings::StringReplaceTypeRule +typerule STRING_REPLACE_RE "SimpleTypeRule<RString, AString, ARegExp, AString>" +typerule STRING_REPLACE_RE_ALL "SimpleTypeRule<RString, AString, ARegExp, AString>" typerule STRING_PREFIX ::cvc5::theory::strings::StringStrToBoolTypeRule typerule STRING_SUFFIX ::cvc5::theory::strings::StringStrToBoolTypeRule typerule STRING_REV ::cvc5::theory::strings::StringStrToStrTypeRule |