projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b2137af) | patch
[proof-new] Adds a proof-producing CNF converter (#5137)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 29 Sep 2020 12:35:46 +0000 (09:35 -0300)
committerGitHub <noreply@github.com>
Tue, 29 Sep 2020 12:35:46 +0000 (09:35 -0300)
commitd11d694f73ec0520cb251304f9508b3355b93725
treeba915dbb35bbbd86cb82d017e265f632e12c5d51tree
parentb2137af7e9dd3993b4206274c59d0e3eeb2725cccommit | diff
[proof-new] Adds a proof-producing CNF converter (#5137)

A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).
src/CMakeLists.txt diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/proof_cnf_stream.cpp [new file with mode: 0644] blob
src/prop/proof_cnf_stream.h [new file with mode: 0644] blob