Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

12 files changed, 22 insertions, 16 deletions

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6ad0562ab..5fcb57beb 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/assertions.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/language.h"
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 167caf379..1a8a6e3d0 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,7 +20,6 @@
 #include <memory>
 #include <vector>
 
-#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 84c4acfac..ed19549c9 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -17,16 +17,18 @@
 #ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 #define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 
-#include <map>
-
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
+#include "expr/proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+class ProofNodeManager;
+
 namespace smt {
 
 /**
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index a3c3a5ae2..e5dd7869c 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,6 +15,7 @@
 #include "smt/preprocessor.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 0191d17e5..eadbbedc5 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -30,6 +30,7 @@ class PreprocessingPassContext;
 namespace smt {
 
 class AbstractValues;
+class PreprocessProofGenerator;
 
 /**
  * The preprocessor module of an SMT engine.
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 45cd8284d..9a6486ded 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -14,7 +14,6 @@
 
 #include "smt/process_assertions.h"
 
-#include <stack>
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
@@ -27,8 +26,10 @@
 #include "options/strings_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
+#include "smt/assertions.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index b05779780..f1c0aed3b 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -21,18 +21,21 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/type_node.h"
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/assertions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace preprocessing {
+class AssertionPipeline;
+class PreprocessingPass;
+class PreprocessingPassContext;
+}
+
 namespace smt {
 
+class Assertions;
 class ExpandDefs;
 struct SmtEngineStatistics;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 79678a5c0..7e8a4fb86 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -44,6 +44,7 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
+#include "smt/logic_exception.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/node_command.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 50f7ddfc7..4f10b6bc5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,12 +19,12 @@
 #ifndef CVC4__SMT_ENGINE_H
 #define CVC4__SMT_ENGINE_H
 
+#include <map>
+#include <memory>
 #include <string>
 #include <vector>
-#include <map>
 
 #include "context/cdhashmap_forward.h"
-#include "context/cdlist_forward.h"
 #include "options/options.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
@@ -87,7 +87,6 @@ class Model;
 class SmtEngineState;
 class AbstractValues;
 class Assertions;
-class ExprNames;
 class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
@@ -110,7 +109,6 @@ class DefinedFunction;
 
 struct SmtEngineStatistics;
 class SmtScope;
-class ProcessAssertions;
 class PfManager;
 class UnsatCoreManager;
 
@@ -120,7 +118,6 @@ ProofManager* currentProofManager();
 /* -------------------------------------------------------------------------- */
 
 namespace theory {
-  class TheoryModel;
   class Rewriter;
   class QuantifiersEngine;
 }/* CVC4::theory namespace */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ab251503b..89e75d892 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
+#include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 
diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
index ba02b5746..daa83ed54 100644
--- a/src/smt/unsat_core_manager.h
+++ b/src/smt/unsat_core_manager.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H
 #define CVC4__SMT__UNSAT_CORE_MANAGER_H
 
-#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 66e35bd52..c48948ade 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -19,7 +19,6 @@
 
 #include <unordered_set>
 
-#include "expr/node_manager.h"
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"