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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 28 Jul 2020 16:03:33 +0000 (11:03 -0500)
committer	GitHub <noreply@github.com>
	Tue, 28 Jul 2020 16:03:33 +0000 (11:03 -0500)
commit	c38f35164adc5ab255803765a568ef820fa8f3b2
tree	6cbd4b21e8e9ff364b5b2f14467cd986ea69acf2	tree
parent	b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42	commit \| diff

Use lemma property enum for OutputChannel::lemma (#4755)

There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.

This makes them into a enum.

24 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/proof/proof_output_channel.cpp		diff \| blob \| history
src/proof/proof_output_channel.h		diff \| blob \| history
src/theory/arith/nl/nl_lemma_utils.cpp		diff \| blob \| history
src/theory/arith/nl/nl_lemma_utils.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/engine_output_channel.cpp		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/ext_theory.cpp		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/output_channel.cpp	[new file with mode: 0644]	blob
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/sets/inference_manager.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history

RSS Atom