projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8699e3e) | patch
Add rewrite for allchar beneath union + star (#8299)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 14 Mar 2022 18:02:09 +0000 (13:02 -0500)
committerGitHub <noreply@github.com>
Mon, 14 Mar 2022 18:02:09 +0000 (18:02 +0000)
commit434596534ef68bcc7c7162f16687f8827c8d8c50
tree83b9f54bb12274a171aa4dfbf579c4ebf108a97btree
parent8699e3e95075e262852b57ea9a298648d5caa26ccommit | diff
Add rewrite for allchar beneath union + star (#8299)

Addresses the issue on #8295.

The re elimination module was assuming that a trivial RE was rewritten when it was not.
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
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue8295-star-union-char.smt2 [new file with mode: 0644] blob