projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 46501b0) | patch
(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 22 May 2020 19:27:13 +0000 (14:27 -0500)
committerGitHub <noreply@github.com>
Fri, 22 May 2020 19:27:13 +0000 (14:27 -0500)
commit0b49b88e4d1c299a7cd662cd2221fd826b5bc972
treee2405e359c0d6bd6b20542915b43a16dba198b62tree
parent46501b092b2d9419273d42f28a7a543ae9b2e338commit | diff
(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)

This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).

This allows us to justify the regular expression inclusion inference as a rewrite.
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/re-in-rewrite.smt2 [new file with mode: 0644] blob