projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0d4d9bf) | patch
Fixes for SyGuS + regular expressions (#3313)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Oct 2019 23:15:28 +0000 (18:15 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 23 Oct 2019 23:15:28 +0000 (16:15 -0700)
commit64cef995a521ac7211b9e3ed95c85deb186ff352
tree927d14ff521127f37192afcfe8b737f15d54e061tree
parent0d4d9bf3f31687d9cf48b0c45ab420b06ff099f7commit | diff
Fixes for SyGuS + regular expressions (#3313)

This commit fixes numerous issues involving the combination of SyGuS and regular expressions.

Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
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_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/re-concat.sy [new file with mode: 0644] blob