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/parser/smt2/smt2.cpp | 1 + 1 file changed, 1 insertion(+) (limited to 'src/parser') diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 88f4b4ef8..d32f149bf 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addStringOperators() { addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); if (!strictModeEnabled()) { + addOperator(api::STRING_INDEXOF_RE, "str.indexof_re"); addOperator(api::STRING_UPDATE, "str.update"); addOperator(api::STRING_TOLOWER, "str.tolower"); addOperator(api::STRING_TOUPPER, "str.toupper"); -- cgit v1.2.3