projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd91768) | patch
Add additional ground terms to SyGuS instantiation grammar (#5167)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 1 Oct 2020 20:48:37 +0000 (13:48 -0700)
committerGitHub <noreply@github.com>
Thu, 1 Oct 2020 20:48:37 +0000 (13:48 -0700)
commit776ee02237b06eb3130e56af4d98d9ff36667d8b
tree56d55c26003f2dfa3ef23c0cf4ae32e7af2e5e11tree
parentcd91768f52349bd14399e49b2fbc4e59bb659dedcommit | diff
Add additional ground terms to SyGuS instantiation grammar (#5167)

This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/sygus_inst.cpp diff | blob | history
src/theory/quantifiers/sygus_inst.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history