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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 29 Jul 2021 16:11:05 +0000 (11:11 -0500)
committer	GitHub <noreply@github.com>
	Thu, 29 Jul 2021 16:11:05 +0000 (16:11 +0000)
commit	b685ed411b6814f0810ce8f61d07aa49bd75ea3b
tree	75029fdd0b7b8d82f6296047c10818cb745c9cdb	tree
parent	f2672e53fae29abe40fc69b004d1df5be0ce1e8b	commit \| diff

Integrate central equality engine approach into theory engine, add option and regressions (#6943)

This commit makes TheoryEngine take into account whether theories are using the central equality engine.

With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.

18 files changed:

src/options/theory_options.toml		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/combination_engine.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/aufbv/cee-small-shared-eq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/sets-deq-dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/cee-bug0909-dd-scope.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/cee-prs-small-dd2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/cee-prs-small.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/cee-npnt-dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/cee-os-delta.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cee-norn-aes-trivially.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/exp-trivially-dd3.smt2	[new file with mode: 0644]	blob

RSS Atom