projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 31983bd) | patch
(proof-new) Make circuit propagator proof producing (#5318)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 21 Oct 2020 23:19:24 +0000 (01:19 +0200)
committerGitHub <noreply@github.com>
Wed, 21 Oct 2020 23:19:24 +0000 (18:19 -0500)
commita99f5aaa46702a4894aaddeed3a7ff5cbf69bdfd
tree7d0e6bc5d9eabfc5e6db6c6e84535b31bc58a964tree
parent31983bd41f8c6ec736e374946de355fd1a9bc6f1commit | diff
(proof-new) Make circuit propagator proof producing (#5318)

This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator.
src/preprocessing/passes/non_clausal_simp.cpp diff | blob | history
src/theory/booleans/circuit_propagator.cpp diff | blob | history
src/theory/booleans/circuit_propagator.h diff | blob | history