projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ed1e21d) | patch
Fix case where RE unfolding generates a trivially true lemma (#6267)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 2 Apr 2021 16:43:53 +0000 (11:43 -0500)
committerGitHub <noreply@github.com>
Fri, 2 Apr 2021 16:43:53 +0000 (16:43 +0000)
commitc6c40d12c38fb30d0c4f503353532b93f03e745a
tree366ad9f9af8144e4259a39bbce7379d7bd2ce944tree
parented1e21df4c7364e9d78f1a5c0605c45640d9cccacommit | diff
Fix case where RE unfolding generates a trivially true lemma (#6267)

An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.

An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).

This PR ensures we are robust to these cases.

This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
src/theory/strings/regexp_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 [new file with mode: 0644] blob