projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3403804) | patch
[proof-new] Fix explanation of literals in SAT proof manager (#6346)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 14 Apr 2021 13:31:35 +0000 (10:31 -0300)
committerGitHub <noreply@github.com>
Wed, 14 Apr 2021 13:31:35 +0000 (13:31 +0000)
commitd1eee40cc8788d38ec7431ea8d7429a5573a101c
treef3e994a1b58ce6a3686e73bc9b8e52c2da58175dtree
parent340380462989ff06d08567147bb16d0df9ddb1bccommit | diff
[proof-new] Fix explanation of literals in SAT proof manager (#6346)

Prevents exponential behavior in SAT proof generation by not reexplaining previously explained literals. Also fix a potential issue in not previously overwriting rederived resolution chains during solving.
src/expr/buffered_proof_generator.cpp diff | blob | history
src/expr/buffered_proof_generator.h diff | blob | history
src/prop/sat_proof_manager.cpp diff | blob | history