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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 23 May 2018 01:27:32 +0000 (20:27 -0500)
committer	GitHub <noreply@github.com>
	Wed, 23 May 2018 01:27:32 +0000 (20:27 -0500)
commit	2ac3d0bf2c00edbbd04033815f10ba0207010f77
tree	7a61979523714dfefa6ba8277b38b0b382706f28	tree
parent	eab7fae2c02ce635500dbe7c743a5c0d7f39137d	commit \| diff

Repair constants using symbolic constructors (#1960)

16 files changed:

src/options/quantifiers_options.toml		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
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/regress0/expect/scrub.07.sy	[deleted file]	blob \| history
test/regress/regress0/expect/scrub.07.sy.expect	[deleted file]	blob \| history
test/regress/regress2/sygus/ex23.sy		diff \| blob \| history