projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e680a29) | patch
Improve defaults for sygus default grammars (#7553)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Nov 2021 21:01:41 +0000 (16:01 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 21:01:41 +0000 (21:01 +0000)
commitbe6f9c2ee9201cc5181ce7ba27b6fe992ab3fff6
tree83e22969a075e584c0b922db1808fb24a4672484tree
parente680a299ac1da58b8fee27e3733d5e5eea255d94commit | diff
Improve defaults for sygus default grammars (#7553)

We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/abduction/abd-real-const.smt2 [new file with mode: 0644] blob