git.libre-soc.org Git - cvc5.git/commit

author	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 26 Feb 2015 14:16:15 +0000 (15:16 +0100)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 26 Feb 2015 14:16:23 +0000 (15:16 +0100)
commit	4f5c9dbbd0125294500cf5788cb131b355979fb6
tree	fd07a862b4ad35111d56bdfa84f17f8c44d45e6c	tree
parent	92e4099d9d2b313a521d2a015e604645e24617f4	commit \| diff

Robust strategy for single invocation LIA synthesis conjectures. Add regressions.

13 files changed:

src/theory/quantifiers/ce_guided_instantiation.cpp		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/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
test/regress/regress0/sygus/Makefile.am		diff \| blob \| history
test/regress/regress0/sygus/array_search_2.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/array_sum_2_5.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/max.sl	[deleted file]	blob \| history
test/regress/regress0/sygus/max.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/parity-AIG-d0.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/twolets1.sy	[new file with mode: 0644]	blob