From 29f0b8f378377ed836bddaaf88883d0b2eeb545d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 27 May 2021 15:42:10 -0700 Subject: 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. --- src/theory/strings/kinds | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/theory/strings/kinds') 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" -typerule STRING_REPLACE_RE_ALL "SimpleTypeRule" 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" typerule STRING_STRREPL ::cvc5::theory::strings::StringReplaceTypeRule typerule STRING_STRREPLALL ::cvc5::theory::strings::StringReplaceTypeRule +typerule STRING_REPLACE_RE "SimpleTypeRule" +typerule STRING_REPLACE_RE_ALL "SimpleTypeRule" typerule STRING_PREFIX ::cvc5::theory::strings::StringStrToBoolTypeRule typerule STRING_SUFFIX ::cvc5::theory::strings::StringStrToBoolTypeRule typerule STRING_REV ::cvc5::theory::strings::StringStrToStrTypeRule -- cgit v1.2.3