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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 29f5a57d4..4d96fa0b3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -444,6 +444,8 @@ libcvc4_add_sources( theory/bags/theory_bags_type_rules.h theory/booleans/circuit_propagator.cpp theory/booleans/circuit_propagator.h + theory/booleans/proof_circuit_propagator.cpp + theory/booleans/proof_circuit_propagator.h theory/booleans/proof_checker.cpp theory/booleans/proof_checker.h theory/booleans/theory_bool.cpp |