projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c789e85) | patch
[proof-new] Adds a proof post processor for the Prop Engine (#5161)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 29 Sep 2020 13:57:37 +0000 (10:57 -0300)
committerGitHub <noreply@github.com>
Tue, 29 Sep 2020 13:57:37 +0000 (10:57 -0300)
commit1c9290c99daa69b549d49dc762cadd8307211bc8
treefc430b9e08512872bfd68ef2d654cf6c660c662ftree
parentc789e8510ffa430f398bdc9eee2101e80c7c27decommit | diff
[proof-new] Adds a proof post processor for the Prop Engine (#5161)

The post processor connects the two proofs in the prop engine: the refutation proof in the SAT solver and the CNF transformation proof in the CNF stream. The proof generators from theory engine in the latter are also expanded during the connection.
src/CMakeLists.txt diff | blob | history
src/prop/proof_post_processor.cpp [new file with mode: 0644] blob
src/prop/proof_post_processor.h [new file with mode: 0644] blob