projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f77646) | patch
[proof-new] Adds a proof manager for the SAT solver (#5140)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Mon, 28 Sep 2020 20:38:59 +0000 (17:38 -0300)
committerGitHub <noreply@github.com>
Mon, 28 Sep 2020 20:38:59 +0000 (17:38 -0300)
commitd4564e7ef8eb277fcfc42c3130a3180165594b58
tree849dc6284bcf3879899aca6964da5a5e415faae9tree
parent0f77646dfc0944f1f17f121ffb3112bf8b244f76commit | diff
[proof-new] Adds a proof manager for the SAT solver (#5140)

Tracks the refutation proof built by Minisat. See the header for extensive explanations.

This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).
src/CMakeLists.txt diff | blob | history
src/expr/lazy_proof_chain.cpp diff | blob | history
src/expr/lazy_proof_chain.h diff | blob | history
src/prop/minisat/core/Solver.h diff | blob | history
src/prop/sat_proof_manager.cpp [new file with mode: 0644] blob
src/prop/sat_proof_manager.h [new file with mode: 0644] blob
src/prop/theory_proxy.cpp diff | blob | history
src/prop/theory_proxy.h diff | blob | history