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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Wed, 2 Sep 2020 13:48:12 +0000 (15:48 +0200)
committer	GitHub <noreply@github.com>
	Wed, 2 Sep 2020 13:48:12 +0000 (08:48 -0500)
commit	02e682821028bc704c57a762dadeb6f82bb70ebf
tree	4eb20c4d3e6b06eaee58b808909e603da013b554	tree
parent	78917e16f6521b0e8a074f3649fc6adf37614617	commit \| diff

Add ArithLemma and arith::InferenceManager (#4960)

This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory.
Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.

15 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/arith/arith_lemma.cpp	[new file with mode: 0644]	blob
src/theory/arith/arith_lemma.h	[new file with mode: 0644]	blob
src/theory/arith/inference_manager.cpp	[new file with mode: 0644]	blob
src/theory/arith/inference_manager.h	[new file with mode: 0644]	blob
src/theory/arith/nl/cad_solver.cpp		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/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nl_solver.cpp		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/arith/nl/transcendental_solver.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.h		diff \| blob \| history

RSS Atom