projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c16b7a2) | patch
Support `try` and `all` reconstruction modes. (#8098)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 15 Feb 2022 18:14:13 +0000 (12:14 -0600)
committerGitHub <noreply@github.com>
Tue, 15 Feb 2022 18:14:13 +0000 (12:14 -0600)
commitfb7cc27d4ae39d224c739c912ccd76563f374999
treec529567a4ec15faefd7a3d64b579acad32419e41tree
parentc16b7a2ba98296a82ccf84e015a7e07f8487908dcommit | diff
Support `try` and `all` reconstruction modes. (#8098)

This PR adds a simple procedure to quickly reconstruct Sygus terms that are already in the grammar. This new procedure fails if the terms are not in the grammar.
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_reconstruct.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/max-all.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/max-limit.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/max-try1.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/max-try2.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/simple-rewrite-not-in-db.sy diff | blob | history