projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f74a822) | patch
(proof-new) Add proofs for circuit propagator (#5301)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 20 Oct 2020 21:32:31 +0000 (23:32 +0200)
committerGitHub <noreply@github.com>
Tue, 20 Oct 2020 21:32:31 +0000 (16:32 -0500)
commit00583622160a91cc2aedc58d00a690bd57306bdc
tree3ff926d51cef593f41630b555858a427c862ea8etree
parentf74a8224d363aa8ae4bdc1324ee56306910b5532commit | diff
(proof-new) Add proofs for circuit propagator (#5301)

This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator.
It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required.
A second PR will use these rules within the circuit propagator class.
src/CMakeLists.txt diff | blob | history
src/theory/booleans/proof_circuit_propagator.cpp [new file with mode: 0644] blob
src/theory/booleans/proof_circuit_propagator.h [new file with mode: 0644] blob