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/sygus | |
| 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/sygus')
5 files changed, 9 insertions, 1 deletions
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; |