diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-03 17:50:45 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-03 16:50:45 +0000 |
commit | a02a794c383ae2381e1210f53174cefb8d94e615 (patch) | |
tree | 0eac511c22ba9eeba1925e3afa4f0542edf5cf60 /src/smt | |
parent | 6db84f6e373f9651af48df7b654e3992f68472ac (diff) |
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.
Diffstat (limited to 'src/smt')
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); |