From 540ef6910a2b7ffeb67bac18dfc489fb4a6115d6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 9 Mar 2021 13:48:43 +0100 Subject: Some more cleanup of includes (#6083) This PR does some more cleanup of the includes. --- src/theory/arith/approx_simplex.cpp | 1 + src/theory/arith/approx_simplex.h | 1 - src/theory/arith/arith_preprocess.cpp | 2 ++ src/theory/arith/arith_preprocess.h | 9 ++++--- src/theory/arith/arith_static_learner.h | 7 ++--- src/theory/arith/arith_utilities.cpp | 4 ++- src/theory/arith/arith_utilities.h | 2 -- src/theory/arith/attempt_solution_simplex.cpp | 2 ++ src/theory/arith/callbacks.cpp | 1 + src/theory/arith/callbacks.h | 4 ++- src/theory/arith/congruence_manager.cpp | 7 +++++ src/theory/arith/congruence_manager.h | 31 ++++++++++++++++------ src/theory/arith/constraint.cpp | 5 ++++ src/theory/arith/constraint.h | 24 +++++++++-------- src/theory/arith/cut_log.h | 3 --- src/theory/arith/dio_solver.cpp | 1 + src/theory/arith/dio_solver.h | 6 ++--- src/theory/arith/dual_simplex.cpp | 1 + src/theory/arith/error_set.h | 1 - src/theory/arith/fc_simplex.h | 2 ++ src/theory/arith/infer_bounds.h | 1 - src/theory/arith/inference_manager.cpp | 1 + src/theory/arith/inference_manager.h | 4 +-- src/theory/arith/nl/cad/constraints.h | 3 --- src/theory/arith/nl/cad/projections.h | 2 -- src/theory/arith/nl/cad/proof_checker.h | 1 - src/theory/arith/nl/cad/proof_generator.cpp | 3 +++ src/theory/arith/nl/cad/proof_generator.h | 9 ++++--- src/theory/arith/nl/cad_solver.h | 3 +++ src/theory/arith/nl/ext/constraint.cpp | 1 + src/theory/arith/nl/ext/constraint.h | 3 ++- src/theory/arith/nl/ext/ext_state.cpp | 2 ++ src/theory/arith/nl/ext/factoring_check.cpp | 1 + src/theory/arith/nl/ext/factoring_check.h | 6 ++++- src/theory/arith/nl/ext/monomial_bounds_check.cpp | 1 + src/theory/arith/nl/ext/monomial_bounds_check.h | 3 ++- src/theory/arith/nl/ext/monomial_check.cpp | 2 ++ src/theory/arith/nl/ext/monomial_check.h | 4 ++- src/theory/arith/nl/ext/split_zero_check.cpp | 1 + src/theory/arith/nl/ext/split_zero_check.h | 3 ++- src/theory/arith/nl/ext/tangent_plane_check.cpp | 1 + src/theory/arith/nl/ext/tangent_plane_check.h | 5 +++- src/theory/arith/nl/ext_theory_callback.h | 3 +++ src/theory/arith/nl/iand_solver.h | 1 - src/theory/arith/nl/iand_utils.h | 1 - src/theory/arith/nl/nl_model.cpp | 1 + src/theory/arith/nl/nl_model.h | 2 +- src/theory/arith/nl/nonlinear_extension.cpp | 1 + src/theory/arith/nl/nonlinear_extension.h | 3 +++ .../arith/nl/transcendental/exponential_solver.cpp | 2 ++ .../arith/nl/transcendental/exponential_solver.h | 6 ++--- src/theory/arith/nl/transcendental/sine_solver.cpp | 3 +++ src/theory/arith/nl/transcendental/sine_solver.h | 3 --- .../nl/transcendental/transcendental_solver.cpp | 1 + .../nl/transcendental/transcendental_state.cpp | 2 ++ .../arith/nl/transcendental/transcendental_state.h | 9 +++++-- src/theory/arith/normal_form.h | 1 - src/theory/arith/operator_elim.cpp | 1 + src/theory/arith/operator_elim.h | 4 ++- src/theory/arith/partial_model.h | 5 ++-- src/theory/arith/proof_checker.h | 1 - src/theory/arith/simplex.cpp | 6 +++-- src/theory/arith/simplex.h | 7 ++--- src/theory/arith/soi_simplex.cpp | 1 + src/theory/arith/soi_simplex.h | 2 ++ src/theory/arith/theory_arith.cpp | 2 ++ src/theory/arith/theory_arith.h | 1 - src/theory/arith/theory_arith_private.h | 15 +++-------- src/theory/arrays/array_info.h | 3 --- src/theory/arrays/proof_checker.h | 1 - src/theory/arrays/theory_arrays.h | 1 - src/theory/atom_requests.h | 2 +- src/theory/bags/bag_solver.cpp | 4 +++ src/theory/bags/bag_solver.h | 11 +++----- src/theory/bags/bags_rewriter.h | 2 +- src/theory/bags/bags_statistics.h | 1 - src/theory/bags/inference_generator.cpp | 2 ++ src/theory/bags/inference_generator.h | 8 +++--- src/theory/bags/inference_manager.cpp | 2 ++ src/theory/bags/inference_manager.h | 4 +-- src/theory/bags/solver_state.h | 1 - src/theory/bags/term_registry.cpp | 3 +++ src/theory/bags/term_registry.h | 7 ++--- src/theory/bags/theory_bags.cpp | 3 +++ src/theory/bags/theory_bags.h | 4 +-- src/theory/booleans/circuit_propagator.cpp | 4 +++ src/theory/booleans/circuit_propagator.h | 13 ++++----- src/theory/booleans/proof_checker.h | 1 - src/theory/booleans/proof_circuit_propagator.cpp | 1 + src/theory/booleans/proof_circuit_propagator.h | 6 ++++- src/theory/builtin/theory_builtin_rewriter.h | 1 - src/theory/builtin/theory_builtin_type_rules.h | 1 - src/theory/builtin/type_enumerator.cpp | 2 ++ src/theory/builtin/type_enumerator.h | 1 - src/theory/bv/bitblast/aig_bitblaster.cpp | 1 + src/theory/bv/bitblast/aig_bitblaster.h | 4 ++- src/theory/bv/bitblast/eager_bitblaster.h | 2 +- src/theory/bv/bitblast/lazy_bitblaster.h | 6 +++-- src/theory/bv/bv_eager_solver.h | 3 --- src/theory/bv/bv_inequality_graph.h | 5 ++-- src/theory/bv/bv_solver_simple.h | 2 -- src/theory/bv/bv_subtheory_algebraic.cpp | 1 + src/theory/bv/bv_subtheory_core.h | 1 - src/theory/bv/bv_subtheory_inequality.cpp | 1 + src/theory/bv/slicer.cpp | 2 ++ src/theory/bv/theory_bv.h | 2 -- src/theory/bv/theory_bv_rewriter.h | 2 -- src/theory/bv/theory_bv_utils.h | 1 - src/theory/combination_care_graph.cpp | 1 + src/theory/combination_engine.cpp | 3 +++ src/theory/combination_engine.h | 7 ++--- src/theory/datatypes/datatypes_rewriter.h | 2 -- src/theory/datatypes/infer_proof_cons.cpp | 2 ++ src/theory/datatypes/infer_proof_cons.h | 7 ++--- src/theory/datatypes/inference.h | 4 +-- src/theory/datatypes/inference_manager.h | 2 -- src/theory/datatypes/sygus_extension.cpp | 3 +++ src/theory/datatypes/sygus_extension.h | 8 +++--- src/theory/datatypes/sygus_simple_sym.h | 1 - src/theory/datatypes/theory_datatypes.cpp | 4 +++ src/theory/datatypes/theory_datatypes.h | 1 + src/theory/decision_strategy.h | 1 - src/theory/eager_proof_generator.cpp | 1 + src/theory/eager_proof_generator.h | 6 ++++- src/theory/ee_manager_distributed.cpp | 1 + src/theory/ee_manager_distributed.h | 6 +++-- src/theory/engine_output_channel.h | 4 ++- src/theory/ext_theory.h | 5 ++-- src/theory/fp/fp_converter.cpp | 2 ++ src/theory/fp/fp_converter.h | 2 -- src/theory/inference_id.h | 7 ++--- src/theory/inference_manager_buffered.h | 1 - src/theory/logic_info.h | 3 ++- src/theory/model_manager.cpp | 1 + src/theory/model_manager.h | 5 ++-- src/theory/model_manager_distributed.cpp | 1 + src/theory/model_manager_distributed.h | 2 -- src/theory/output_channel.h | 5 ---- .../quantifiers/candidate_rewrite_database.cpp | 1 + .../quantifiers/candidate_rewrite_database.h | 4 +-- .../quantifiers/cegqi/ceg_arith_instantiator.cpp | 1 + .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 1 + src/theory/quantifiers/conjecture_generator.cpp | 1 + .../inst_match_generator_multi_linear.cpp | 1 + .../ematching/inst_match_generator_simple.cpp | 1 + src/theory/quantifiers/ematching/trigger.cpp | 3 +++ src/theory/quantifiers/ematching/trigger.h | 7 ++--- .../quantifiers/ematching/var_match_generator.h | 1 - src/theory/quantifiers/fmf/full_model_check.cpp | 1 + src/theory/quantifiers/fmf/model_builder.cpp | 1 + src/theory/quantifiers/fmf/model_builder.h | 4 +-- src/theory/quantifiers/inst_strategy_enumerative.h | 5 ++-- src/theory/quantifiers/instantiate.cpp | 3 +++ src/theory/quantifiers/instantiate.h | 4 ++- src/theory/quantifiers/quant_conflict_find.cpp | 1 + src/theory/quantifiers/quantifiers_modules.cpp | 1 + .../quantifiers/sygus/ce_guided_single_inv.cpp | 2 ++ .../quantifiers/sygus/ce_guided_single_inv_sol.cpp | 1 + src/theory/quantifiers/sygus/cegis.cpp | 1 + .../quantifiers/sygus/cegis_core_connective.cpp | 1 + src/theory/quantifiers/sygus/cegis_unif.cpp | 1 + src/theory/quantifiers/sygus/example_infer.h | 2 -- src/theory/quantifiers/sygus/sygus_enumerator.cpp | 3 +++ src/theory/quantifiers/sygus/sygus_explain.cpp | 2 ++ src/theory/quantifiers/sygus/sygus_explain.h | 4 ++- .../quantifiers/sygus/sygus_grammar_cons.cpp | 1 + src/theory/quantifiers/sygus/sygus_grammar_norm.h | 1 - src/theory/quantifiers/sygus/sygus_invariance.cpp | 1 + src/theory/quantifiers/sygus/sygus_module.h | 1 - src/theory/quantifiers/sygus/sygus_pbe.cpp | 1 + src/theory/quantifiers/sygus/sygus_pbe.h | 3 +-- src/theory/quantifiers/sygus/sygus_qe_preproc.h | 3 --- .../quantifiers/sygus/sygus_repair_const.cpp | 1 + src/theory/quantifiers/sygus/sygus_repair_const.h | 5 ++-- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 1 + src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 1 + src/theory/quantifiers/sygus/synth_conjecture.cpp | 4 +++ src/theory/quantifiers/sygus/synth_conjecture.h | 5 ++-- .../quantifiers/sygus/transition_inference.cpp | 1 + src/theory/quantifiers/sygus/type_info.cpp | 1 + src/theory/quantifiers/sygus/type_info.h | 2 -- src/theory/quantifiers/sygus/type_node_id_trie.h | 2 -- src/theory/quantifiers/sygus_inst.cpp | 1 + src/theory/quantifiers/term_database.h | 2 +- src/theory/quantifiers_engine.cpp | 1 + src/theory/relevance_manager.cpp | 2 ++ src/theory/sets/cardinality_extension.cpp | 1 + src/theory/sets/inference_manager.cpp | 1 + src/theory/sets/theory_sets.h | 1 + src/theory/shared_solver.cpp | 2 ++ src/theory/shared_solver.h | 7 ++--- src/theory/smt_engine_subsolver.h | 1 - src/theory/sort_inference.h | 5 ++-- src/theory/strings/base_solver.cpp | 1 + src/theory/strings/core_solver.cpp | 2 ++ src/theory/strings/infer_proof_cons.cpp | 1 + src/theory/strings/regexp_solver.cpp | 1 + src/theory/strings/solver_state.cpp | 1 + src/theory/term_registration_visitor.cpp | 1 + src/theory/theory_engine.cpp | 3 ++- src/theory/theory_id.h | 2 +- src/theory/theory_inference_manager.cpp | 1 + src/theory/theory_inference_manager.h | 1 + src/theory/theory_model.cpp | 1 + src/theory/theory_model_builder.cpp | 1 + src/theory/theory_preprocessor.cpp | 1 + src/theory/uf/cardinality_extension.cpp | 2 ++ src/theory/uf/cardinality_extension.h | 3 +-- src/theory/uf/equality_engine.cpp | 3 +++ src/theory/uf/equality_engine.h | 5 +--- src/theory/uf/proof_equality_engine.cpp | 4 +++ src/theory/uf/proof_equality_engine.h | 10 ++++--- src/theory/uf/theory_uf.cpp | 1 + src/theory/uf/theory_uf.h | 3 --- src/theory/uf/theory_uf_model.cpp | 2 ++ src/theory/uf/theory_uf_model.h | 4 ++- src/theory/valuation.cpp | 1 + src/theory/valuation.h | 2 +- 218 files changed, 401 insertions(+), 250 deletions(-) (limited to 'src/theory') diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 152146cdf..80690f39c 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -28,6 +28,7 @@ #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" +#include "theory/eager_proof_generator.h" using namespace std; diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 58e115b81..46e252ec7 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -66,7 +66,6 @@ class NodeLog; class TreeLog; class ArithVariables; class CutInfo; -class RowsDeleted; class ApproximateSimplex{ public: diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 0c1923448..a075c87fe 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -14,7 +14,9 @@ #include "theory/arith/arith_preprocess.h" +#include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" +#include "theory/skolem_lemma.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index 69cc02bb9..db0fd7d5e 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -18,16 +18,19 @@ #define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H #include "context/cdhashmap.h" -#include "theory/arith/arith_state.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/operator_elim.h" #include "theory/logic_info.h" -#include "theory/skolem_lemma.h" namespace CVC4 { namespace theory { + +class SkolemLemma; + namespace arith { +class ArithState; +class InferenceManager; + /** * This module can be used for (on demand) elimination of extended arithmetic * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 2b74e6005..799d0bcee 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -20,14 +20,15 @@ #ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H #define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H -#include - #include "context/cdhashmap.h" -#include "context/context.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/delta_rational.h" #include "util/statistics_registry.h" namespace CVC4 { +namespace context { +class Context; +} namespace theory { namespace arith { diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index f9051328c..4f1f50b7a 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -14,6 +14,8 @@ #include "arith_utilities.h" +#include + using namespace CVC4::kind; namespace CVC4 { @@ -114,7 +116,7 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec) Rational cr = c.getConst(); unsigned lower = 0; - unsigned upper = pow(10, prec); + unsigned upper = std::pow(10, prec); Rational den = Rational(upper); if (cr.getDenominator() < den.getNumerator()) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index e4d6bd0ee..40ca7b8f6 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define CVC4__THEORY__ARITH__ARITH_UTILITIES_H -#include #include #include #include @@ -25,7 +24,6 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "theory/arith/arithvar.h" -#include "theory/arith/delta_rational.h" #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index efcb96325..e5c995971 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -21,6 +21,8 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" +#include "theory/arith/linear_equality.h" +#include "theory/arith/tableau.h" using namespace std; diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 84bfafcc8..ee412483b 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -17,6 +17,7 @@ #include "theory/arith/callbacks.h" +#include "expr/proof_node.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 9fbe3b90f..574d289b0 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -18,13 +18,15 @@ #pragma once #include "expr/node.h" -#include "expr/proof_node.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" #include "theory/arith/constraint_forward.h" #include "util/rational.h" namespace CVC4 { + +class ProofNode; + namespace theory { namespace arith { diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 636cebe5f..f2210574b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -18,9 +18,16 @@ #include "theory/arith/congruence_manager.h" #include "base/output.h" +#include "expr/proof_node.h" +#include "expr/proof_node_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/constraint.h" +#include "theory/arith/partial_model.h" +#include "theory/ee_setup_info.h" +#include "theory/rewriter.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/proof_equality_engine.h" #include "options/arith_options.h" namespace CVC4 { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index f2aef815f..9815ad9c8 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -19,27 +19,42 @@ #pragma once +#include "context/cdhashmap.h" #include "context/cdlist.h" #include "context/cdmaybe.h" -#include "context/cdo.h" #include "context/cdtrail_queue.h" -#include "context/context.h" -#include "expr/proof_node_manager.h" #include "theory/arith/arithvar.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" -#include "theory/arith/partial_model.h" -#include "theory/eager_proof_generator.h" -#include "theory/ee_setup_info.h" #include "theory/trust_node.h" -#include "theory/uf/equality_engine.h" -#include "theory/uf/proof_equality_engine.h" +#include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" #include "util/statistics_registry.h" namespace CVC4 { + +class ProofNodeManager; + +namespace context { +class Context; +class UserContext; +} + namespace theory { + +class EagerProofGenerator; +struct EeSetupInfo; + +namespace eq { +class ProofEqEngine; +class EqualityEngine; +} + namespace arith { +class ArithVariables; + class ArithCongruenceManager { private: context::CDRaised d_inConflict; diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 70106b14c..bafd4d682 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -21,9 +21,14 @@ #include #include "base/output.h" +#include "expr/proof_node_manager.h" #include "smt/smt_statistics_registry.h" +#include "theory/eager_proof_generator.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" +#include "theory/arith/partial_model.h" +#include "theory/rewriter.h" using namespace std; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 6a73d69d2..6ac03bb82 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -78,36 +78,38 @@ #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H #define CVC4__THEORY__ARITH__CONSTRAINT_H -#include -#include #include #include #include "base/configuration_private.h" #include "context/cdlist.h" #include "context/cdqueue.h" -#include "context/context.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" -#include "theory/arith/congruence_manager.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" #include "theory/trust_node.h" +#include "util/statistics_registry.h" namespace CVC4 { -namespace theory { -namespace arith { -class Comparison; -} -} + +class ProofNodeManager; + +namespace context { +class Context; } -namespace CVC4 { namespace theory { + +class EagerProofGenerator; + namespace arith { +class Comparison; +class ArithCongruenceManager; +class ArithVariables; + /** * Logs the types of different proofs. * Current, proof types: diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index f6f974fca..2b67026dc 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -22,13 +22,11 @@ #include #include #include -#include #include "expr/kind.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -230,7 +228,6 @@ public: }; std::ostream& operator<<(std::ostream& os, const NodeLog& nl); -class ApproximateSimplex; class TreeLog { private: int next_exec_ord; diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 2c06967c4..a232464e5 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -20,6 +20,7 @@ #include "base/output.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/arith/partial_model.h" using namespace std; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 571c64a78..3ce7199c0 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -24,18 +24,18 @@ #include #include -#include "base/output.h" #include "context/cdlist.h" #include "context/cdmaybe.h" #include "context/cdo.h" #include "context/cdqueue.h" -#include "context/context.h" #include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" #include "util/rational.h" #include "util/statistics_registry.h" namespace CVC4 { +namespace context { +class Context; +} namespace theory { namespace arith { diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 3784ec79b..5ad2f16c0 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -21,6 +21,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" +#include "theory/arith/linear_equality.h" using namespace std; diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 34d695f8a..7400a229f 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -62,7 +62,6 @@ namespace arith { class ErrorSet; -class ErrorInfoMap; class ComparatorPivotRule { private: diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 658f7c23e..45a9b79bb 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -55,7 +55,9 @@ #pragma once #include "theory/arith/error_set.h" +#include "theory/arith/linear_equality.h" #include "theory/arith/simplex.h" +#include "theory/arith/simplex_update.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index e1eb786d0..03ab8e53b 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -23,7 +23,6 @@ #include "expr/node.h" #include "theory/arith/delta_rational.h" -#include "theory/theory.h" #include "util/integer.h" #include "util/maybe.h" #include "util/rational.h" diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index c4281f0bd..a281c825b 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -15,6 +15,7 @@ #include "theory/arith/inference_manager.h" #include "options/arith_options.h" +#include "theory/arith/arith_state.h" #include "theory/arith/theory_arith.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 80cb62201..dd617f4a3 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -17,18 +17,16 @@ #ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H #define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H -#include #include -#include "theory/arith/arith_state.h" #include "theory/inference_id.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/inference_manager_buffered.h" namespace CVC4 { namespace theory { namespace arith { +class ArithState; class TheoryArith; /** diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index f0a3fbe25..42f8920c8 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -23,12 +23,9 @@ #include -#include #include #include -#include "expr/kind.h" -#include "expr/node_manager_attributes.h" #include "theory/arith/nl/poly_conversion.h" namespace CVC4 { diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 9302cb7f2..33267cb7a 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -23,8 +23,6 @@ #include -#include -#include #include namespace CVC4 { diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index f13e6f4a3..5ebe0c6b7 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/proof_checker.h" -#include "expr/proof_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 62d3c03ff..9f0799e7c 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -16,6 +16,9 @@ #ifdef CVC4_POLY_IMP +#include "theory/lazy_tree_proof_generator.h" +#include "theory/arith/nl/poly_conversion.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 72f0f766b..4709b8e59 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -23,18 +23,21 @@ #include -#include "context/cdlist.h" #include "expr/node.h" -#include "expr/proof_generator.h" #include "expr/proof_set.h" #include "theory/arith/nl/cad/cdcac_utils.h" -#include "theory/arith/nl/poly_conversion.h" #include "theory/lazy_tree_proof_generator.h" namespace CVC4 { + +class ProofGenerator; + namespace theory { namespace arith { namespace nl { + +struct VariableMapper; + namespace cad { /** diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 3a7d5159a..b83398cd6 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -23,6 +23,9 @@ #include "theory/arith/nl/cad/proof_checker.h" namespace CVC4 { + +class ProofNodeManager; + namespace theory { namespace arith { diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp index 452368640..9ec3b1fc1 100644 --- a/src/theory/arith/nl/ext/constraint.cpp +++ b/src/theory/arith/nl/ext/constraint.cpp @@ -16,6 +16,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/ext/monomial.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index 2f439f65e..d5ed7ccfd 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -20,13 +20,14 @@ #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl/ext/monomial.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { +class MonomialDb; + /** constraint information * * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index c7841748f..28373223b 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -21,6 +21,8 @@ #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_lemma_utils.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index f64fc8feb..7a0da42aa 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -20,6 +20,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index c8d27ec27..4c017d198 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -18,13 +18,17 @@ #include #include "expr/node.h" -#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { + +class CDProof; + namespace theory { namespace arith { namespace nl { +struct ExtState; + class FactoringCheck { public: diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 2c25a6e29..47cb5daec 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -20,6 +20,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" +#include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index 103e2725f..e7ba4d861 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -17,13 +17,14 @@ #include "expr/node.h" #include "theory/arith/nl/ext/constraint.h" -#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { +struct ExtState; + class MonomialBoundsCheck { public: diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 3f62d0afb..7f99b876d 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -19,6 +19,8 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index b964f00a4..a08554476 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -16,14 +16,16 @@ #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H #include "expr/node.h" +#include "theory/arith/nl/ext/monomial.h" #include "theory/theory_inference.h" -#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { +struct ExtState; + class MonomialCheck { public: diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 09954bf19..45f4160a0 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -19,6 +19,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index bee2fe405..030445737 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -17,13 +17,14 @@ #include "expr/node.h" #include "context/cdhashset.h" -#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { +struct ExtState; + class SplitZeroCheck { public: diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 254151283..64ea19f3c 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -19,6 +19,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index e0656789b..a771ae543 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -15,14 +15,17 @@ #ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H #define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H +#include + #include "expr/node.h" -#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { +struct ExtState; + class TangentPlaneCheck { public: diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index f1ad3df20..a3dc74ec8 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -20,6 +20,9 @@ namespace CVC4 { namespace theory { +namespace eq { +class EqualityEngine; +} namespace arith { namespace nl { diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index e484252f2..137d430c0 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -21,7 +21,6 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "theory/arith/nl/iand_utils.h" -#include "theory/arith/nl/nl_lemma_utils.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index 15ccab231..a84fcf978 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -17,7 +17,6 @@ #define CVC4__THEORY__ARITH__IAND_TABLE_H #include -#include #include "expr/node.h" diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index dae13318c..5467c64ce 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -20,6 +20,7 @@ #include "options/theory_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/theory_model.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index f907963c1..cd52cb159 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -21,7 +21,6 @@ #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl/nl_lemma_utils.h" namespace CVC4 { @@ -36,6 +35,7 @@ class TheoryModel; namespace arith { namespace nl { +class NlLemma; class NonlinearExtension; /** Non-linear model finder diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 38243823b..3f32e7075 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -24,6 +24,7 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 47d62e607..baa0f886c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "theory/arith/nl/cad_solver.h" +#include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "theory/arith/nl/ext/monomial_check.h" @@ -37,6 +38,7 @@ #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { @@ -46,6 +48,7 @@ namespace eq { namespace arith { class InferenceManager; +class TheoryArith; namespace nl { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 68d5a5f31..8b6f4484d 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -24,6 +24,8 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 76b14022f..484174d5f 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -16,12 +16,8 @@ #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H #include -#include -#include -#include #include "expr/node.h" -#include "theory/arith/nl/transcendental/transcendental_state.h" namespace CVC4 { namespace theory { @@ -29,6 +25,8 @@ namespace arith { namespace nl { namespace transcendental { +struct TranscendentalState; + /** Transcendental solver class * * This class implements model-based refinement schemes diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 0e5c09a2f..528e0bea2 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -23,6 +23,9 @@ #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 0b2e9d920..c628559fc 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -16,9 +16,6 @@ #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H #include -#include -#include -#include #include "expr/node.h" #include "theory/arith/nl/transcendental/transcendental_state.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index c6b929fec..f236b472a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -23,6 +23,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 438cc7047..593354794 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -16,6 +16,8 @@ #include "expr/proof.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 33994fa3a..cd5466e89 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -17,8 +17,7 @@ #include "expr/node.h" #include "expr/proof_set.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" @@ -26,7 +25,13 @@ namespace CVC4 { class CDProof; namespace theory { namespace arith { + +class InferenceManager; + namespace nl { + +class NlModel; + namespace transcendental { /** diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index bf8ec6c58..c3500e699 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -21,7 +21,6 @@ #define CVC4__THEORY__ARITH__NORMAL_FORM_H #include -#include #include "base/output.h" #include "expr/node.h" diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 6a9a130ca..c6f961129 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -17,6 +17,7 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" #include "expr/skolem_manager.h" +#include "expr/term_conversion_proof_generator.h" #include "options/arith_options.h" #include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 6dc535444..489974eac 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -17,12 +17,14 @@ #include #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" #include "theory/eager_proof_generator.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" namespace CVC4 { + +class TConvProofGenerator; + namespace theory { namespace arith { diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index ec682b948..af0fe37ec 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -21,11 +21,9 @@ #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H -#include #include #include "context/cdlist.h" -#include "context/context.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" @@ -35,6 +33,9 @@ #include "theory/arith/delta_rational.h" namespace CVC4 { +namespace context { +class Context; +} namespace theory { namespace arith { diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 8d2a94215..0745bdd61 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/proof_checker.h" -#include "expr/proof_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index c383c3a85..fc3d919c3 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -15,12 +15,14 @@ ** \todo document this file **/ +#include "theory/arith/simplex.h" + #include "base/output.h" #include "options/arith_options.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" -#include "theory/arith/simplex.h" - +#include "theory/arith/linear_equality.h" +#include "theory/arith/tableau.h" using namespace std; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index d1f891676..110093068 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -56,19 +56,20 @@ #include +#include "options/arith_options.h" #include "theory/arith/arithvar.h" -#include "theory/arith/delta_rational.h" -#include "theory/arith/linear_equality.h" #include "theory/arith/partial_model.h" -#include "theory/arith/tableau.h" #include "util/dense_map.h" #include "util/result.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace arith { class ErrorSet; +class LinearEqualityModule; +class Tableau; class SimplexDecisionProcedure { protected: diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index d47dba70f..79136e77c 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -23,6 +23,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" +#include "theory/arith/tableau.h" #include "util/statistics_registry.h" using namespace std; diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 5febe1bb0..d9d11dcc5 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -54,7 +54,9 @@ #pragma once +#include "theory/arith/linear_equality.h" #include "theory/arith/simplex.h" +#include "theory/arith/simplex_update.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 42cd16efc..937901c57 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -25,6 +25,8 @@ #include "theory/arith/nl/nonlinear_extension.h" #include "theory/arith/theory_arith_private.h" #include "theory/ext_theory.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1a41c9301..a208c9b10 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -22,7 +22,6 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/operator_elim.h" #include "theory/theory.h" namespace CVC4 { diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 583ff8dee..55a2472b3 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -18,22 +18,15 @@ #pragma once #include -#include #include #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" #include "context/cdqueue.h" -#include "context/context.h" #include "expr/kind.h" -#include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/proof_generator.h" -#include "options/arith_options.h" -#include "smt/logic_exception.h" -#include "smt_util/boolean_simplification.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" @@ -51,12 +44,8 @@ #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/arith/proof_checker.h" -#include "theory/arith/simplex.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/eager_proof_generator.h" -#include "theory/rewriter.h" -#include "theory/theory_model.h" #include "theory/trust_node.h" #include "theory/valuation.h" #include "util/dense_map.h" @@ -67,6 +56,10 @@ namespace CVC4 { namespace theory { + +class EagerProofGenerator; +class TheoryModel; + namespace arith { class BranchCutInfo; diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 5adb0e783..499f96bfb 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -18,14 +18,11 @@ #ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H #define CVC4__THEORY__ARRAYS__ARRAY_INFO_H -#include -#include #include #include #include "context/backtrackable.h" #include "context/cdlist.h" -#include "context/cdhashmap.h" #include "expr/node.h" #include "util/statistics_registry.h" diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index a8d1407a8..053502788 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/proof_checker.h" -#include "expr/proof_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 34a7a71b9..689e72a44 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -33,7 +33,6 @@ #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/proof_equality_engine.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 05c159b4b..b8a653bc3 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -20,7 +20,7 @@ #pragma once #include "expr/node.h" -#include "theory/theory.h" +#include "theory/theory_id.h" #include "context/cdlist.h" #include "context/cdhashset.h" #include "context/cdhashmap.h" 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 -#include - #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 -#include #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 -#include #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 - #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 { diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 1912d1ba6..b50ec34c7 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -21,8 +21,12 @@ #include #include "expr/node_algorithm.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" +#include "theory/eager_proof_generator.h" +#include "theory/theory.h" +#include "util/hash.h" #include "util/utility.h" using namespace std; diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index a2e4febad..ba8c5782d 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -19,7 +19,6 @@ #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H -#include #include #include #include @@ -30,15 +29,17 @@ #include "context/context.h" #include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "theory/eager_proof_generator.h" -#include "theory/theory.h" #include "theory/trust_node.h" -#include "util/hash.h" namespace CVC4 { + +class ProofGenerator; +class ProofNode; + namespace theory { + +class EagerProofGenerator; + namespace booleans { /** diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index b3d7c0f64..1d807fd90 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/proof_checker.h" -#include "expr/proof_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index a7ae4ac18..aaff82933 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -18,6 +18,7 @@ #include +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index f9a51e067..fa472b602 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -22,9 +22,13 @@ #include #include "expr/node.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" namespace CVC4 { + +class ProofNode; +class ProofNodeManager; + namespace theory { namespace booleans { diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 5878a4da5..bf84d543b 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -20,7 +20,6 @@ #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H -#include "theory/theory.h" #include "theory/theory_rewriter.h" namespace CVC4 { diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index aef88b539..84e64baa4 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -21,7 +21,6 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "theory/rewriter.h" #include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation #include diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index faafacfc5..6f7082191 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -16,6 +16,8 @@ #include "theory/builtin/type_enumerator.h" +#include "theory/builtin/theory_builtin_rewriter.h" + namespace CVC4 { namespace theory { namespace builtin { diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 25f750cf9..7b4b09f84 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -22,7 +22,6 @@ #include "expr/kind.h" #include "expr/type_node.h" #include "expr/uninterpreted_constant.h" -#include "theory/builtin/theory_builtin_rewriter.h" #include "theory/type_enumerator.h" #include "util/integer.h" diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index b4d4960ed..465a8eb65 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -20,6 +20,7 @@ #include "cvc4_private.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" +#include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 8f9deb2da..d3326f853 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -20,7 +20,6 @@ #define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H #include "theory/bv/bitblast/bitblaster.h" -#include "prop/sat_solver.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -35,6 +34,9 @@ class Cnf_Dat_t_; typedef Cnf_Dat_t_ Cnf_Dat_t; namespace CVC4 { +namespace prop { +class SatSolver; +} namespace theory { namespace bv { diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index f2b462b6b..d66b46505 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -19,11 +19,11 @@ #ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H #define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H +#include #include #include "theory/bv/bitblast/bitblaster.h" -#include "prop/cnf_stream.h" #include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 053ca6373..622369043 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -23,12 +23,14 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" -#include "prop/cnf_stream.h" -#include "prop/registrar.h" #include "prop/bv_sat_solver_notify.h" #include "theory/bv/abstraction.h" namespace CVC4 { +namespace prop { +class CnfStream; +class NullRegistrat; +} namespace theory { namespace bv { diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 28624a949..6a1d61a3b 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -19,9 +19,6 @@ #ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H #define CVC4__THEORY__BV__BV_EAGER_SOLVER_H -#include -#include - #include "expr/node.h" #include "theory/bv/bv_solver_lazy.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 39728c2ec..be5da70b2 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -19,16 +19,15 @@ #ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H #define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H -#include #include #include #include +#include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index dd1e7c9f7..a34ec98ad 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -19,8 +19,6 @@ #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H -#include - #include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 43fd90030..38d94ea27 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -28,6 +28,7 @@ #include "theory/bv/bv_quick_check.h" #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" using namespace CVC4::context; diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 9af95fa20..969ded528 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -21,7 +21,6 @@ #include #include -#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "theory/bv/bv_subtheory.h" #include "theory/ext_theory.h" diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 1b471dd68..aa3607a66 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -20,6 +20,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" using namespace std; diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index ab3c8d774..a19c18df8 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -15,6 +15,8 @@ **/ #include "theory/bv/slicer.h" +#include + #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0151791b7..4e7cfdd2a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -19,8 +19,6 @@ #ifndef CVC4__THEORY__BV__THEORY_BV_H #define CVC4__THEORY__BV__THEORY_BV_H -#include - #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index ee153a695..9ecc25973 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -21,13 +21,11 @@ #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H #include "theory/theory_rewriter.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace bv { -struct AllRewriteRules; typedef RewriteResponse (*RewriteFunction) (TNode, bool); class TheoryBVRewriter : public TheoryRewriter diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 2a2639505..c6c03e561 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -19,7 +19,6 @@ #pragma once #include -#include #include #include #include diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 4290ff989..567a16636 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -17,6 +17,7 @@ #include "expr/node_visitor.h" #include "prop/prop_engine.h" #include "theory/care_graph.h" +#include "theory/model_manager.h" #include "theory/theory_engine.h" namespace CVC4 { diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index ec2f7e336..160b56625 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -16,8 +16,11 @@ #include "expr/node_visitor.h" #include "theory/care_graph.h" +#include "theory/eager_proof_generator.h" #include "theory/ee_manager_distributed.h" +#include "theory/model_manager.h" #include "theory/model_manager_distributed.h" +#include "theory/shared_solver.h" #include "theory/shared_solver_distributed.h" #include "theory/theory_engine.h" diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 1e18ee558..a6331b406 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -20,10 +20,7 @@ #include #include -#include "theory/eager_proof_generator.h" #include "theory/ee_manager.h" -#include "theory/model_manager.h" -#include "theory/shared_solver.h" #include "theory/valuation.h" namespace CVC4 { @@ -32,6 +29,10 @@ class TheoryEngine; namespace theory { +class EagerProofGenerator; +class ModelManager; +class SharedSolver; + /** * Manager for doing theory combination. This class is responsible for: * (1) Initializing the various components of theory combination (equality diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index ad1947700..8ad927ce4 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -19,9 +19,7 @@ #ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H #define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H -#include "expr/node_manager_attributes.h" #include "theory/theory_rewriter.h" -#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 0c8db3eaf..b231e8fd4 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -15,7 +15,9 @@ #include "theory/datatypes/infer_proof_cons.h" #include "expr/proof.h" +#include "expr/proof_checker.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/model_manager.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index 11bc64095..eeb8214e2 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -17,14 +17,15 @@ #ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H #define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H -#include - +#include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" #include "theory/datatypes/inference.h" -#include "theory/theory_proof_step_buffer.h" namespace CVC4 { + +class ProofNodeManager; + namespace theory { namespace datatypes { diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index aed58fa2d..9c19608c1 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -17,10 +17,10 @@ #ifndef CVC4__THEORY__DATATYPES__INFERENCE_H #define CVC4__THEORY__DATATYPES__INFERENCE_H -#include "context/cdhashmap.h" #include "expr/node.h" -#include "theory/inference_manager_buffered.h" #include "theory/inference_id.h" +#include "theory/theory_inference.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 643ae669b..110747043 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -17,10 +17,8 @@ #ifndef CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H #define CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H -#include "context/cdhashmap.h" #include "expr/node.h" #include "theory/datatypes/infer_proof_cons.h" -#include "theory/datatypes/inference.h" #include "theory/inference_manager_buffered.h" namespace CVC4 { diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 206e97846..e75d1005f 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -22,11 +22,14 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "smt/logic_exception.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" using namespace CVC4; diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h index 16cd00cae..c35fc86ff 100644 --- a/src/theory/datatypes/sygus_extension.h +++ b/src/theory/datatypes/sygus_extension.h @@ -22,20 +22,18 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/cdo.h" #include "context/context.h" -#include "expr/dtype.h" #include "expr/node.h" #include "theory/datatypes/sygus_simple_sym.h" #include "theory/decision_manager.h" -#include "theory/quantifiers/sygus/sygus_explain.h" -#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers/term_database.h" namespace CVC4 { namespace theory { +namespace quantifiers { +class SynthConjecture; +} namespace datatypes { class InferenceManager; diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h index f1a77910f..713d1bdc2 100644 --- a/src/theory/datatypes/sygus_simple_sym.h +++ b/src/theory/datatypes/sygus_simple_sym.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H #define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H -#include #include "expr/dtype.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index bb6a84792..e20e3db9b 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -27,11 +27,15 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "smt/logic_exception.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/logic_info.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" #include "theory/type_enumerator.h" #include "theory/valuation.h" diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 27caad03c..95dccf2e5 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -31,6 +31,7 @@ #include "theory/datatypes/sygus_extension.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "util/hash.h" diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h index ef0b6f09d..74edde7f9 100644 --- a/src/theory/decision_strategy.h +++ b/src/theory/decision_strategy.h @@ -18,7 +18,6 @@ #ifndef CVC4__THEORY__DECISION_STRATEGY__H #define CVC4__THEORY__DECISION_STRATEGY__H -#include #include "context/cdo.h" #include "expr/node.h" #include "theory/valuation.h" diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index 2a6d28d56..7bbdc91d3 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -15,6 +15,7 @@ #include "theory/eager_proof_generator.h" #include "expr/proof.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 3fd8118ed..256dfeee9 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -20,10 +20,14 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" #include "theory/trust_node.h" namespace CVC4 { + +class ProofNode; +class ProofNodeManager; + namespace theory { /** diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 0ba62065b..3757f153a 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers_engine.h" #include "theory/shared_solver.h" #include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 3ae1a90de..26f3d9430 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -18,15 +18,17 @@ #ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H #define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H -#include #include #include "theory/ee_manager.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { +namespace eq { +class EqualityEngine; +} + /** * The (distributed) equality engine manager. This encapsulates an architecture * in which all theories maintain their own copy of an equality engine. diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 3240ec77b..0bdccab1b 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -19,7 +19,7 @@ #include "expr/node.h" #include "theory/output_channel.h" -#include "theory/theory.h" +#include "theory/theory_id.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -28,6 +28,8 @@ class TheoryEngine; namespace theory { +class Theory; + /** * An output channel for Theory that passes messages back to a TheoryEngine * for a given Theory. diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index ae54a8d3b..f2235c6bf 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -34,17 +34,18 @@ #define CVC4__THEORY__EXT_THEORY_H #include -#include #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "theory/theory.h" namespace CVC4 { namespace theory { +class OutputChannel; + /** * A callback class for ExtTheory below. This class is responsible for * determining how to apply context-dependent simplification. diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 60d229215..359079948 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -16,6 +16,8 @@ #include +#include "base/check.h" +#include "expr/node_builder.h" #include "theory/theory.h" // theory.h Only needed for the leaf test #include "util/floatingpoint.h" #include "util/floatingpoint_literal_symfpu.h" diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 8f02cc115..6623f308c 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -23,11 +23,9 @@ #ifndef CVC4__THEORY__FP__FP_CONVERTER_H #define CVC4__THEORY__FP__FP_CONVERTER_H -#include "base/check.h" #include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node.h" -#include "expr/node_builder.h" #include "expr/type_node.h" #include "theory/valuation.h" #include "util/bitvector.h" diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 5f6b9cf4d..73f7a2404 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -14,14 +14,11 @@ #include "cvc4_private.h" +#include + #ifndef CVC4__THEORY__INFERENCE_ID_H #define CVC4__THEORY__INFERENCE_ID_H -#include -#include - -#include "util/safe_print.h" - namespace CVC4 { namespace theory { diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index f1ef4e096..2772385d2 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H #define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H -#include "context/cdhashmap.h" #include "expr/node.h" #include "theory/theory_inference.h" #include "theory/theory_inference_manager.h" diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index f048e9e90..fe6d1cf62 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -23,7 +23,8 @@ #include #include -#include "expr/kind.h" + +#include "theory/theory_id.h" namespace CVC4 { diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index cecb4ccc5..b9057604e 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -18,6 +18,7 @@ #include "options/theory_options.h" #include "prop/prop_engine.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/theory_engine.h" diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index 69efe6e5f..1e4c39066 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -21,8 +21,6 @@ #include "theory/ee_manager.h" #include "theory/logic_info.h" -#include "theory/theory_model.h" -#include "theory/theory_model_builder.h" namespace CVC4 { @@ -30,6 +28,9 @@ class TheoryEngine; namespace theory { +class TheoryEngineModelBuilder; +class TheoryModel; + /** * A base class for managing models. Its main feature is to implement a * buildModel command. Overall, its behavior is specific to the kind of equality diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 3177e16ff..838cf0ad6 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -16,6 +16,7 @@ #include "theory/theory_engine.h" #include "theory/theory_model.h" +#include "theory/theory_model_builder.h" namespace CVC4 { namespace theory { diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h index f8cbf2322..d41b6fa3b 100644 --- a/src/theory/model_manager_distributed.h +++ b/src/theory/model_manager_distributed.h @@ -17,8 +17,6 @@ #ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H #define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H -#include - #include "theory/ee_manager.h" #include "theory/model_manager.h" diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 0441b1126..8c10a1348 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -19,11 +19,6 @@ #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H #define CVC4__THEORY__OUTPUT_CHANNEL_H -#include - -#include "expr/proof_node.h" -#include "smt/logic_exception.h" -#include "theory/interrupted.h" #include "theory/trust_node.h" #include "util/resource_manager.h" diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 7da13adcd..ca1d43b2f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 5260b4690..a5fb33a1f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -17,10 +17,8 @@ #ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H -#include -#include -#include #include + #include "theory/quantifiers/candidate_rewrite_filter.h" #include "theory/quantifiers/expr_miner.h" #include "theory/quantifiers/sygus_sampler.h" diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 7926116db..94c8b87e6 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -22,6 +22,7 @@ #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "util/random.h" using namespace std; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 6f529ea83..56bd14b33 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index dfc79d5a7..f1ed9fe00 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "util/random.h" using namespace CVC4; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index c6675745d..41f83269c 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 68f8e2e0d..91cb6e929 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/ematching/inst_match_generator_simple.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/instantiate.h" diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 153f2e6ba..ef9b8063f 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "expr/skolem_manager.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" @@ -23,12 +24,14 @@ #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/valuation.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 4211816b7..892f453ea 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -17,17 +17,13 @@ #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#include - #include "expr/node.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/valuation.h" namespace CVC4 { namespace theory { class QuantifiersEngine; +class Valuation; namespace quantifiers { class QuantifiersState; @@ -38,6 +34,7 @@ class QuantifiersRegistry; namespace inst { class IMGenerator; +class InstMatch; class InstMatchGenerator; /** A collection of nodes representing a trigger. * diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 57246202d..910dbc79b 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H #define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H -#include #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 3e70e5e69..2ecf3673f 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 8b8503022..878b4ddd3 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 121708a36..578554d79 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -18,15 +18,15 @@ #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "expr/node.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/quantifiers_state.h" #include "theory/theory_model_builder.h" namespace CVC4 { namespace theory { namespace quantifiers { +class FirstOrderModel; +class QuantifiersState; class QModelBuilder : public TheoryEngineModelBuilder { diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index b91a81641..92e5ec71b 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -17,15 +17,14 @@ #ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H #define CVC4__INST_STRATEGY_ENUMERATIVE_H -#include "context/context.h" -#include "context/context_mm.h" #include "theory/quantifiers/quant_module.h" -#include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { namespace quantifiers { +class RelevantDomain; + /** Enumerative instantiation * * This class implements enumerative instantiation described diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 8fbb58fe0..f6fb9ed75 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -14,12 +14,14 @@ #include "theory/quantifiers/instantiate.h" +#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" #include "expr/proof_node_manager.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "proof/proof_manager.h" +#include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" @@ -29,6 +31,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 CVC4::context; diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index a1e08e274..e55e677df 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -20,7 +20,6 @@ #include #include "context/cdhashset.h" -#include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof.h" #include "theory/quantifiers/inst_match_trie.h" @@ -28,6 +27,9 @@ #include "util/statistics_registry.h" namespace CVC4 { + +class LazyCDProof; + namespace theory { class QuantifiersEngine; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index d233dac62..17081bb7b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/term_database.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/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 8b68457bb..0b1f18f5b 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { 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 #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 #include -#include #include #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 #include #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 -#include #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 #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 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 -#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 -#include #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. diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index eeeb5385e..fa6d80085 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 588201fbf..61754ac32 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -18,7 +18,7 @@ #define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #include -#include +#include #include "context/cdhashmap.h" #include "context/cdhashset.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f72c970ba..401857206 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -31,6 +31,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index 9b26c3817..d38170563 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -14,6 +14,8 @@ #include "theory/relevance_manager.h" +#include + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index fc1e7dffa..5c3e2d38d 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "options/sets_options.h" #include "smt/logic_exception.h" +#include "theory/rewriter.h" #include "theory/sets/normal_form.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 8997d2b47..9e16bfb97 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -15,6 +15,7 @@ #include "theory/sets/inference_manager.h" #include "options/sets_options.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index e9529d4e0..3937a32b6 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -21,6 +21,7 @@ #include +#include "smt/logic_exception.h" #include "theory/sets/inference_manager.h" #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index fcdb7810f..91e008f80 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -15,6 +15,8 @@ #include "theory/shared_solver.h" #include "expr/node_visitor.h" +#include "theory/ee_setup_info.h" +#include "theory/logic_info.h" #include "theory/theory_engine.h" namespace CVC4 { diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h index d1c6f6c03..a4d08bd1b 100644 --- a/src/theory/shared_solver.h +++ b/src/theory/shared_solver.h @@ -18,19 +18,20 @@ #define CVC4__THEORY__SHARED_SOLVER__H #include "expr/node.h" -#include "expr/proof_node_manager.h" -#include "theory/ee_setup_info.h" -#include "theory/logic_info.h" #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" namespace CVC4 { +class LogicInfo; +class ProofNodeManager; class TheoryEngine; namespace theory { +struct EeSetupInfo; + /** * A base class for shared solver. The shared solver is the component of theory * engine that behaves like a theory solver, and whose purpose is to ensure the diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 9ad91ed33..cc99e75b4 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -18,7 +18,6 @@ #ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H #define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H -#include #include #include diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index c1e5b1fa8..822416da3 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -17,10 +17,9 @@ #ifndef CVC4__SORT_INFERENCE_H #define CVC4__SORT_INFERENCE_H -#include -#include -#include #include +#include + #include "expr/node.h" #include "expr/type_node.h" diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index c6bdad898..8a8abbf81 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -17,6 +17,7 @@ #include "expr/sequence.h" #include "options/strings_options.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 5dab55e65..b746f2961 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -18,6 +18,8 @@ #include "base/configuration.h" #include "options/strings_options.h" +#include "smt/logic_exception.h" +#include "theory/rewriter.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" #include "theory/strings/theory_strings_utils.h" diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index b6db6175f..a02566a41 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -14,6 +14,7 @@ #include "theory/strings/infer_proof_cons.h" +#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/strings_options.h" diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 0a938b236..f252196d8 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -19,6 +19,7 @@ #include #include "options/strings_options.h" +#include "smt/logic_exception.h" #include "theory/ext_theory.h" #include "theory/strings/theory_strings_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 1fd0169b0..456cd492b 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -14,6 +14,7 @@ #include "theory/strings/solver_state.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 9ea9042cd..3a3003ba9 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -17,6 +17,7 @@ #include "base/configuration.h" #include "options/quantifiers_options.h" +#include "smt/logic_exception.h" #include "theory/theory_engine.h" using namespace CVC4::theory; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8a5c40fd8..f34aebe8b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -32,12 +32,14 @@ #include "prop/prop_engine.h" #include "smt/dump.h" #include "smt/logic_exception.h" +#include "smt/output_manager.h" #include "theory/combination_care_graph.h" #include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers_engine.h" #include "theory/relevance_manager.h" #include "theory/rewriter.h" +#include "theory/shared_solver.h" #include "theory/theory.h" #include "theory/theory_engine_proof_generator.h" #include "theory/theory_id.h" @@ -48,7 +50,6 @@ using namespace std; -using namespace CVC4::preprocessing; using namespace CVC4::theory; namespace CVC4 { diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index 96ac5bef0..1833f1cac 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -20,7 +20,7 @@ #ifndef CVC4__THEORY__THEORY_ID_H #define CVC4__THEORY__THEORY_ID_H -#include +#include namespace CVC4 { namespace theory { diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index f970ce41e..68f70b740 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -16,6 +16,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" +#include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 6e9622e23..a599afa23 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "expr/proof_rule.h" #include "theory/inference_id.h" #include "theory/output_channel.h" #include "theory/trust_node.h" diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 10eb789b2..0c1ea7a7a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -19,6 +19,7 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "smt/smt_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 73b1d1d80..0d83fa42d 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -19,6 +19,7 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "theory/rewriter.h" #include "theory/uf/theory_uf_model.h" using namespace std; diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 6d76968ad..51f2155d3 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -16,6 +16,7 @@ #include "expr/lazy_proof.h" #include "expr/skolem_manager.h" +#include "smt/logic_exception.h" #include "theory/logic_info.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 810987a0c..d61f2d15b 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -18,6 +18,8 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "smt/logic_exception.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 91653785f..d701adfc4 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -19,11 +19,10 @@ #include "context/cdhashmap.h" #include "context/context.h" +#include "theory/decision_strategy.h" #include "theory/theory.h" #include "util/statistics_registry.h" -#include "theory/decision_manager.h" - namespace CVC4 { namespace theory { namespace uf { diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index bfcb829ff..59dc3943d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,9 +17,12 @@ #include "theory/uf/equality_engine.h" +#include "base/output.h" #include "options/smt_options.h" #include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" +#include "theory/rewriter.h" +#include "theory/uf/eq_proof.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7e297134e..b81a17dcf 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -22,18 +22,14 @@ #include #include -#include #include #include -#include "base/output.h" #include "context/cdhashmap.h" #include "context/cdo.h" #include "expr/kind_map.h" #include "expr/node.h" -#include "theory/rewriter.h" #include "theory/theory_id.h" -#include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine_iterator.h" #include "theory/uf/equality_engine_notify.h" #include "theory/uf/equality_engine_types.h" @@ -45,6 +41,7 @@ namespace eq { class EqClassesIterator; class EqClassIterator; +class EqProof; /** * Class for keeping an incremental congruence closure over a set of terms. It provides diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 0a7418e8d..7db887b56 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -15,7 +15,11 @@ #include "theory/uf/proof_equality_engine.h" #include "expr/lazy_proof_chain.h" +#include "expr/proof_node.h" +#include "expr/proof_node_manager.h" #include "theory/rewriter.h" +#include "theory/uf/eq_proof.h" +#include "theory/uf/equality_engine.h" #include "theory/uf/proof_checker.h" using namespace CVC4::kind; diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 1ce623683..adf8d2c18 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -17,7 +17,6 @@ #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H -#include #include #include "context/cdhashmap.h" @@ -25,15 +24,18 @@ #include "expr/buffered_proof_generator.h" #include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" #include "theory/eager_proof_generator.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { + +class ProofNode; +class ProofNodeManager; + namespace theory { namespace eq { +class EqualityEngine; + /** * A layer on top of an EqualityEngine. The goal of this class is manage the * use of an EqualityEngine object in such a way that the proper proofs are diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index caa15e69e..273e81740 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -26,6 +26,7 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "smt/logic_exception.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/cardinality_extension.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 7f136f9c1..be63be373 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -20,15 +20,12 @@ #ifndef CVC4__THEORY__UF__THEORY_UF_H #define CVC4__THEORY__UF__THEORY_UF_H -#include "context/cdo.h" #include "expr/node.h" #include "expr/node_trie.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" #include "theory/theory_state.h" -#include "theory/uf/equality_engine.h" #include "theory/uf/proof_checker.h" -#include "theory/uf/proof_equality_engine.h" #include "theory/uf/symmetry_breaker.h" #include "theory/uf/theory_uf_rewriter.h" diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 3613a9b22..393f1f705 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -18,6 +18,8 @@ #include "expr/attribute.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" using namespace CVC4::kind; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 3c5cc681b..62ec8204f 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -20,10 +20,12 @@ #include #include "expr/node.h" -#include "theory/theory_model.h" namespace CVC4 { namespace theory { + +class TheoryModel; + namespace uf { class UfModelTreeNode diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 54b71f9f8..e46f38a28 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "options/theory_options.h" #include "prop/prop_engine.h" +#include "theory/assertion.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 840da860f..860517451 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/node.h" #include "options/theory_options.h" -#include "theory/assertion.h" namespace CVC4 { @@ -32,6 +31,7 @@ class TheoryEngine; namespace theory { +struct Assertion; class TheoryModel; class SortInference; -- cgit v1.2.3