projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 40807e2) | patch
Use default consts when not using any const during grammar normalization (#3807)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Feb 2020 17:47:05 +0000 (11:47 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Feb 2020 17:47:05 +0000 (11:47 -0600)
commit2a274c84867a2974abc0b626349b934d520339b0
treeba38f050cc21927407ec45bd9b14e8d9ab97b0ectree
parent40807e2f5f3b9d07e66dc2d2a7dde4c8aac98720commit | diff
Use default consts when not using any const during grammar normalization (#3807)

Fixes #3802.

If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/issue3802-default-consts.sy [new file with mode: 0644] blob