projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 16c7729) | patch
(proof-new) New proofs in arith::Constraint::externalExplain (#5176)
authorAlex Ozdemir <aozdemir@hmc.edu>
Fri, 2 Oct 2020 13:03:23 +0000 (06:03 -0700)
committerGitHub <noreply@github.com>
Fri, 2 Oct 2020 13:03:23 +0000 (08:03 -0500)
commitd3fcaabbafdfebe17aa20f656ff2d3922d0dcb96
treeb34b7e6a4130f7b879db543973da0b1cf1c718f8tree
parent16c772966206835c7f380e3a926e51af75ec3584commit | diff
(proof-new) New proofs in arith::Constraint::externalExplain (#5176)

This commit threads proofs through the core of arith:
Constraint::externalExplain, which recursively explain arith literals.
One of the base cases here is asking the EE for an explanation, through
the congruence manager. To delay implementing proofs in
ArithCongruenceManager to a separate commit, we stub out proof
production in ArithCongruenceManager::explain for now.
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/constraint.cpp diff | blob | history
src/theory/arith/constraint.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history