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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 9 Oct 2018 21:54:58 +0000 (16:54 -0500)
committer	GitHub <noreply@github.com>
	Tue, 9 Oct 2018 21:54:58 +0000 (16:54 -0500)
commit	9168f325706e61bb12fec71cd375647e2102f8d3
tree	aa5129a48322e43ae0f5faa9ade2decbd7091df0	tree
parent	90ffa8b4eb26af9060e57be7fe5d6008717d3ce6	commit \| diff

Support for basic actively-generated enumerators (#2606)

20 files changed:

src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/quantifiers_modes.h		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		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.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.h		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/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.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/regress1/sygus/trivial-stream.sy		diff \| blob \| history