projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e2a64ae) | patch
[proof-new] Adds Lazy CDProof chain data-structure (#5060)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 16 Sep 2020 16:25:33 +0000 (13:25 -0300)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 16:25:33 +0000 (11:25 -0500)
commit5557985d7320668b2625f1559f907488e2a85590
treea4ffd4059344cd49e595e6d5cbc03b8445b22ee9tree
parente2a64ae3e03ade771363df90dfa3f50b87a9205acommit | diff
[proof-new] Adds Lazy CDProof chain data-structure (#5060)

A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
src/expr/CMakeLists.txt diff | blob | history
src/expr/lazy_proof_chain.cpp [new file with mode: 0644] blob
src/expr/lazy_proof_chain.h [new file with mode: 0644] blob
src/expr/proof_node_algorithm.cpp diff | blob | history
src/expr/proof_node_algorithm.h diff | blob | history
src/expr/proof_node_manager.cpp diff | blob | history