projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85121a0) | patch
Throw exception for non-well-founded unimplemented SyGuS types. (#4125)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Mar 2020 18:30:48 +0000 (13:30 -0500)
committerGitHub <noreply@github.com>
Mon, 23 Mar 2020 18:30:48 +0000 (13:30 -0500)
commitdd515b59583cba1afed8fbb583f8012a214feaad
treee808f4ac62becd2b725c1e870f1020f7b7de4dd8tree
parent85121a067789d9c6ac7ff14c3e34a2bc5aa83d24commit | diff
Throw exception for non-well-founded unimplemented SyGuS types. (#4125)

Fixes #3931.

Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype.
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history