projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 60ed666) | patch
Do RE derivation inference only for concrete constant RE (#4609)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 15 Jun 2020 14:40:34 +0000 (09:40 -0500)
committerGitHub <noreply@github.com>
Mon, 15 Jun 2020 14:40:34 +0000 (07:40 -0700)
commit5de97c3efe8794bf7e39774686dca81a1982a8ed
tree092aca5e779a1a719e88a78ff4755df88210cad9tree
parent60ed666d657bfcd69f48821c78a34696796df5fbcommit | diff
 Do RE derivation inference only for concrete constant RE (#4609)

The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.
src/theory/strings/regexp_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue4608-re-derive.smt2 [new file with mode: 0644] blob