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/theory/quantifiers | |
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/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_utils.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 1 |
7 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index f1307f142..842ef59bf 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -14,6 +14,8 @@ **/ #include "theory/quantifiers/single_inv_partition.h" +#include <sstream> + #include "expr/node_algorithm.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index cdc43658d..69adc9a4b 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -18,11 +18,12 @@ #define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #include <unordered_set> + #include "expr/node.h" #include "expr/node_trie.h" - #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 67f02b558..e56312362 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/sygus/sygus_abduct.h" +#include <sstream> + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 3edec96c7..9f8ac0e3c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/sygus/sygus_interpol.h" +#include <sstream> + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index ca87e1049..d793fb718 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/sygus_utils.h" +#include <sstream> + #include "expr/node_algorithm.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 275e9a27f..a5be5871f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index a72054f6d..c835369b7 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include "util/random.h" #include "util/sampler.h" |