projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75ccf2b) | patch
Sygus inv templ refactor (#1110)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 21 Sep 2017 08:20:09 +0000 (03:20 -0500)
committerGitHub <noreply@github.com>
Thu, 21 Sep 2017 08:20:09 +0000 (03:20 -0500)
commit69d511da599dc18fbf3d42571e0f23b8e1d39032
treeb44d1007c3b0a82565494bc112b61ba245a9e001tree
parent75ccf2b4ad3dbcb1a0edfc336db35b45719a09f5commit | diff
Sygus inv templ refactor (#1110)

* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.

* Update comment on class

* Cleanup

* Comments for sygus type construction.
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/term_database_sygus.h diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/cegar1.sy [new file with mode: 0644] blob