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/theory/bv | |
| 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/theory/bv')
| -rw-r--r-- | src/theory/bv/bitblast/simple_bitblaster.cpp | 1 | ||||
| -rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 1 | ||||
| -rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 1 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 1 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.h | 1 |
5 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp index 551c18612..4c7311945 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 38e4b3aa6..d9adf06fb 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -24,6 +24,7 @@ #include <unordered_map> #include <unordered_set> +#include "context/cdhashset.h" #include "context/cdqueue.h" #include "context/context.h" #include "theory/theory.h" diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index d8d8dbed7..3cadac621 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -30,6 +30,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4::theory::bv::utils; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 55a0ff46b..47974fc03 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,6 +21,7 @@ #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/ee_setup_info.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 2aa722e48..fafde0601 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { |