More cleanup of includes to reduce compilation times (#6037)

Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.

31 files changed, 98 insertions, 55 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 3f03c00e2..6a326ed2e 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/abduction_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6776b06e2..5c1e1b879 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -19,6 +19,7 @@
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "smt/abstract_values.h"
 #include "smt/smt_engine.h"
 
 using namespace CVC4::theory;
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 5ce2556a7..bba4d2e29 100644
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -20,14 +20,14 @@
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "smt/abstract_values.h"
 
 namespace CVC4 {
 namespace smt {
 
+class AbstractValues;
+
 /**
  * Contains all information pertaining to the assertions of an SMT engine.
  *
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 310201f47..b211c61c2 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -15,8 +15,10 @@
 #include "smt/check_models.h"
 
 #include "options/smt_options.h"
+#include "smt/model.h"
 #include "smt/node_command.h"
 #include "smt/preprocessor.h"
+#include "smt/smt_solver.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index 14af41b27..f9d527867 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -19,12 +19,13 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/model.h"
-#include "smt/smt_solver.h"
 
 namespace CVC4 {
 namespace smt {
 
+class Model;
+class SmtSolver;
+
 /**
  * This utility is responsible for checking the current model.
  */
diff --git a/src/smt/command.h b/src/smt/command.h
index c11012944..a2230e12a 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -23,7 +23,6 @@
 #define CVC4__COMMAND_H
 
 #include <iosfwd>
-#include <map>
 #include <sstream>
 #include <string>
 #include <vector>
@@ -40,8 +39,6 @@ class Term;
 }  // namespace api
 
 class SymbolManager;
-class UnsatCore;
-class SmtEngine;
 class Command;
 class CommandStatus;
 
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 192bb2324..c7a05e21b 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,13 +20,17 @@
 #include <memory>
 #include <vector>
 
-#include "context/cdlist.h"
+#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {
 
 class NodeCommand;
 
+namespace context {
+class UserContext;
+}
+
 namespace smt {
 
 /**
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index c2c4b6fd2..c01b5a243 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -18,8 +18,10 @@
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "smt/defined_function.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::preprocessing;
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 486aa0c3a..0c2f9b2d5 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -20,17 +20,23 @@
 #include <unordered_map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "smt/smt_engine_stats.h"
-#include "util/resource_manager.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+class ResourceManager;
 class SmtEngine;
+class TConvProofGenerator;
+
+namespace preprocessing {
+class AssertionPipeline;
+}
 
 namespace smt {
 
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of expanding definitions for an SMT engine.
  *
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 09ddfde75..965f49855 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/interpolation_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index d4cf33554..2482f77ef 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -22,11 +22,10 @@
 
 #include <ostream>
 
-#include "options/open_ostream.h"
-#include "smt/update_ostream.h"
-
 namespace CVC4 {
 
+class OstreamOpener;
+
 /** This abstracts the management of ostream memory and initialization. */
 class ManagedOstream {
  public:
diff --git a/src/smt/model.h b/src/smt/model.h
index e7c2434a6..277803499 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -21,13 +21,15 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
-#include "util/cardinality.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace theory {
+class TheoryModel;
+}
+
 namespace smt {
 
 class Model;
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cabd7bd20..95c9f1d18 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -18,6 +18,8 @@
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 5c45a6a56..6c453987e 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -21,10 +21,13 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 
+namespace theory {
+class TheoryModel;
+}
+
 /**
  * A utility for blocking the current model.
  */
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 33b5d9953..3fc3a2e0c 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -16,6 +16,8 @@
 
 #include "smt/node_command.h"
 
+#include <sstream>
+
 #include "printer/printer.h"
 
 namespace CVC4 {
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 983b98b34..81b935f36 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -15,15 +15,15 @@
 #ifndef CVC4__SMT__OPTIONS_MANAGER_H
 #define CVC4__SMT__OPTIONS_MANAGER_H
 
-#include "options/options.h"
 #include "options/options_listener.h"
 #include "smt/managed_ostreams.h"
 
 namespace CVC4 {
 
-class SmtEngine;
 class LogicInfo;
+class Options;
 class ResourceManager;
+class SmtEngine;
 
 namespace smt {
 
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index ef80ebdae..261450dbb 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,6 +16,8 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "options/proof_options.h"
 #include "theory/rewriter.h"
 
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 01d9c89da..312e58453 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -20,12 +20,10 @@
 #include <map>
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/lazy_proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node_manager.h"
-#include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 3e4ef0cdd..e5e9b98f4 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -19,8 +19,10 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/dump.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/smt_engine.h"
 
+using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
 
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 22b585e05..ece5fb5a8 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -17,14 +17,16 @@
 #ifndef CVC4__SMT__PREPROCESSOR_H
 #define CVC4__SMT__PREPROCESSOR_H
 
-#include <vector>
+#include <memory>
 
-#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/expand_definitions.h"
 #include "smt/process_assertions.h"
 #include "theory/booleans/circuit_propagator.h"
 
 namespace CVC4 {
+namespace preprocessing {
+class PreprocessingPassContext;
+}
 namespace smt {
 
 class AbstractValues;
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 0c01abbbb..23890d9fc 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -31,10 +31,13 @@
 #include "printer/printer.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
+#include "smt/expand_definitions.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index ca834459d..891ef93f1 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
 #define CVC4__SMT__PROCESS_ASSERTIONS_H
 
-#include <map>
+#include <unordered_map>
 
-#include "context/cdhashmap.h"
 #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 "smt/expand_definitions.h"
-#include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -36,6 +33,9 @@ class SmtEngine;
 
 namespace smt {
 
+class ExpandDefs;
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of processing assertions for an SMT engine.
  *
@@ -54,7 +54,7 @@ class ProcessAssertions
 {
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
-  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
  public:
   ProcessAssertions(SmtEngine& smt,
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index cb7943aed..2f7683e7c 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -14,11 +14,15 @@
 
 #include "smt/proof_manager.h"
 
+#include "expr/proof_checker.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/base_options.h"
 #include "options/proof_options.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
+#include "smt/preprocess_proof_generator.h"
+#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 namespace smt {
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index a6f284cad..abb984ea9 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -18,22 +18,21 @@
 #define CVC4__SMT__PROOF_MANAGER_H
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
-#include "smt/preprocess_proof_generator.h"
-#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+class ProofNode;
+class ProofNodeManager;
 class SmtEngine;
 
 namespace smt {
 
 class Assertions;
 class DefinedFunction;
+class PreprocessProofGenerator;
+class ProofPostproccess;
 
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 0898096f5..f7811911b 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/proof_post_processor.h"
 
+#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index de74d4869..b3e636b58 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -22,6 +22,7 @@
 
 #include "expr/proof_node_updater.h"
 #include "smt/witness_form.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 80d7b96fa..891349809 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,11 +34,13 @@
 #include "printer/printer.h"
 #include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
+#include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
+#include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8974e5e60..50e45c52f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -887,8 +887,6 @@ class CVC4_PUBLIC SmtEngine
   /* .......................................................................  */
  private:
   /* .......................................................................  */
-  /** The type of our internal assertion list */
-  typedef context::CDList<Node> AssertionList;
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) = delete;
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 996a51e90..9b5871139 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -20,9 +20,12 @@
 #include "smt/preprocessor.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 
+using namespace std;
+
 namespace CVC4 {
 namespace smt {
 
@@ -67,12 +70,12 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -88,12 +91,12 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5f08efb14..133d1e692 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -18,8 +18,11 @@
 #include <vector>
 
 #include "expr/attribute.h"
+#include "expr/lazy_proof.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_context_stack.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 803021fc3..c2a88d718 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -18,22 +18,22 @@
 
 #pragma once
 
-#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/term_context_stack.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "theory/eager_proof_generator.h"
+#include "expr/term_context.h"
 #include "theory/trust_node.h"
-#include "util/bool.h"
 #include "util/hash.h"
 
 namespace CVC4 {
 
+class LazyCDProof;
+class ProofNodeManager;
+class TConvProofGenerator;
+
 class RemoveTermFormulas {
  public:
   RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);