projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 16b5470) | patch
Limit cases of sygus inference based on type (#3370)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 Oct 2019 23:06:16 +0000 (18:06 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 8 Oct 2019 23:06:16 +0000 (16:06 -0700)
commit1b6784fe52f4fb745262842e0406d6dd34053cb2
tree6c64a7485612f8af60631fde4dd827222d17215dtree
parent16b54708ff83a1bf6393203b79da6dc059fd2025commit | diff
Limit cases of sygus inference based on type (#3370)

This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.

It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.

Fixes #3250 and fixes #3356.
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/issue3356-syg-inf-usort.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue3250-syg-inf-q.smt2 [new file with mode: 0644] blob