projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a3605a3) | patch
Initial support for parametric datatypes in sygus (#6304)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 8 Apr 2021 01:40:42 +0000 (20:40 -0500)
committerGitHub <noreply@github.com>
Thu, 8 Apr 2021 01:40:42 +0000 (01:40 +0000)
commit89384c9a4aad291ce5ca26917507e4fd47c6ec4f
tree5b963e9c863686dd452322a672a6deb46cec1bfatree
parenta3605a32a3968c141d50e95477584185616bdbbdcommit | diff
Initial support for parametric datatypes in sygus (#6304)

Fixes #6298.

Enables parsing of par in the sygus parser, and adds support for default grammar construction.

Also fixes a bug related to single invocation for non-function types.
src/expr/dtype_cons.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/theory/quantifiers/single_inv_partition.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/issue6298-par.sy [new file with mode: 0644] blob