projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c940080) | patch
Fix single invocation partition for higher-order (#7046)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Aug 2021 20:45:38 +0000 (15:45 -0500)
committerGitHub <noreply@github.com>
Mon, 23 Aug 2021 20:45:38 +0000 (20:45 +0000)
commitb272d60452028025d56dbf6ffe10276d6f9281cb
treee93bc1cafe5fdd50c110e84e629dcaa58a233228tree
parentc94008073d2b9ddec19ca9713d0c30eb41777eb6commit | diff
Fix single invocation partition for higher-order (#7046)

It was not robust to cases where a function-to-synthesize occurred in a higher-order context.

Also does general clean up of the single invocation utility.
src/expr/subs.cpp diff | blob | history
src/expr/subs.h diff | blob | history
src/theory/quantifiers/single_inv_partition.cpp diff | blob | history
src/theory/quantifiers/single_inv_partition.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/ho-occ-synth-fun.sy [new file with mode: 0644] blob