diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-02 01:58:20 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-02 00:58:20 +0000 |
commit | b5073e16ea49ce9214fcc5318ce080724719c809 (patch) | |
tree | 1073858c57a3590b67ae7fd8e6fa2d46872f9114 /src/expr | |
parent | 822ae21e0b26e9a98b3a5585dbcd2694bbbce685 (diff) |
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.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/buffered_proof_generator.cpp | 1 | ||||
-rw-r--r-- | src/expr/buffered_proof_generator.h | 7 | ||||
-rw-r--r-- | src/expr/datatype_index.cpp | 1 | ||||
-rw-r--r-- | src/expr/datatype_index.h | 1 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 1 | ||||
-rw-r--r-- | src/expr/dtype.h | 6 | ||||
-rw-r--r-- | src/expr/lazy_proof.cpp | 1 | ||||
-rw-r--r-- | src/expr/lazy_proof.h | 3 | ||||
-rw-r--r-- | src/expr/lazy_proof_chain.cpp | 1 | ||||
-rw-r--r-- | src/expr/lazy_proof_chain.h | 3 | ||||
-rw-r--r-- | src/expr/node.cpp | 1 | ||||
-rw-r--r-- | src/expr/node.h | 5 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 1 | ||||
-rw-r--r-- | src/expr/node_traversal.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_traversal.h | 1 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/expr/proof.cpp | 2 | ||||
-rw-r--r-- | src/expr/proof.h | 3 |
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. * |