diff options
Diffstat (limited to 'src/prop/sat_proof_manager.h')
| -rw-r--r-- | src/prop/sat_proof_manager.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 0555e7ba7..e05923268 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -21,10 +21,7 @@ #include "expr/buffered_proof_generator.h" #include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" #include "prop/minisat/core/SolverTypes.h" -#include "prop/cnf_stream.h" #include "prop/sat_solver_types.h" namespace Minisat { @@ -32,8 +29,13 @@ class Solver; } namespace CVC4 { + +class ProofNodeManager; + namespace prop { +class CnfStream; + /** * This class is responsible for managing the proof production of the SAT * solver. It tracks resolutions produced during solving and stores them, |