diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-20 23:32:31 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-20 16:32:31 -0500 |
| commit | 00583622160a91cc2aedc58d00a690bd57306bdc (patch) | |
| tree | 3ff926d51cef593f41630b555858a427c862ea8e /src/theory/uf | |
| parent | f74a8224d363aa8ae4bdc1324ee56306910b5532 (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.
Diffstat (limited to 'src/theory/uf')
0 files changed, 0 insertions, 0 deletions