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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 10 May 2018 21:48:51 +0000 (16:48 -0500)
committer	GitHub <noreply@github.com>
	Thu, 10 May 2018 21:48:51 +0000 (16:48 -0500)
commit	adcbee78823120baa47eb8ba868b614512a121a9
tree	f019c19fa63cc06c8b4e93df2cbde7d61791368b	tree
parent	f29ced85757a85b6bd72b741d6ac7ff45ba29619	commit \| diff

Sygus repair constants (#1812)

16 files changed:

src/Makefile.am		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_conjecture.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_repair_const.h	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.h		diff \| blob \| history
test/regress/Makefile.tests		diff \| blob \| history
test/regress/regress1/sygus/constant-ite-bv.sy	[new file with mode: 0644]	blob