projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a681764) | patch
(proof-new) proofs in ee -> arith pipeline (#5215)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 7 Oct 2020 18:48:06 +0000 (11:48 -0700)
committerGitHub <noreply@github.com>
Wed, 7 Oct 2020 18:48:06 +0000 (13:48 -0500)
commit5d51949548af6df9a18f498de2d424f15988a07b
treed66dd6802be239ddd3246417f0c76f686fa83991tree
parenta6817647ee9bae0df0f1922c0d521d7f100d0245commit | diff
(proof-new) proofs in ee -> arith pipeline (#5215)

Threads proofs through the flow of information from the equality engine
into the theory of arithmetic.

Pretty straightforward. You just have to bundle up information from the EE.
src/theory/arith/callbacks.cpp diff | blob | history
src/theory/arith/callbacks.h diff | blob | history
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history