projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6923f0c) | patch
[proof-new] Optimizing sat proof (#6324)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 9 Apr 2021 20:30:44 +0000 (17:30 -0300)
committerGitHub <noreply@github.com>
Fri, 9 Apr 2021 20:30:44 +0000 (15:30 -0500)
commit62f5fb8db269e12f13ce5c4e1c3f975776737836
treebdf16437b8c0c5ead202ac7fb08f6483aa3a9c19tree
parent6923f0cb9930332a61e187d3b4d1a7ec7e65b15ccommit | diff
[proof-new] Optimizing sat proof (#6324)

For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
src/expr/lazy_proof_chain.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/prop/sat_proof_manager.cpp diff | blob | history
src/prop/sat_proof_manager.h diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/smt/proof_post_processor.cpp diff | blob | history
src/theory/booleans/proof_checker.cpp diff | blob | history