diff options
Diffstat (limited to 'src/theory/arith')
52 files changed, 113 insertions, 65 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" |