projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a3670b5) | patch
Fix abduction with datatypes (#4566)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Jun 2020 16:31:55 +0000 (11:31 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Jun 2020 16:31:55 +0000 (11:31 -0500)
commit8c467723be3746ed711c609fa6dafb19a5a49e8b
treebd68e5503cef07eb76a3f4c2aee52abb044ceda3tree
parenta3670b55e0ef3d4c8e31800aa943688065ca029ccommit | diff
Fix abduction with datatypes (#4566)

Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
src/theory/quantifiers/sygus/sygus_abduct.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/abduct-dt.smt2 [new file with mode: 0644] blob