Clean up includes to reduce compile times (#6031)

This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.

18 files changed, 21 insertions, 21 deletions

diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index f6753a601..266cfb18a 100644
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -15,6 +15,7 @@
 #include "expr/buffered_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index f774e383d..da80891a2 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 #define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "context/cdhashmap.h"
-#include "context/cdhashset.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * The proof generator for buffered steps. This class is a context-dependent
  * mapping from formulas to proof steps. It does not generate ProofNodes until it
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 694d75db6..23d6b3ca1 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -15,6 +15,7 @@
 
 #include <sstream>
 #include <string>
+#include "util/hash.h"
 #include "util/integer.h"
 
 using namespace std;
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index c7f170ff6..08640e1d5 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -18,7 +18,6 @@
 #define CVC4__DATATYPE_INDEX_H
 
 #include <iosfwd>
-#include "util/hash.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5cb76858a..f94f0063a 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -13,6 +13,7 @@
  **/
 #include "expr/dtype.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"
 
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index e4bae29b8..c68a7d44a 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -20,10 +20,8 @@
 #include <map>
 #include <string>
 #include <vector>
-#include "expr/dtype_cons.h"
-#include "expr/dtype_selector.h"
+#include "expr/attribute.h"
 #include "expr/node.h"
-#include "expr/node_manager_attributes.h"
 #include "expr/type_node.h"
 
 namespace CVC4 {
@@ -76,7 +74,7 @@ struct DTypeUFiniteComputedTag
 typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
-class NodeManager;
+class DTypeConstructor;
 
 /**
  * The Node-level representation of an inductive datatype, which currently
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 0c209f393..8d8d2741f 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -15,6 +15,7 @@
 #include "expr/lazy_proof.h"
 
 #include "expr/proof_ensure_closed.h"
+#include "expr/proof_node_manager.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index e2bba3015..83dc90e4d 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -22,10 +22,11 @@
 
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy proof. This class is an extension of CDProof
  * that additionally maps facts to proof generators in a context-dependent
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 2edad1647..f80ab099c 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -17,6 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/proof_options.h"
 
 namespace CVC4 {
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 59cab72c9..1604bf182 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -22,10 +22,11 @@
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy generator for proof chains. This class is an
  * extension of ProofGenerator that additionally that maps facts to proof
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index c45295622..1aca73d2e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -21,6 +21,7 @@
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/attribute.h"
+#include "expr/type_checker.h"
 
 using namespace std;
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 559ce5ddb..06c327018 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,8 +22,6 @@
 #ifndef CVC4__NODE_H
 #define CVC4__NODE_H
 
-#include <algorithm>
-#include <functional>
 #include <iostream>
 #include <string>
 #include <unordered_map>
@@ -32,14 +30,12 @@
 #include <vector>
 
 #include "base/check.h"
-#include "base/configuration.h"
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/type.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/hash.h"
@@ -980,7 +976,6 @@ std::ostream& operator<<(
 
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
-#include "expr/type_checker.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 883febd6f..4404e3445 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -26,6 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index 75a11eac7..0b778ebef 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -14,6 +14,8 @@
 
 #include "node_traversal.h"
 
+#include <functional>
+
 namespace CVC4 {
 
 NodeDfsIterator::NodeDfsIterator(TNode n,
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index e7e49db45..124372f79 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__EXPR__NODE_TRAVERSAL_H
 #define CVC4__EXPR__NODE_TRAVERSAL_H
 
-#include <functional>
 #include <iterator>
 #include <unordered_map>
 #include <vector>
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 0635e983b..1ad498ecd 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -399,7 +399,6 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 }/* CVC4 namespace */
 
 #include "expr/node_manager.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
@@ -501,7 +500,6 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }/* CVC4 namespace */
 
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 1c21a59e7..b512b5869 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof.h"
 
+#include "expr/proof_node_manager.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 8350b4954..3a26f0975 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -24,11 +24,12 @@
 #include "expr/node.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) proof.
  *