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/api/cpp | |
| 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/api/cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 2 | ||||
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 16 |
2 files changed, 18 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 16366c3cf..0f2d5ad1b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -312,6 +312,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {STRING_CHARAT, cvc5::Kind::STRING_CHARAT}, {STRING_CONTAINS, cvc5::Kind::STRING_STRCTN}, {STRING_INDEXOF, cvc5::Kind::STRING_STRIDOF}, + {STRING_INDEXOF_RE, cvc5::Kind::STRING_INDEXOF_RE}, {STRING_REPLACE, cvc5::Kind::STRING_STRREPL}, {STRING_REPLACE_ALL, cvc5::Kind::STRING_STRREPLALL}, {STRING_REPLACE_RE, cvc5::Kind::STRING_REPLACE_RE}, @@ -618,6 +619,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::STRING_CHARAT, STRING_CHARAT}, {cvc5::Kind::STRING_STRCTN, STRING_CONTAINS}, {cvc5::Kind::STRING_STRIDOF, STRING_INDEXOF}, + {cvc5::Kind::STRING_INDEXOF_RE, STRING_INDEXOF_RE}, {cvc5::Kind::STRING_STRREPL, STRING_REPLACE}, {cvc5::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL}, {cvc5::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 6f6bf1d0e..4263eedb2 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2631,6 +2631,22 @@ enum CVC5_EXPORT Kind : int32_t */ STRING_INDEXOF, /** + * String index-of regular expression match. + * Returns the first match of a regular expression r in a string s. If the + * index is negative or greater than the length of string s1, or r does not + * match a substring in s after index i, the result is -1. + * + * Parameters: + * - 1: Term of sort String (string s) + * - 2: Term of sort RegLan (regular expression r) + * - 3: Term of sort Integer (index i) + * + * Create with: + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` + */ + STRING_INDEXOF_RE, + /** * String replace. * Replaces a string s2 in a string s1 with string s3. If s2 does not appear * in s1, s1 is returned unmodified. |