projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2de8778) | patch
(proof-new) Fix true explanations of propagations in pf equality engine (#5338)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Nov 2020 16:00:36 +0000 (10:00 -0600)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 16:00:36 +0000 (10:00 -0600)
commitb9eee8d69e9de4641514c35d49c495bd5adead5f
tree493aff91499c84e1b3543f34c679b2c6f1aa2d17tree
parent2de877854e590e8edf89ffb1d940cd4c9717f195commit | diff
(proof-new) Fix true explanations of propagations in pf equality engine (#5338)

This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
src/expr/proof_node_manager.cpp diff | blob | history
src/expr/proof_node_manager.h diff | blob | history
src/theory/uf/proof_equality_engine.cpp diff | blob | history