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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 31 Aug 2020 19:24:27 +0000 (14:24 -0500)
committer	GitHub <noreply@github.com>
	Mon, 31 Aug 2020 19:24:27 +0000 (12:24 -0700)
commit	7b3b19f73ceb2168ced48d07a590c0f3be82a8d4
tree	a2ca8f1cae261c87ea659c2d8f36a8090475e88d	tree
parent	57a02fd0c7faa7a87b8619d52cf519e033633c1d	commit \| diff

Simplify interface for computing relevant terms. (#4966)

This is a followup to #4945 which simplifies the contract for computeRelevantTerms.

16 files changed:

src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history