diff options
Diffstat (limited to 'src/theory/arith')
28 files changed, 43 insertions, 44 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index f343ce56a..33860d2d9 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -25,12 +25,12 @@ #include "base/cvc5config.h" #include "base/output.h" +#include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" #include "theory/arith/normal_form.h" -#include "theory/eager_proof_generator.h" #ifdef CVC5_USE_GLPK #include "theory/arith/partial_model.h" diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 2edc7b210..0c0a4959d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -18,8 +18,8 @@ #include "theory/arith/callbacks.h" -#include "expr/proof_node.h" #include "expr/skolem_manager.h" +#include "proof/proof_node.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 3d5e7270b..96272f939 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -19,8 +19,9 @@ #include "theory/arith/congruence_manager.h" #include "base/output.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "options/arith_options.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/constraint.h" @@ -29,7 +30,6 @@ #include "theory/rewriter.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" -#include "options/arith_options.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index e45b7bf29..8ada48cfe 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -24,11 +24,11 @@ #include "context/cdlist.h" #include "context/cdmaybe.h" #include "context/cdtrail_queue.h" +#include "proof/trust_node.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" #include "util/statistics_stats.h" diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 15dfe4791..d8fc1c578 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -22,16 +22,15 @@ #include <unordered_set> #include "base/output.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" #include "smt/smt_statistics_registry.h" -#include "theory/eager_proof_generator.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/rewriter.h" - using namespace std; using namespace cvc5::kind; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 0d3c96f89..fce071e6e 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -86,12 +86,12 @@ #include "context/cdlist.h" #include "context/cdqueue.h" #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index d7ce05b60..8cc544fc4 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index b0d785b2a..374a7e4ef 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -17,7 +17,7 @@ #ifdef CVC5_POLY_IMP -#include "theory/lazy_tree_proof_generator.h" +#include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" namespace cvc5 { diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index b493455a6..613db7565 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -25,9 +25,9 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/lazy_tree_proof_generator.h" +#include "proof/proof_set.h" #include "theory/arith/nl/cad/cdcac_utils.h" -#include "theory/lazy_tree_proof_generator.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 9ebd42d55..c1937797e 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -18,11 +18,11 @@ #include <vector> #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index b0a4fd859..7c2cc1b9b 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -19,7 +19,7 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/proof_set.h" #include "theory/arith/nl/ext/monomial.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index c4bba6ec8..d6b732eb9 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -16,12 +16,12 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "expr/node.h" -#include "expr/proof.h" #include "expr/skolem_manager.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 44f59c521..0deb2c99d 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -16,8 +16,8 @@ #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "expr/node.h" -#include "expr/proof.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 404916453..bf38bc8f0 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -16,12 +16,12 @@ #include "theory/arith/nl/ext/monomial_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 400126510..bf28cea59 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index ace7e0868..6d9faa356 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -16,11 +16,11 @@ #include "theory/arith/nl/ext/split_zero_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index a66f1396c..9efa9c0f2 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -16,11 +16,11 @@ #include "theory/arith/nl/ext/tangent_plane_check.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/ext/ext_state.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 11e2b9cc8..73279a782 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -20,8 +20,8 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 8675afe39..06359e62a 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 26d959878..6fdd4cc15 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -20,9 +20,9 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" +#include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index c0f5d23b2..db20713f1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -15,7 +15,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 74f005294..56cbec79a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -17,7 +17,7 @@ #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H #include "expr/node.h" -#include "expr/proof_set.h" +#include "proof/proof_set.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index f39be2c59..7b4e920fb 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -19,8 +19,8 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" -#include "expr/term_conversion_proof_generator.h" #include "options/arith_options.h" +#include "proof/conv_proof_generator.h" #include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 829601827..27a3d293e 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -19,7 +19,7 @@ #include "expr/node.h" #include "expr/skolem_manager.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 402656154..8fa9f21c1 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARITH__PROOF_CHECKER_H #include "expr/node.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1843ddb8a..5c4678cb4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -15,9 +15,9 @@ #include "theory/arith/theory_arith.h" -#include "expr/proof_checker.h" -#include "expr/proof_rule.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" +#include "proof/proof_rule.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/infer_bounds.h" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 911954a5a..d12553e90 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,13 +33,13 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_rule.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() #include "preprocessing/util/ite_utilities.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_rule.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e029e3c41..e3094ae88 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "proof/trust_node.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" @@ -47,7 +48,6 @@ #include "theory/arith/proof_checker.h" #include "theory/arith/soi_simplex.h" #include "theory/arith/theory_arith.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" |