projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85a8dfd) | patch
Fixes for degenerate case of sygus decision tree learning (#4800)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Aug 2020 22:13:14 +0000 (17:13 -0500)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 22:13:14 +0000 (17:13 -0500)
commit103b5ea715e532e021e91f9b03ea7d7876a3ccbf
treebe6dbe34884cf96e4d22bfefd8071e3afb11e841tree
parent85a8dfddd887a041f397d1ff2c3a6c34900c5775commit | diff
Fixes for degenerate case of sygus decision tree learning (#4800)

Fixes #4790.

Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.
src/theory/quantifiers/sygus/sygus_unif_io.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/issue4790-dtd.sy [new file with mode: 0644] blob