projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af18cd2) | patch
Split sygus template inference to its own file (#5388)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 Nov 2020 05:06:13 +0000 (23:06 -0600)
committerGitHub <noreply@github.com>
Fri, 6 Nov 2020 05:06:13 +0000 (23:06 -0600)
commit04dc5b60462dc367fe1b99254c215957006f7b21
treee13c0360026bb3c6d19d5f61e0034345c98306e9tree
parentaf18cd275f340d1896c3b635dbeecbea2e521db1commit | diff
Split sygus template inference to its own file (#5388)

This splits techniques for inferring templates for functions-to-synthesize to their own file.

This is work towards cleaning up the single invocation utility, which will be undergoing some additions.
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.h diff | blob | history
src/theory/quantifiers/sygus/template_infer.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/template_infer.h [new file with mode: 0644] blob