projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d8d3c55) | patch
(proof-new) Refactor regular expression operation (#4596)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 6 Aug 2020 11:48:45 +0000 (06:48 -0500)
committerGitHub <noreply@github.com>
Thu, 6 Aug 2020 11:48:45 +0000 (06:48 -0500)
commit77e98815254c68301ffcd7fb8addeb6751c51187
tree068ad98b6b43692276972a1ee5111ced3178338ctree
parentd8d3c55afc94482fc05f68ba6be47f767ab3b5c6commit | diff
(proof-new) Refactor regular expression operation (#4596)

This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.

Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.
src/theory/strings/regexp_operation.cpp diff | blob | history
src/theory/strings/regexp_operation.h diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
src/theory/strings/regexp_solver.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
test/unit/theory/regexp_operation_black.h diff | blob | history