projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad87bbc) | patch
Add rewrite for str.replace_re. (#4601)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 12 Jun 2020 02:25:07 +0000 (21:25 -0500)
committerGitHub <noreply@github.com>
Fri, 12 Jun 2020 02:25:07 +0000 (21:25 -0500)
commit4d547e52d3f2b54a0af7270d2b653d2cb24edb57
tree3e73d2c1adbe9798bbcc316831d34821adac54d8tree
parentad87bbc615944514fcfcb3689768aab60a9cc9d6commit | diff
Add rewrite for str.replace_re. (#4601)

This was discovered due to a proof checking abnormality, where the checker surprisingly succeeded in proving that the reduced form for a str.replace_re was equivalent for 2 different sets of skolems after rewriting.
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history