diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-09 13:48:43 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-09 13:48:43 +0100 |
commit | 540ef6910a2b7ffeb67bac18dfc489fb4a6115d6 (patch) | |
tree | 23b0c78b126cb5b1584b75eca14fe648624a023a /src/smt | |
parent | b302cb1f92aae1c0954c86065469e5c2b7206e74 (diff) |
Some more cleanup of includes (#6083)
This PR does some more cleanup of the includes.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/assertions.cpp | 2 | ||||
-rw-r--r-- | src/smt/dump_manager.h | 1 | ||||
-rw-r--r-- | src/smt/preprocess_proof_generator.h | 8 | ||||
-rw-r--r-- | src/smt/preprocessor.cpp | 1 | ||||
-rw-r--r-- | src/smt/preprocessor.h | 1 | ||||
-rw-r--r-- | src/smt/process_assertions.cpp | 3 | ||||
-rw-r--r-- | src/smt/process_assertions.h | 11 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 7 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 1 | ||||
-rw-r--r-- | src/smt/unsat_core_manager.h | 1 | ||||
-rw-r--r-- | src/smt/witness_form.h | 1 |
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" |