diff options
Diffstat (limited to 'src/theory')
154 files changed, 300 insertions, 108 deletions
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 31eb8bb8f..26f51c8b8 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -14,6 +14,8 @@ #include "theory/arith/arith_preprocess.h" +#include "theory/arith/inference_manager.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 6c858d1eb..396395e1f 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -21,7 +21,6 @@ #define CVC4__THEORY__ARITH__ARITH_REWRITER_H #include "theory/arith/rewrites.h" -#include "theory/theory.h" #include "theory/theory_rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 72f8e49ff..61715df9b 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" using namespace std; diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 374b17d88..5d4bc9b1e 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" using namespace std; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 85af862fa..8cb249c46 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" #include "util/statistics_registry.h" using namespace std; diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 1bd4416e0..e001d98d4 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -52,6 +52,7 @@ #pragma once +#include "theory/arith/error_set.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index df3ba37f3..04165c289 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "theory/arith/nl/cad/projections.h" #include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/nl_model.h" namespace std { /** Generic streaming operator for std::vector. */ diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 4511d0c55..8736b7a08 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -32,12 +32,14 @@ #include "theory/arith/nl/cad/constraints.h" #include "theory/arith/nl/cad/proof_generator.h" #include "theory/arith/nl/cad/variable_ordering.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { + +class NlModel; + namespace cad { /** diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 74c0457a8..efc5c465a 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -14,15 +14,11 @@ #include "theory/arith/nl/cad_solver.h" -#ifdef CVC4_POLY_IMP -#include <poly/polyxx.h> -#endif - -#include "options/arith_options.h" #include "theory/inference_id.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" -#include "util/poly_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 21fbbab2e..b67d78f0d 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -17,17 +17,22 @@ #include <vector> +#include "context/context.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/cad/proof_checker.h" -#include "theory/arith/nl/nl_model.h" +#include "util/real_algebraic_number.h" namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { +class NlModel; + /** * A solver for nonlinear arithmetic that implements the CAD-based method * described in https://arxiv.org/pdf/2003.05633.pdf. diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 5da5319a1..7e77efb16 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -17,6 +17,7 @@ #include <vector> #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 863b3f879..285189ccc 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -19,15 +19,21 @@ #include "expr/node.h" #include "expr/proof_set.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { + +class CDProof; + namespace theory { namespace arith { + +class InferenceManager; + namespace nl { +class NlModel; + struct ExtState { ExtState(InferenceManager& im, diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 7b4d98037..09cfd7410 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -15,10 +15,12 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 5ae898bd2..ad6fd36b8 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -15,11 +15,13 @@ #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "expr/node.h" +#include "expr/proof.h" #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/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a3e56358b..d970bd95d 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/ext/monomial_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 51179826a..05908ecc7 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -16,6 +16,7 @@ #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H #include "expr/node.h" +#include "theory/theory_inference.h" #include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 1e9b444e3..5bcdb801d 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -15,9 +15,11 @@ #include "theory/arith/nl/ext/split_zero_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index e8730e496..0e7ad0999 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -16,6 +16,7 @@ #define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H #include "expr/node.h" +#include "context/cdhashset.h" #include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 3d646a684..2d04c2b5c 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -15,9 +15,11 @@ #include "theory/arith/nl/ext/tangent_plane_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 62e1fa904..ee12d17d6 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/arith_utilities.h" +#include "theory/uf/equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index a5b4e87bd..6487b48ec 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -18,7 +18,10 @@ #include "options/smt_options.h" #include "preprocessing/passes/bv_to_int.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" #include "util/iand.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index c854f3ab7..044a37abc 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -20,17 +20,20 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "theory/arith/arith_state.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/iand_utils.h" #include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { + +class ArithState; +class InferenceManager; + namespace nl { +class NlModel; + /** Integer and solver class * */ diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 17eb518a2..652f0eec7 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -19,6 +19,8 @@ #include "cvc4_private.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index a05defc0a..4c1de0196 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -16,7 +16,7 @@ #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H #define CVC4__THEORY__ARITH__IAND_TABLE_H -#include <tuple> +#include <map> #include <vector> #include "expr/node.h" diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index af86d69fd..7d698a221 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -20,6 +20,7 @@ #include "base/output.h" #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/poly_conversion.h" #include "theory/arith/normal_form.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 176549d8b..b9ecfc437 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -23,7 +23,6 @@ #include "expr/node.h" #include "theory/arith/bound_inference.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/icp/candidate.h" #include "theory/arith/nl/icp/contraction_origins.h" #include "theory/arith/nl/icp/intersection.h" @@ -32,6 +31,9 @@ namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { namespace icp { diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index aa8fcf543..b5fedb7eb 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -18,6 +18,8 @@ #include <iostream> +#include <poly/polyxx.h> + #include "base/check.h" #include "base/output.h" #include "theory/arith/nl/poly_conversion.h" diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index 0df6caf34..cdc166139 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -18,7 +18,9 @@ #include "util/real_algebraic_number.h" #ifdef CVC4_POLY_IMP -#include <poly/polyxx.h> +namespace poly { + class Interval; +} namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 5c4140430..9255d3349 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/theory_model.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index cd2d15563..4d5585545 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -19,15 +19,20 @@ #include <unordered_map> #include <vector> -#include "context/cdo.h" -#include "context/context.h" #include "expr/kind.h" #include "expr/node.h" #include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/theory_model.h" namespace CVC4 { + +namespace context { +class Context; +} + namespace theory { + +class TheoryModel; + namespace arith { namespace nl { diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index c46781e76..f269f1d69 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -18,10 +18,10 @@ #include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" -#include "options/theory_options.h" #include "theory/arith/arith_state.h" -#include "theory/arith/arith_utilities.h" #include "theory/arith/bound_inference.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index fba9e8e87..6a38021a0 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -21,10 +21,7 @@ #include <map> #include <vector> -#include "context/cdlist.h" -#include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" @@ -35,19 +32,25 @@ #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/icp/icp_solver.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { +namespace eq { + class EqualityEngine; +} namespace arith { + +class InferenceManager; + namespace nl { +class NlLemma; + /** Non-linear extension class * * This class implements model-based refinement schemes diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 5b7edb3ef..67cfd5807 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -20,9 +20,8 @@ #include "expr/node.h" #include "expr/node_manager_attributes.h" -#include "util/integer.h" +#include "theory/arith/bound_inference.h" #include "util/poly_util.h" -#include "util/rational.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 37d816179..102d2d6ae 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -23,15 +23,18 @@ #include <poly/polyxx.h> -#include <iostream> +#include <cstddef> +#include <map> +#include <utility> #include "expr/node.h" -#include "theory/arith/bound_inference.h" -#include "util/real_algebraic_number.h" namespace CVC4 { namespace theory { namespace arith { + +class BoundInference; + namespace nl { /** Bijective mapping between CVC4 variables and poly variables. */ diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index f869d83a4..fab4de35a 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -17,8 +17,6 @@ #ifndef CVC4__THEORY__ARITH__NL__STATS_H #define CVC4__THEORY__ARITH__NL__STATS_H -#include "expr/kind.h" -#include "theory/inference_id.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 526ae36f1..1f7b85b60 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -16,7 +16,6 @@ #define CVC4__THEORY__ARITH__NL__STRATEGY_H #include <iosfwd> -#include <map> #include <vector> namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 86b17376c..74766926b 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -19,9 +19,11 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof.h" #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/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 b874e1a4b..ddef4faf7 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -21,8 +21,6 @@ #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/transcendental_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index f5dc49da8..11852ac3a 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index da4b48fd6..a009df09b 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -21,8 +21,6 @@ #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/transcendental_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 375f1757e..f45b906bc 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index ccdc80e0f..0e1248f7c 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -16,12 +16,14 @@ #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H #include "expr/node.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { + +class NlModel; + namespace transcendental { class TaylorGenerator diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index e58da1aad..d1355c746 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -22,6 +22,7 @@ #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/transcendental/taylor_generator.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 8135ba1fb..343f303d1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -9,37 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/********************* */ -/*! \file transcendental_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Solving for handling transcendental functions. **/ #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H -#include <map> -#include <unordered_map> -#include <unordered_set> #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/exponential_solver.h" #include "theory/arith/nl/transcendental/sine_solver.h" #include "theory/arith/nl/transcendental/transcendental_state.h" @@ -47,7 +25,13 @@ namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { + +class NlModel; + namespace transcendental { /** Transcendental solver class diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 76c3d5357..ae8c1eea7 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -14,8 +14,10 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" +#include "expr/proof.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/nl/transcendental/taylor_generator.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 93ac4627a..d0678fb9a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -23,6 +23,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" namespace CVC4 { +class CDProof; namespace theory { namespace arith { namespace nl { diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 5c1b90663..d0a7f7fc4 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -19,6 +19,7 @@ #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" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 6740c8e1c..e34696cb5 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -57,7 +57,6 @@ #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/error_set.h" #include "theory/arith/linear_equality.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" @@ -68,6 +67,8 @@ namespace CVC4 { namespace theory { namespace arith { +class ErrorSet; + class SimplexDecisionProcedure { protected: typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 18169474d..796cd9412 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" #include "util/statistics_registry.h" using namespace std; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index eba84e339..f3344cbda 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -22,13 +22,15 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nonlinear_extension.h" #include "theory/arith/operator_elim.h" #include "theory/theory.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { +class NonlinearExtension; +} class TheoryArithPrivate; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 3b5f0dd82..40bd81795 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -65,6 +65,7 @@ #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 56e8fa4b0..818393cc7 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -43,6 +43,7 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/dio_solver.h" #include "theory/arith/dual_simplex.h" +#include "theory/arith/error_set.h" #include "theory/arith/fc_simplex.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/linear_equality.h" diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 96f2b02c3..b5bb9be14 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -16,6 +16,7 @@ #include "options/smt_options.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4dd7dcafd..49f530e32 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -28,8 +28,10 @@ #include "smt/smt_statistics_registry.h" #include "theory/arrays/skolem_cache.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/decision_manager.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" using namespace std; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7e4f0e36c..e02c30296 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -29,7 +29,9 @@ #include "theory/arrays/inference_manager.h" #include "theory/arrays/proof_checker.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/decision_strategy.h" #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" diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 76c001ba2..c39e0198b 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -17,6 +17,7 @@ #include "theory/bags/bag_solver.h" #include "theory/bags/inference_generator.h" +#include "theory/uf/equality_engine_iterator.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 48cd9c419..d9f736c4f 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -19,6 +19,7 @@ #include "theory/bags/rewrites.h" #include "theory/rewriter.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 726160d83..f00bffb2e 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -21,6 +21,7 @@ #include <vector> #include "expr/node_algorithm.h" +#include "expr/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" #include "util/utility.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 90de1d8da..b5ad16b1c 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -25,6 +25,7 @@ #include "theory/booleans/theory_bool_rewriter.h" #include "theory/substitutions.h" #include "theory/theory.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/hash.h" diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp index 551c18612..4c7311945 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 38e4b3aa6..d9adf06fb 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -24,6 +24,7 @@ #include <unordered_map> #include <unordered_set> +#include "context/cdhashset.h" #include "context/cdqueue.h" #include "context/context.h" #include "theory/theory.h" diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index d8d8dbed7..3cadac621 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -30,6 +30,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4::theory::bv::utils; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 55a0ff46b..47974fc03 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,6 +21,7 @@ #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/ee_setup_info.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 2aa722e48..fafde0601 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h index 40553f01b..6793d6e90 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -21,8 +21,8 @@ #include <set> -#include "expr/kind.h" // For TheoryId. #include "expr/node.h" +#include "theory/theory_id.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 4dbf26062..5334e76df 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "options/datatypes_options.h" diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 14dc9fbf1..ea5928a42 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/infer_proof_cons.h" +#include "expr/proof.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 9702a5584..4c7773e29 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -17,7 +17,11 @@ #include "expr/dtype.h" #include "options/datatypes_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/eager_proof_generator.h" +#include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" +#include "theory/trust_substitutions.h" using namespace CVC4::kind; diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index ba46d2a42..610383ff1 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -25,6 +25,9 @@ namespace CVC4 { namespace theory { + +class EagerProofGenerator; + namespace datatypes { /** diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 6bfa20151..9a9f7cb7b 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/proof_checker.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 60bf36139..6169d3752 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "smt/smt_engine.h" diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 7efd2a9ac..8622ec483 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -15,6 +15,7 @@ #include "theory/datatypes/sygus_extension.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_manager.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index b7ab9b4f7..a2530f4ac 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/sygus_simple_sym.h" +#include "expr/dtype_cons.h" #include "theory/quantifiers/term_util.h" using namespace std; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 45787ee04..9105cdfd6 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -19,7 +19,9 @@ #include "base/check.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 2834b86ba..73aef4dd7 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/type_matcher.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index c55b4a14f..1247ecca5 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 079430342..25bdd2f94 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -14,6 +14,7 @@ ** Enumerators for datatypes. **/ +#include "expr/dtype_cons.h" #include "theory/datatypes/type_enumerator.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 7b4936a53..030d9a497 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -20,7 +20,9 @@ #include "base/check.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/substitutions.h" using namespace std; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 6df991ef9..e9b59fdae 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -22,9 +22,12 @@ #include <unordered_set> #include <vector> +#include "base/configuration.h" #include "options/fp_options.h" +#include "smt/logic_exception.h" #include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" +#include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory_model.h" diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 1a745b3a3..bd6e70ff1 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -23,9 +23,11 @@ #include <string> #include <utility> +#include "context/cdhashset.h" #include "context/cdo.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" namespace CVC4 { diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 0c143f265..3e4b921db 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -16,6 +16,7 @@ #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" using namespace CVC4::kind; diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index bb2bf937a..24570f9a6 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/fmf/model_builder.h" #include "theory/theory_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 16f0f3957..7a584c146 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0d1a51a30..bda4e31fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -18,6 +18,8 @@ #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" +#include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index e782a1b6f..0c416fdf4 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index eb02eb19e..c553a1239 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -14,11 +14,13 @@ #include "theory/quantifiers/ematching/candidate_generator.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 5df350fe5..1875dc631 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -16,7 +16,10 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index ce535d5e8..07cb74a83 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/ematching/inst_match_generator.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/ematching/candidate_generator.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 5c5dcfef1..dfe2e3ae9 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -15,7 +15,9 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine_iterator.h" using namespace CVC4::kind; 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 66433ba78..00a233d6a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/term_util.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 6b2f1b7f8..f9692bd76 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -14,6 +14,11 @@ #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/trigger_term_info.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index e7635f200..9768e7f2c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/quant_relevance.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" #include "util/random.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 14913bdc1..c2b5f78ae 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index a64dc4424..6564f407e 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -18,6 +18,7 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 79bd5c1dd..9d8b64e25 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -22,10 +22,12 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #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/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" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 8448fe810..17baf5000 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -13,7 +13,9 @@ **/ #include "theory/quantifiers/ematching/var_match_generator.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 759d3e69f..6ce561b2d 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -19,6 +19,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace std; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 700ae2c64..fb0505bae 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -16,10 +16,12 @@ #include "theory/quantifiers/fmf/bounded_integers.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 9d4a414e9..3e7466ed2 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -23,6 +23,7 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "expr/attribute.h" +#include "theory/decision_strategy.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 96e8a40be..c248167cb 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 993fad90a..ab5dcb166 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine_iterator.h" using namespace CVC4::context; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 2eb99a774..3164ff5ce 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/instantiate.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" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index a0b776819..37cc49f17 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -19,6 +19,8 @@ #include <map> +#include "context/cdhashset.h" +#include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof.h" #include "theory/quantifiers/inst_match_trie.h" diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index f89f9f0ea..cf37bc746 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_conflict_find.h" +#include "base/configuration.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "options/theory_options.h" diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index 5bb50c926..58716f809 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index a0b780836..e3bd2072f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -13,6 +13,9 @@ **/ #include "theory/quantifiers/quant_split.h" + +#include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2126bf1f0..ec7e7fd2c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -16,6 +16,7 @@ #include "expr/bound_var_manager.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" @@ -27,6 +28,7 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace std; diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 0bcca266e..55f680897 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "options/quantifiers_options.h" +#include "theory/uf/equality_engine_iterator.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 3cef2884f..b97a8e539 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index a9ac7d0d2..42729ef5b 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/skolemize.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" 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 b296a4421..77714f87d 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/command.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index db2a972d5..a58ce894d 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/cegis_core_connective.h" +#include "expr/dtype_cons.h" #include "options/base_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 9db77fd95..5da6f2121 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -19,6 +19,7 @@ #include <map> #include <vector> +#include "theory/decision_strategy.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 360476399..f6e34e8a1 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" +#include "expr/dtype_cons.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index e0159049b..2fa6009d3 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 882c9ca77..90765284a 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -14,10 +14,12 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 0f9d2ccd1..5965e9430 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_explain.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 538d80e44..98a177f86 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -16,6 +16,7 @@ #include <stack> +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 7d757ca98..953eac7b0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_norm.h" +#include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" #include "smt/smt_engine.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 6e36222b6..cc29e7b0a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 1e67bb8cc..a2675dd96 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -19,6 +19,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 81120da28..8b741b6d7 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "api/cvc4cpp.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index f0d3e47b6..1c0cfcc55 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -15,12 +15,14 @@ #include "theory/quantifiers/sygus/sygus_unif_strat.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_unif.h" #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/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0fcba916b..56691c7c1 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/synth_conjecture.h" +#include "base/configuration.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index bc5cd1fda..f393601ad 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "base/check.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" #include "options/datatypes_options.h" @@ -23,6 +24,8 @@ #include "theory/arith/arith_msum.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index d44d2eda8..8e29ab9d6 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -16,6 +16,7 @@ #include "base/check.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 9fdf0aa7f..a46d4e445 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -18,11 +18,14 @@ #include <unordered_set> #include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 3116f35e6..17cb1c9a1 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -21,6 +21,7 @@ #include <unordered_set> #include "context/cdhashset.h" +#include "theory/decision_strategy.h" #include "theory/quantifiers/quant_module.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 62eef124a..a72054f6d 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus_sampler.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cb5c7dfec..281d5c844 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -21,6 +21,8 @@ #include "options/uf_options.h" #include "theory/quantifiers/ematching/trigger_term_info.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/theory_engine.h" diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9a031f99c..b121b2c46 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -20,6 +20,8 @@ #include <map> #include <unordered_set> +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/attribute.h" #include "expr/node_trie.h" #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 9cbf2cf53..33f74c7c4 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers_engine.h" #include "theory/strings/word.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 036b63b27..98bb9bec3 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -18,7 +18,6 @@ #define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H #include <map> -#include <unordered_set> #include "expr/attribute.h" #include "expr/node.h" @@ -55,8 +54,6 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; namespace quantifiers { -class TermDatabase; - // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. class TermUtil { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7046a8ef0..79422b418 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -20,10 +20,22 @@ #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/equality_query.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/full_model_check.h" +#include "theory/quantifiers/fmf/model_builder.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/skolemize.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f464b24d4..d08e32f6e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -20,23 +20,11 @@ #include <map> #include <unordered_map> +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" -#include "expr/attribute.h" -#include "theory/quantifiers/ematching/trigger_trie.h" -#include "theory/quantifiers/equality_query.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/model_builder.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_inference_manager.h" -#include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -46,9 +34,24 @@ class TheoryEngine; namespace theory { class DecisionManager; +class QuantifiersModule; +class RepSetIterator; +namespace inst { +class TriggerTrie; +} namespace quantifiers { +class EqualityQueryQuantifiersEngine; +class FirstOrderModel; +class Instantiate; +class QModelBuilder; +class QuantifiersInferenceManager; class QuantifiersModules; +class QuantifiersState; +class Skolemize; +class TermDb; +class TermDbSygus; +class TermEnumeration; } // TODO: organize this more/review this, github issue #1163 diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index be26510c6..fc98e6198 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/rewriter.h" +#include "expr/term_conversion_proof_generator.h" #include "options/theory_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 572662483..f5c1348ad 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,20 +19,21 @@ #pragma once #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" #include "theory/theory_rewriter.h" -#include "theory/trust_node.h" -#include "util/unsafe_interrupt_exception.h" namespace CVC4 { + +class TConvProofGenerator; +class ProofNodeManager; + namespace theory { +class TrustNode; + namespace builtin { class BuiltinProofRuleChecker; } -class RewriterInitializer; - /** * The rewrite environment holds everything that the individual rewrites have * access to. diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 2a409a304..0a8039ed1 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -24,6 +24,7 @@ #include "options/sep_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b2cd6bf45..198273993 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -23,9 +23,11 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/cdqueue.h" +#include "theory/decision_strategy.h" #include "theory/inference_manager_buffered.h" #include "theory/sep/theory_sep_rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 13ee672db..0d832b646 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -18,6 +18,7 @@ #define SRC_THEORY_SETS_RELS_UTILS_H_ #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index e06a8cb52..5c6300059 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -20,6 +20,7 @@ #include "theory/sets/theory_sets_private.h" #include "theory/sets/theory_sets_rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4::kind; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 1e4473d6f..eb802af4a 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/sets/theory_sets_rewriter.h" #include "expr/attribute.h" +#include "expr/dtype_cons.h" #include "options/sets_options.h" #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 5446f67be..642a4d4ae 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" +#include "base/configuration.h" #include "options/strings_options.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 770991286..620cca185 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -15,6 +15,7 @@ #include "theory/strings/regexp_elim.h" +#include "expr/proof_node_manager.h" #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0157a47f0..bd95933a5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -19,6 +19,7 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "smt/logic_exception.h" +#include "theory/decision_manager.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 82463367e..a725f4d88 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -15,6 +15,7 @@ #include "theory/term_registration_visitor.h" +#include "base/configuration.h" #include "options/quantifiers_options.h" #include "theory/theory_engine.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index fef3fdc67..19fc91312 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -26,10 +26,16 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/ee_setup_info.h" #include "theory/ext_theory.h" +#include "theory/output_channel.h" #include "theory/quantifiers_engine.h" #include "theory/substitutions.h" +#include "theory/theory_inference_manager.h" +#include "theory/theory_model.h" #include "theory/theory_rewriter.h" +#include "theory/theory_state.h" +#include "theory/trust_substitutions.h" using namespace std; diff --git a/src/theory/theory.h b/src/theory/theory.h index fa26ab65e..5f4698e56 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -20,49 +20,39 @@ #define CVC4__THEORY__THEORY_H #include <iosfwd> -#include <map> #include <set> #include <string> #include <unordered_set> -#include "context/cdhashset.h" #include "context/cdlist.h" #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "options/options.h" #include "options/theory_options.h" -#include "smt/logic_request.h" #include "theory/assertion.h" #include "theory/care_graph.h" -#include "theory/decision_manager.h" -#include "theory/ee_setup_info.h" #include "theory/logic_info.h" -#include "theory/output_channel.h" #include "theory/theory_id.h" -#include "theory/theory_inference_manager.h" -#include "theory/theory_rewriter.h" -#include "theory/theory_state.h" #include "theory/trust_node.h" -#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { -class TheoryEngine; class ProofNodeManager; +class TheoryEngine; namespace theory { +class DecisionManager; +struct EeSetupInfo; +class OutputChannel; class QuantifiersEngine; +class TheoryInferenceManager; class TheoryModel; -class SubstitutionMap; class TheoryRewriter; - -namespace rrinst { - class CandidateGenerator; -}/* CVC4::theory::rrinst namespace */ +class TheoryState; +class TrustSubstitutionMap; namespace eq { class EqualityEngine; diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 53a812653..810f31ce5 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,8 +15,11 @@ #include "theory/theory_inference_manager.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index d3a317cbc..61b105dac 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -23,9 +23,8 @@ #include "expr/node.h" #include "theory/inference_id.h" #include "theory/output_channel.h" -#include "theory/theory_state.h" #include "theory/trust_node.h" -#include "theory/uf/proof_equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -34,8 +33,10 @@ class ProofNodeManager; namespace theory { class Theory; +class TheoryState; namespace eq { class EqualityEngine; +class ProofEqEngine; } /** diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 9604dc72b..89f53acb8 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -14,6 +14,7 @@ #include "theory/theory_model_builder.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index a0586bd0c..d4d2a78a5 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -18,11 +18,11 @@ #define CVC4__THEORY__TRUST_NODE_H #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { class ProofGenerator; +class ProofNode; namespace theory { diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 7ab43091a..58d5f4924 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -15,6 +15,7 @@ #include "theory/uf/eq_proof.h" +#include "base/configuration.h" #include "expr/proof.h" #include "options/uf_options.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 497e394c7..49e19c15f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -25,6 +25,7 @@ #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" |