projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b68e063) | patch
Fix handling of start index in `str.indexof_re` (#6674)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 4 Jun 2021 00:41:40 +0000 (17:41 -0700)
committerGitHub <noreply@github.com>
Fri, 4 Jun 2021 00:41:40 +0000 (00:41 +0000)
commitadf497af7a3fc8b06b875eaf9feca2568d0ba9d8
treef544a1e6207bf76e998e1ba17bee44f5d46b87dbtree
parentb68e0636fb839142f1515fc8551ade09d3ed1a5dcommit | diff
Fix handling of start index in `str.indexof_re` (#6674)

Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/indexof_re-start-index.smt2 [new file with mode: 0644] blob
test/regress/regress2/strings/issue6636-replace-re-all.smt2 [new file with mode: 0644] blob
test/regress/regress2/strings/issue6637-replace-re-all.smt2 [new file with mode: 0644] blob