projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35d080b) | patch
(proof-new) Fixes and improvements for smt proof postprocessor (#5197)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 8 Oct 2020 22:10:36 +0000 (17:10 -0500)
committerGitHub <noreply@github.com>
Thu, 8 Oct 2020 22:10:36 +0000 (17:10 -0500)
commit2edc04bdfdac32ce899c98c4a8887c037b1f6a3f
tree26eb2e286d6738a7e18a61bb1edf3a9316dfa0e9tree
parent35d080bfb56ff96fd41b31ce7025c019193f6abccommit | diff
(proof-new) Fixes and improvements for smt proof postprocessor (#5197)

This includes several subtle issues encountered in the past month based on our regressions.

It also improves the expansion forms of MACRO_ rules to use EQ_RESOLVE instead of a TRUE_INTRO/TRUE_ELIM scheme. This is both more compact and avoids cyclic proofs for some corner cases of proofs with Boolean constant equalites.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/smt/proof_post_processor.cpp diff | blob | history
src/smt/proof_post_processor.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history