Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

5 files changed, 17 insertions, 8 deletions

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 1912d1ba6..b50ec34c7 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,8 +21,12 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/theory.h"
+#include "util/hash.h"
 #include "util/utility.h"
 
 using namespace std;
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index a2e4febad..ba8c5782d 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
-#include <functional>
 #include <memory>
 #include <unordered_map>
 #include <vector>
@@ -30,15 +29,17 @@
 #include "context/context.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/theory.h"
 #include "theory/trust_node.h"
-#include "util/hash.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+class ProofNode;
+
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace booleans {
 
 /**
diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h
index b3d7c0f64..1d807fd90 100644
--- a/src/theory/booleans/proof_checker.h
+++ b/src/theory/booleans/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index a7ae4ac18..aaff82933 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -18,6 +18,7 @@
 
 #include <sstream>
 
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
index f9a51e067..fa472b602 100644
--- a/src/theory/booleans/proof_circuit_propagator.h
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -22,9 +22,13 @@
 #include <memory>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace booleans {