summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/indexof-sym-simp.smt2
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-05-24 12:19:33 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2021-05-24 15:57:06 -0700
commitb686cbe705ca127492239dfdf983bc3ce236834c (patch)
tree9861c1da51f1d1535d3307d1778ad376736375da /test/regress/regress0/strings/indexof-sym-simp.smt2
parentcaf47102f2b666aff7c89387067e7531412fd61d (diff)
Fix `str.replace_re` and `str.replace_re_all`
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 'test/regress/regress0/strings/indexof-sym-simp.smt2')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback