projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b115aec) | patch
Fixes for regular expressions + sygus (#5044)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Sep 2020 19:12:52 +0000 (14:12 -0500)
committerGitHub <noreply@github.com>
Wed, 9 Sep 2020 19:12:52 +0000 (14:12 -0500)
commit060eedcd5fdb0316d323c4528402034629285b97
treeee7a93f408a7b18113e1b29b081afab9639e11fetree
parentb115aecf296b8d712363c506daecfab364f71712commit | diff
Fixes for regular expressions + sygus (#5044)

Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/rex-strings-alarm.sy [new file with mode: 0644] blob