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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 14 Jan 2022 23:59:58 +0000 (17:59 -0600)
committer	GitHub <noreply@github.com>
	Fri, 14 Jan 2022 23:59:58 +0000 (23:59 +0000)
commit	e037509aa86cf68691d9ef9eac3cac771fb26d03
tree	a6b0c4d2562e742a15c299e382cd01cbab24a154	tree
parent	9b120a987bc0421d2fd9029ec9b9b7c6a78c3897	commit \| diff

Improve names for sygus enumeration option (#7945)

Also deletes the unused (naive) basic enumerator.

28 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp	[deleted file]	blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_basic.h	[deleted file]	blob \| history
src/theory/quantifiers/sygus/sygus_random_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
test/regress/regress1/sygus/commutative-stream.sy		diff \| blob \| history
test/regress/regress1/sygus/error1-dt.sy		diff \| blob \| history
test/regress/regress1/sygus/fast-enum-backtrack.sy		diff \| blob \| history
test/regress/regress1/sygus/interpol1-push-pop.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol1.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol_arr1.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol_arr2.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol_cosa_1.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol_from_pono_1.smt2		diff \| blob \| history
test/regress/regress1/sygus/interpol_from_pono_2.smt2		diff \| blob \| history
test/regress/regress1/sygus/issue3580.sy		diff \| blob \| history
test/regress/regress1/sygus/rand_const.sy		diff \| blob \| history
test/regress/regress1/sygus/rand_p_0.sy		diff \| blob \| history
test/regress/regress1/sygus/rand_p_1.sy		diff \| blob \| history
test/regress/regress1/sygus/trivial-stream.sy		diff \| blob \| history
test/regress/regress2/sygus/multi-udiv.sy		diff \| blob \| history
test/regress/regress2/sygus/sets-fun-test.sy		diff \| blob \| history
test/regress/regress2/sygus/three.sy		diff \| blob \| history
test/regress/regress3/interpol2.smt2		diff \| blob \| history
test/regress/regress3/strings-any-term.sy		diff \| blob \| history

RSS Atom