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/theory/quantifiers/sygus | |
parent | b302cb1f92aae1c0954c86065469e5c2b7206e74 (diff) |
Some more cleanup of includes (#6083)
This PR does some more cleanup of the includes.
Diffstat (limited to 'src/theory/quantifiers/sygus')
26 files changed, 32 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 4c232ef78..3e223fd7c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "options/quantifiers_options.h" +#include "smt/logic_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" @@ -27,6 +28,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 5ac93d436..509e4905e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 7c1ed40eb..56743e264 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index e2573bb52..3c6ab6bc1 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/transition_inference.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" #include "util/random.h" diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 742b3a3d9..fec15fdc6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/cegis_unif.h" +#include "expr/sygus_datatype.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index d9ec52aff..61c0327b7 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -18,8 +18,6 @@ #ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H #define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H -#include "context/cdhashmap.h" -#include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index b550c3550..4f870830e 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -18,8 +18,11 @@ #include "expr/node_algorithm.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" +#include "smt/logic_exception.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/sygus/type_node_id_trie.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 4fe2b8afc..9025b1a51 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -16,7 +16,9 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "smt/logic_exception.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/sygus_invariance.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index bf6807151..262062f14 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -20,12 +20,14 @@ #include <vector> #include "expr/node.h" -#include "theory/quantifiers/sygus/sygus_invariance.h" namespace CVC4 { namespace theory { namespace quantifiers { +class SygusInvarianceTest; +class TermDbSygus; + /** Recursive term builder * * This is a utility used to generate variants diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 278233668..49c0f5f47 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/strings/word.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 4dd85e0ac..bb4bb6384 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -19,7 +19,6 @@ #include <map> #include <memory> -#include <string> #include <vector> #include "expr/node.h" diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index be6d4c7eb..1740ecc3d 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 4ef0f8f08..86d113edc 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H #define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H -#include <map> #include <vector> #include "expr/node.h" diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index aa2551251..bc9da0c4d 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/example_infer.h" +#include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 52e574d49..7b20df8de 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -17,14 +17,13 @@ #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H -#include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" -#include "theory/quantifiers/sygus/sygus_unif_io.h" namespace CVC4 { namespace theory { namespace quantifiers { +class SygusUnifIo; class SynthConjecture; /** SygusPbe diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 1123830f3..3629164ee 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -15,10 +15,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H #define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H -#include <string> -#include <vector> #include "expr/node.h" -#include "expr/type_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 1400882eb..0911b73c2 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -24,6 +24,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/logic_info.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 30d04c8e2..319497f77 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -19,16 +19,17 @@ #include <unordered_set> #include "expr/node.h" -#include "theory/logic_info.h" namespace CVC4 { + +class LogicInfo; + namespace theory { class QuantifiersEngine; namespace quantifiers { -class CegConjecture; class TermDbSygus; /** SygusRepairConst diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 2c0ac227b..a9891aa72 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/strings/word.h" #include "util/random.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 732b52bf9..a3cf5ed19 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -19,6 +19,7 @@ #include "printer/printer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" #include "util/random.h" #include <math.h> diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 57043086b..dc864fbd8 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -19,6 +19,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "smt/logic_exception.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -29,9 +30,12 @@ #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_enumerator_basic.h" #include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 47ebe6853..27c565795 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -20,7 +20,6 @@ #include <memory> -#include "theory/decision_manager.h" #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" @@ -28,8 +27,6 @@ #include "theory/quantifiers/sygus/cegis_unif.h" #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/example_infer.h" -#include "theory/quantifiers/sygus/sygus_grammar_cons.h" -#include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "theory/quantifiers/sygus/sygus_stats.h" @@ -39,6 +36,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class CegGrammarConstructor; +class SygusPbe; class SygusStatistics; /** diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 0a50f90c7..543d5e7f0 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index a8f247b58..9266a3f9d 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -20,6 +20,7 @@ #include "expr/sygus_datatype.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/sygus/type_node_id_trie.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 43a6cd07a..7b45d115b 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -18,10 +18,8 @@ #define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H #include <map> -#include <unordered_set> #include "expr/node.h" -#include "theory/quantifiers/sygus/type_node_id_trie.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h index 5625a8d1f..020c8d086 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -26,8 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class TermDbSygus; - /** * A trie indexed by types that assigns unique identifiers to nodes based on * a vector of types. |