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/bags | |
parent | b302cb1f92aae1c0954c86065469e5c2b7206e74 (diff) |
Some more cleanup of includes (#6083)
This PR does some more cleanup of the includes.
Diffstat (limited to 'src/theory/bags')
-rw-r--r-- | src/theory/bags/bag_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/bags/bag_solver.h | 11 | ||||
-rw-r--r-- | src/theory/bags/bags_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/bags/bags_statistics.h | 1 | ||||
-rw-r--r-- | src/theory/bags/inference_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/bags/inference_generator.h | 8 | ||||
-rw-r--r-- | src/theory/bags/inference_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/bags/inference_manager.h | 4 | ||||
-rw-r--r-- | src/theory/bags/solver_state.h | 1 | ||||
-rw-r--r-- | src/theory/bags/term_registry.cpp | 3 | ||||
-rw-r--r-- | src/theory/bags/term_registry.h | 7 | ||||
-rw-r--r-- | src/theory/bags/theory_bags.cpp | 3 | ||||
-rw-r--r-- | src/theory/bags/theory_bags.h | 4 |
13 files changed, 29 insertions, 23 deletions
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 869b229ea..a7a0f8796 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -17,6 +17,10 @@ #include "theory/bags/bag_solver.h" #include "theory/bags/inference_generator.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/normal_form.h" +#include "theory/bags/solver_state.h" +#include "theory/bags/term_registry.h" #include "theory/uf/equality_engine_iterator.h" using namespace std; diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index e524f7422..914a12ae2 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -17,19 +17,16 @@ #ifndef CVC4__THEORY__BAG__SOLVER_H #define CVC4__THEORY__BAG__SOLVER_H -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "theory/bags/infer_info.h" #include "theory/bags/inference_generator.h" -#include "theory/bags/inference_manager.h" -#include "theory/bags/normal_form.h" -#include "theory/bags/solver_state.h" -#include "theory/bags/term_registry.h" namespace CVC4 { namespace theory { namespace bags { +class InferenceManager; +class SolverState; +class TermRegistry; + /** The solver for the theory of bags * */ diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 3718aedb7..51b2e5438 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -18,7 +18,7 @@ #define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H #include "theory/bags/rewrites.h" -#include "theory/rewriter.h" +#include "theory/theory_rewriter.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index caf4070ec..f59c43cb6 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__BAGS_STATISTICS_H #define CVC4__THEORY__BAGS_STATISTICS_H -#include "expr/kind.h" #include "theory/bags/rewrites.h" #include "util/statistics_registry.h" diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index c61075f51..0d56080c4 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -17,6 +17,8 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" #include "expr/skolem_manager.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" #include "theory/uf/equality_engine.h" namespace CVC4 { diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index d6fc184c7..bfaf5d0fc 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -17,18 +17,16 @@ #ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H #define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H -#include <map> -#include <vector> - #include "expr/node.h" #include "infer_info.h" -#include "theory/bags/inference_manager.h" -#include "theory/bags/solver_state.h" namespace CVC4 { namespace theory { namespace bags { +class InferenceManager; +class SolverState; + /** * An inference generator class. This class is used by the core solver to * generate lemmas diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 44a18bcc4..dcc5387e9 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -14,6 +14,8 @@ #include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" + using namespace std; using namespace CVC4::kind; diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index 8b0fe0590..d74d3c189 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -17,14 +17,14 @@ #ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H #define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H -#include "theory/bags/infer_info.h" -#include "theory/bags/solver_state.h" #include "theory/inference_manager_buffered.h" namespace CVC4 { namespace theory { namespace bags { +class SolverState; + /** Inference manager * * This class manages inferences produced by the theory of bags. It manages diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 93f1af11d..d8820d8c4 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -18,7 +18,6 @@ #define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H #include <map> -#include <vector> #include "theory/theory_state.h" diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 38c494219..192fd6809 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -14,6 +14,9 @@ #include "theory/bags/term_registry.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" + using namespace std; using namespace CVC4::kind; diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index fcd822e16..87e61a026 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -18,16 +18,17 @@ #define CVC4__THEORY__BAGS__TERM_REGISTRY_H #include <map> -#include <vector> #include "context/cdhashmap.h" -#include "theory/bags/inference_manager.h" -#include "theory/bags/solver_state.h" +#include "expr/node.h" namespace CVC4 { namespace theory { namespace bags { +class InferenceManager; +class SolverState; + /** * Term registry, the purpose of this class is to maintain a database of * commonly used terms, and mappings from bags to their "proxy variables". diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 253fe2b7f..2950739e4 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -14,6 +14,9 @@ #include "theory/bags/theory_bags.h" +#include "smt/logic_exception.h" +#include "theory/bags/normal_form.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" using namespace CVC4::kind; diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 3839629d4..df64c3f1c 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -17,17 +17,15 @@ #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H #define CVC4__THEORY__BAGS__THEORY_BAGS_H -#include <memory> - #include "theory/bags/bag_solver.h" #include "theory/bags/bags_rewriter.h" #include "theory/bags/bags_statistics.h" #include "theory/bags/inference_generator.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" +#include "theory/bags/term_registry.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { |