From bd33d20609999f6f847aeb63a42350aeb3041406 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 May 2021 13:51:09 -0500 Subject: Move proof utilities to src/proof/ (#6611) This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/. It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term"). --- src/theory/arith/nl/cad/proof_checker.h | 2 +- src/theory/arith/nl/cad/proof_generator.cpp | 2 +- src/theory/arith/nl/cad/proof_generator.h | 4 ++-- src/theory/arith/nl/ext/ext_state.cpp | 4 ++-- src/theory/arith/nl/ext/ext_state.h | 2 +- src/theory/arith/nl/ext/factoring_check.cpp | 4 ++-- src/theory/arith/nl/ext/monomial_bounds_check.cpp | 2 +- src/theory/arith/nl/ext/monomial_check.cpp | 6 +++--- src/theory/arith/nl/ext/proof_checker.h | 4 ++-- src/theory/arith/nl/ext/split_zero_check.cpp | 4 ++-- src/theory/arith/nl/ext/tangent_plane_check.cpp | 4 ++-- src/theory/arith/nl/transcendental/exponential_solver.cpp | 2 +- src/theory/arith/nl/transcendental/proof_checker.h | 4 ++-- src/theory/arith/nl/transcendental/sine_solver.cpp | 2 +- src/theory/arith/nl/transcendental/transcendental_state.cpp | 2 +- src/theory/arith/nl/transcendental/transcendental_state.h | 2 +- 16 files changed, 25 insertions(+), 25 deletions(-) (limited to 'src/theory/arith/nl') 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 #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 #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 #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" -- cgit v1.2.3