diff options
Diffstat (limited to 'src/theory')
95 files changed, 142 insertions, 1556 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" diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 93feb0a53..9b219c9b7 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H #include "expr/node.h" -#include "expr/proof_rule.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_rule.h" #include "theory/theory_inference_manager.h" namespace cvc5 { diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index 9064dbfca..0b7bef163 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__ARRAYS__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/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9b5676d65..0bdccfd17 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -20,9 +20,9 @@ #include "expr/kind.h" #include "expr/node_algorithm.h" -#include "expr/proof_checker.h" #include "options/arrays_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/arrays/skolem_cache.h" diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index d5917f91c..c2aa9eb1e 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -15,7 +15,7 @@ #include "theory/bags/theory_bags.h" -#include "expr/proof_checker.h" +#include "proof/proof_checker.h" #include "smt/logic_exception.h" #include "theory/bags/normal_form.h" #include "theory/rewriter.h" diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 7920f5b7f..2fa2890c2 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -20,10 +20,10 @@ #include <vector> #include "expr/node_algorithm.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" -#include "theory/eager_proof_generator.h" #include "theory/theory.h" #include "util/hash.h" #include "util/utility.h" diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 1d4f6e9ee..74e1a7cd8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -26,9 +26,9 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" -#include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof_chain.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index 47a1ce633..114ab2e9b 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__BOOLEANS__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/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index d1f8bb854..f7e788e9a 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -17,8 +17,8 @@ #include <sstream> -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index 624a17f2f..0bed57078 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -21,7 +21,7 @@ #include <memory> #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" namespace cvc5 { diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index bac2be70c..3aac5ecfb 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,7 +18,7 @@ #include <stack> #include <vector> -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index dd6bf82e7..892fc7a4b 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BUILTIN__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" #include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index c5bd77e36..80c5dba3d 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -16,7 +16,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 6082a7128..a55adaace 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -16,8 +16,8 @@ #include <unordered_set> -#include "expr/term_conversion_proof_generator.h" #include "options/proof_options.h" +#include "proof/conv_proof_generator.h" #include "theory/theory_model.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 3da08f868..31d9443c8 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -21,12 +21,12 @@ #include <unordered_map> #include "context/cdqueue.h" +#include "proof/eager_proof_generator.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/bv/bv_solver.h" #include "theory/bv/proof_checker.h" -#include "theory/eager_proof_generator.h" namespace cvc5 { diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp index 3faad29a9..a16bf7eb8 100644 --- a/src/theory/bv/bv_solver_simple.cpp +++ b/src/theory/bv/bv_solver_simple.cpp @@ -15,7 +15,7 @@ #include "theory/bv/bv_solver_simple.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h index 674678ff8..c89dd359c 100644 --- a/src/theory/bv/proof_checker.h +++ b/src/theory/bv/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__BV__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" #include "theory/bv/bitblast/simple_bitblaster.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c5ab08f0c..22b05b026 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -15,9 +15,9 @@ #include "theory/bv/theory_bv.h" -#include "expr/proof_checker.h" #include "options/bv_options.h" #include "options/smt_options.h" +#include "proof/proof_checker.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_lazy.h" diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 33300ead8..2b35fb97d 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -16,8 +16,8 @@ #include "theory/combination_engine.h" #include "expr/node_visitor.h" +#include "proof/eager_proof_generator.h" #include "theory/care_graph.h" -#include "theory/eager_proof_generator.h" #include "theory/ee_manager_distributed.h" #include "theory/model_manager.h" #include "theory/model_manager_distributed.h" diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 5ab8a563f..19f396a56 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -15,8 +15,8 @@ #include "theory/datatypes/infer_proof_cons.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h index f8e7eea09..6c1663a09 100644 --- a/src/theory/datatypes/infer_proof_cons.h +++ b/src/theory/datatypes/infer_proof_cons.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/proof_generator.h" +#include "proof/proof_generator.h" #include "theory/datatypes/inference.h" namespace cvc5 { diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index db1d2b4b0..2dac0d7aa 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -19,9 +19,9 @@ #define CVC5__THEORY__DATATYPES__INFERENCE_H #include "expr/node.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/theory_inference.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 393813590..014255a7c 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -17,8 +17,8 @@ #include "expr/dtype.h" #include "options/datatypes_options.h" +#include "proof/eager_proof_generator.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" diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h index 76fcee411..5949441d8 100644 --- a/src/theory/datatypes/proof_checker.h +++ b/src/theory/datatypes/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__DATATYPES__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/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f9d08dfc2..dc57e4165 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -21,12 +21,12 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp deleted file mode 100644 index c9a8823aa..000000000 --- a/src/theory/eager_proof_generator.cpp +++ /dev/null @@ -1,158 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Alex Ozdemir - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of the abstract proof generator class. - */ - -#include "theory/eager_proof_generator.h" - -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { -namespace theory { - -EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, - context::Context* c, - std::string name) - : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c) -{ -} - -void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf) -{ - // pf should prove f - Assert(pf->getResult() == f) - << "EagerProofGenerator::setProofFor: unexpected result" << std::endl - << "Expected: " << f << std::endl - << "Actual: " << pf->getResult() << std::endl; - d_proofs[f] = pf; -} -void EagerProofGenerator::setProofForConflict(Node conf, - std::shared_ptr<ProofNode> pf) -{ - // Normalize based on key - Node ckey = TrustNode::getConflictProven(conf); - setProofFor(ckey, pf); -} - -void EagerProofGenerator::setProofForLemma(Node lem, - std::shared_ptr<ProofNode> pf) -{ - // Normalize based on key - Node lkey = TrustNode::getLemmaProven(lem); - setProofFor(lkey, pf); -} - -void EagerProofGenerator::setProofForPropExp(TNode lit, - Node exp, - std::shared_ptr<ProofNode> pf) -{ - // Normalize based on key - Node pekey = TrustNode::getPropExpProven(lit, exp); - setProofFor(pekey, pf); -} - -std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f) -{ - NodeProofNodeMap::iterator it = d_proofs.find(f); - if (it == d_proofs.end()) - { - return nullptr; - } - return (*it).second; -} - -bool EagerProofGenerator::hasProofFor(Node f) -{ - return d_proofs.find(f) != d_proofs.end(); -} - -TrustNode EagerProofGenerator::mkTrustNode(Node n, - std::shared_ptr<ProofNode> pf, - bool isConflict) -{ - if (pf == nullptr) - { - return TrustNode::null(); - } - if (isConflict) - { - // this shouldnt modify the key - setProofForConflict(n, pf); - // we can now return the trust node - return TrustNode::mkTrustConflict(n, this); - } - // this shouldnt modify the key - setProofForLemma(n, pf); - // we can now return the trust node - return TrustNode::mkTrustLemma(n, this); -} - -TrustNode EagerProofGenerator::mkTrustNode(Node conc, - PfRule id, - const std::vector<Node>& exp, - const std::vector<Node>& args, - bool isConflict) -{ - // if no children, its easy - if (exp.empty()) - { - std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc); - return mkTrustNode(conc, pf, isConflict); - } - // otherwise, we use CDProof + SCOPE - CDProof cdp(d_pnm); - cdp.addStep(conc, id, exp, args); - std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc); - // We use mkNode instead of mkScope, since there is no reason to check - // whether the free assumptions of pf are in exp, since they are by the - // construction above. - std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp); - return mkTrustNode(pfs->getResult(), pfs, isConflict); -} - -TrustNode EagerProofGenerator::mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf) -{ - if (pf == nullptr) - { - return TrustNode::null(); - } - Node eq = a.eqNode(b); - setProofFor(eq, pf); - return TrustNode::mkTrustRewrite(a, b, this); -} - -TrustNode EagerProofGenerator::mkTrustedPropagation( - Node n, Node exp, std::shared_ptr<ProofNode> pf) -{ - if (pf == nullptr) - { - return TrustNode::null(); - } - setProofForPropExp(n, exp, pf); - return TrustNode::mkTrustPropExp(n, exp, this); -} - -TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) -{ - // make the lemma - Node lem = f.orNode(f.notNode()); - return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false); -} - -std::string EagerProofGenerator::identify() const { return d_name; } - -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h deleted file mode 100644 index c0b368e6e..000000000 --- a/src/theory/eager_proof_generator.h +++ /dev/null @@ -1,198 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Alex Ozdemir, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The eager proof generator class. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H -#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H - -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_rule.h" -#include "theory/trust_node.h" - -namespace cvc5 { - -class ProofNode; -class ProofNodeManager; - -namespace theory { - -/** - * An eager proof generator, with explicit proof caching. - * - * The intended use of this class is to store proofs for lemmas and conflicts - * at the time they are sent out on the ProofOutputChannel. This means that the - * getProofForConflict and getProofForLemma methods are lookups in a - * (user-context depedent) map, the field d_proofs below. - * - * In detail, the method setProofForConflict(conf, pf) should be called prior to - * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator. - * Similarly for setProofForLemma. - * - * The intended usage of this class in combination with OutputChannel is - * the following: - * //----------------------------------------------------------- - * class MyEagerProofGenerator : public EagerProofGenerator - * { - * public: - * TrustNode getProvenConflictByMethodX(...) - * { - * // construct a conflict - * Node conf = [construct conflict]; - * // construct a proof for conf - * std::shared_ptr<ProofNode> pf = [construct the proof for conf]; - * // wrap the conflict in a trust node - * return mkTrustNode(conf,pf); - * } - * }; - * // [1] Make objects given user context u and output channel out. - * - * MyEagerProofGenerator epg(u); - * OutputChannel out; - * - * // [2] Assume epg realizes there is a conflict. We have it store the proof - * // internally and return the conflict node paired with epg. - * - * TrustNode pconf = epg.getProvenConflictByMethodX(...); - * - * // [3] Send the conflict on the output channel. - * - * out.trustedConflict(pconf); - * - * // [4] The trust node has information about what is proven and who can - * // prove it, where this association is valid in the remainder of the user - * // context. - * - * Node conf = pconf.getProven(); - * ProofGenerator * pg = pconf.getGenerator(); - * std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf); - * //----------------------------------------------------------- - * In other words, the proof generator epg is responsible for creating and - * storing the proof internally, and the proof output channel is responsible for - * maintaining the map that epg is who to ask for the proof of the conflict. - */ -class EagerProofGenerator : public ProofGenerator -{ - typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; - - public: - EagerProofGenerator(ProofNodeManager* pnm, - context::Context* c = nullptr, - std::string name = "EagerProofGenerator"); - ~EagerProofGenerator() {} - /** Get the proof for formula f. */ - std::shared_ptr<ProofNode> getProofFor(Node f) override; - /** Can we give the proof for formula f? */ - bool hasProofFor(Node f) override; - /** - * Set proof for fact f, called when pf is a proof of f. - * - * @param f The fact proven by pf, - * @param pf The proof to store in this class. - */ - void setProofFor(Node f, std::shared_ptr<ProofNode> pf); - /** - * Make trust node: wrap n in a trust node with this generator, and have it - * store the proof pf to lemma or conflict n. - * - * @param n The proven node, - * @param pf The proof of n, - * @param isConflict Whether the returned trust node is a conflict (otherwise - * it is a lemma), - * @return The trust node corresponding to the fact that this generator has - * a proof of n. - */ - TrustNode mkTrustNode(Node n, - std::shared_ptr<ProofNode> pf, - bool isConflict = false); - /** - * Make trust node from a single step proof. This is a convenience function - * that avoids the need to explictly construct ProofNode by the caller. - * - * @param conc The conclusion of the rule, - * @param id The rule of the proof concluding conc - * @param exp The explanation (premises) to the proof concluding conc, - * @param args The arguments to the proof concluding conc, - * @param isConflict Whether the returned trust node is a conflict (otherwise - * it is a lemma), - * @return The trust node corresponding to the fact that this generator has - * a proof of (exp => conc), or of conc if exp is empty. - */ - TrustNode mkTrustNode(Node conc, - PfRule id, - const std::vector<Node>& exp, - const std::vector<Node>& args, - bool isConflict = false); - /** - * Make trust node: wrap `exp => n` in a trust node with this generator, and - * have it store the proof `pf` too. - * - * @param n The implication - * @param exp A conjunction of literals that imply it - * @param pf The proof of exp => n, - * @return The trust node corresponding to the fact that this generator has - * a proof of exp => n. - */ - TrustNode mkTrustedPropagation(Node n, - Node exp, - std::shared_ptr<ProofNode> pf); - /** - * Make trust node: `a = b` as a Rewrite trust node - * - * @param a the original - * @param b what is rewrites to - * @param pf The proof of a = b, - * @return The trust node corresponding to the fact that this generator has - * a proof of a = b - */ - TrustNode mkTrustedRewrite( - Node a, Node b, std::shared_ptr<ProofNode> pf); - //--------------------------------------- common proofs - /** - * This returns the trust node corresponding to the splitting lemma - * (or f (not f)) and this generator. The method registers its proof in the - * map maintained by this class. - */ - TrustNode mkTrustNodeSplit(Node f); - //--------------------------------------- end common proofs - /** identify */ - std::string identify() const override; - - protected: - /** Set that pf is the proof for conflict conf */ - void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf); - /** Set that pf is the proof for lemma lem */ - void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf); - /** Set that pf is the proof for explained propagation */ - void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf); - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** Name identifier */ - std::string d_name; - /** A dummy context used by this class if none is provided */ - context::Context d_context; - /** - * A user-context-dependent map from lemmas and conflicts to proofs provided - * by calls to setProofForConflict and setProofForLemma above. - */ - NodeProofNodeMap d_proofs; -}; - -} // namespace theory -} // namespace cvc5 - -#endif /* CVC5__THEORY__PROOF_GENERATOR_H */ diff --git a/src/theory/fp/fp_expand_defs.h b/src/theory/fp/fp_expand_defs.h index a9edc8b02..8240f1f8e 100644 --- a/src/theory/fp/fp_expand_defs.h +++ b/src/theory/fp/fp_expand_defs.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp deleted file mode 100644 index 3fd3795c1..000000000 --- a/src/theory/lazy_tree_proof_generator.cpp +++ /dev/null @@ -1,146 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of the lazy tree proof generator class. - */ - -#include "theory/lazy_tree_proof_generator.h" - -#include <iostream> - -#include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { -namespace theory { - -LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, - const std::string& name) - : d_pnm(pnm), d_name(name) -{ - d_stack.emplace_back(&d_proof); -} -void LazyTreeProofGenerator::openChild() -{ - detail::TreeProofNode& pn = getCurrent(); - pn.d_children.emplace_back(); - d_stack.emplace_back(&pn.d_children.back()); -} -void LazyTreeProofGenerator::closeChild() -{ - Assert(getCurrent().d_rule != PfRule::UNKNOWN); - d_stack.pop_back(); -} -detail::TreeProofNode& LazyTreeProofGenerator::getCurrent() -{ - Assert(!d_stack.empty()) << "Proof construction has already been finished."; - return *d_stack.back(); -} -void LazyTreeProofGenerator::setCurrent(PfRule rule, - const std::vector<Node>& premise, - std::vector<Node> args, - Node proven) -{ - detail::TreeProofNode& pn = getCurrent(); - pn.d_rule = rule; - pn.d_premise = premise; - pn.d_args = args; - pn.d_proven = proven; -} -std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof() const -{ - // Check cache - if (d_cached) return d_cached; - Assert(d_stack.empty()) << "Proof construction has not yet been finished."; - std::vector<std::shared_ptr<ProofNode>> scope; - d_cached = getProof(scope, d_proof); - return d_cached; -} - -std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProofFor(Node f) -{ - Assert(hasProofFor(f)); - return getProof(); -} - -bool LazyTreeProofGenerator::hasProofFor(Node f) -{ - return f == getProof()->getResult(); -} - -std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof( - std::vector<std::shared_ptr<ProofNode>>& scope, - const detail::TreeProofNode& pn) const -{ - // Store scope size to reset scope afterwards - std::size_t before = scope.size(); - std::vector<std::shared_ptr<ProofNode>> children; - if (pn.d_rule == PfRule::SCOPE) - { - // Extend scope for all but the root node - if (&pn != &d_proof) - { - for (const auto& a : pn.d_args) - { - scope.emplace_back(d_pnm->mkAssume(a)); - } - } - } - else - { - // Initialize the children with the scope - children = scope; - } - for (auto& c : pn.d_children) - { - // Recurse into tree - children.emplace_back(getProof(scope, c)); - } - for (const auto& p : pn.d_premise) - { - // Add premises as assumptions - children.emplace_back(d_pnm->mkAssume(p)); - } - // Reset scope - scope.resize(before); - return d_pnm->mkNode(pn.d_rule, children, pn.d_args); -} - -void LazyTreeProofGenerator::print(std::ostream& os, - const std::string& prefix, - const detail::TreeProofNode& pn) const -{ - os << prefix << pn.d_rule << ": "; - container_to_stream(os, pn.d_premise); - os << " ==> " << pn.d_proven << std::endl; - if (!pn.d_args.empty()) - { - os << prefix << ":args "; - container_to_stream(os, pn.d_args); - std::cout << std::endl; - } - for (const auto& c : pn.d_children) - { - print(os, prefix + '\t', c); - } -} - -std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg) -{ - ltpg.print(os, "", ltpg.d_proof); - return os; -} - -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/lazy_tree_proof_generator.h b/src/theory/lazy_tree_proof_generator.h deleted file mode 100644 index 7ab921a70..000000000 --- a/src/theory/lazy_tree_proof_generator.h +++ /dev/null @@ -1,223 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The lazy tree proof generator class. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H -#define CVC5__THEORY__LAZY_TREE_PROOF_GENERATOR_H - -#include <iostream> - -#include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { -namespace theory { -namespace detail { -/** - * A single node in the proof tree created by the LazyTreeProofGenerator. - * A node directly represents a ProofNode that is eventually constructed from - * it. The Nodes of the additional field d_premise are added to d_children as - * new assumptions via ASSUME. - */ -struct TreeProofNode -{ - /** The proof rule */ - PfRule d_rule = PfRule::UNKNOWN; - /** Assumptions used as premise for this proof step */ - std::vector<Node> d_premise; - /** Arguments for this proof step */ - std::vector<Node> d_args; - /** Conclusion of this proof step */ - Node d_proven; - /** Children of this proof step */ - std::vector<TreeProofNode> d_children; -}; -} // namespace detail - -/** - * This class supports the lazy creation of a tree-shaped proof. - * The core idea is that the lazy creation is necessary because proof rules - * depend on assumptions that are only known after the whole subtree has been - * finished. - * - * We indend to argue about proofs that roughly go as follows: - * - we assume a set of assumptions - * - we do a case split - * - for every case, we derive false, possibly by nested case splits - * - * Every case is represented by a SCOPE whose child derives false. When - * composing the final proof, we explicitly extend the premise of every proof - * step with the scope (the currently selected case) that this proof step lives - * in. When doing this, we ignore the outermost scope (which assumes the - * assertion set) to allow for having conflicts that are only a subset of the - * assertion set. - * - * Consider the example x*x<1 and x>2 and the intended proof - * (SCOPE - * (ARITH_NL_CAD_SPLIT - * (SCOPE - * (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false) - * :args [x<=2] - * ) - * (SCOPE - * (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false) - * :args [x>=1] - * ) - * ) - * :args [ x*x<1, x>2 ] - * ) - * We obtain this proof in a way that (in general) gives us the assumptions - * for the scopes (x<=2, x>=1) only when the scope children have been fully - * computed. Thus, we store the proof in an intermediate form and add the scope - * arguments when we learn them. Once we have completed the proof, we can easily - * transform it into proper ProofNodes. - * - * This class is stateful in the sense that the interface (in particular - * openChild() and closeChild()) navigates the proof tree (and creating it - * on-the-fly). Initially, and after reset() has been called, the proof consists - * of one empty proof node (with proof rule UNKNOWN). It stores the current - * position in the proof tree internally to make the interface easier to use. - * - * THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE! - * - * To construct the above proof, use this class roughly as follows: - * setCurrent(SCOPE, {}, assertions, false); - * openChild(); - * // First nested scope - * openChild(); - * setCurrent(SCOPE, {}, {}, false); - * openChild(); - * setCurrent(CAD_DIRECT, {x>2}, {}, false); - * closeChild(); - * getCurrent().args = {x<=2}; - * closeChild(); - * // Second nested scope - * openChild(); - * setCurrent(SCOPE, {}, {}, false); - * openChild(); - * setCurrent(CAD_DIRECT, {x*x<1}, {}, false); - * closeChild(); - * getCurrent().args = {x>=1}; - * closeChild(); - * // Finish split - * setCurrent(CAD_SPLIT, {}, {}, false); - * closeChild(); - * closeChild(); - * - * To explicitly finish proof construction, we need to call closeChild() one - * additional time. - */ -class LazyTreeProofGenerator : public ProofGenerator -{ - public: - friend std::ostream& operator<<(std::ostream& os, - const LazyTreeProofGenerator& ltpg); - - LazyTreeProofGenerator(ProofNodeManager* pnm, - const std::string& name = "LazyTreeProofGenerator"); - - std::string identify() const override { return d_name; } - /** Create a new child and make it the current node */ - void openChild(); - /** - * Finish the current node and return to its parent - * Checks that the current node has a proof rule different from UNKNOWN. - * When called on the root node, this finishes the proof construction: we can - * no longer call getCurrent(), setCurrent() openChild() and closeChild(), but - * instead can call getProof() now. - */ - void closeChild(); - /** - * Return a reference to the current node - */ - detail::TreeProofNode& getCurrent(); - /** Set the current node / proof step */ - void setCurrent(PfRule rule, - const std::vector<Node>& premise, - std::vector<Node> args, - Node proven); - /** Construct the proof as a ProofNode */ - std::shared_ptr<ProofNode> getProof() const; - /** Return the constructed proof. Checks that we have proven f */ - std::shared_ptr<ProofNode> getProofFor(Node f) override; - /** Checks whether we have proven f */ - bool hasProofFor(Node f) override; - - /** - * Removes children from the current node based on the given predicate. - * It can be used for cases where facts (and their proofs) are eagerly - * generated and then later pruned, for example to produce smaller conflicts. - * The predicate is given as a Callable f that is called for every child with - * the id of the child and the child itself. - * f should return true if the child should be kept, fals if the child should - * be removed. - * @param f a Callable bool(std::size_t, const detail::TreeProofNode&) - */ - template <typename F> - void pruneChildren(F&& f) - { - auto& children = getCurrent().d_children; - std::size_t cur = 0; - std::size_t pos = 0; - for (std::size_t size = children.size(); cur < size; ++cur) - { - if (f(cur, children[pos])) - { - if (cur != pos) - { - children[pos] = std::move(children[cur]); - } - ++pos; - } - } - children.resize(pos); - } - - private: - /** recursive proof construction used by getProof() */ - std::shared_ptr<ProofNode> getProof( - std::vector<std::shared_ptr<ProofNode>>& scope, - const detail::TreeProofNode& pn) const; - - /** recursive debug printing used by operator<<() */ - void print(std::ostream& os, - const std::string& prefix, - const detail::TreeProofNode& pn) const; - - /** The ProofNodeManager used for constructing ProofNodes */ - ProofNodeManager* d_pnm; - /** The trace to the current node */ - std::vector<detail::TreeProofNode*> d_stack; - /** The root node of the proof tree */ - detail::TreeProofNode d_proof; - /** Caches the result of getProof() */ - mutable std::shared_ptr<ProofNode> d_cached; - /** Name of this proof generator */ - std::string d_name; -}; - -/** - * Prints the current state of a LazyTreeProofGenerator. Can also be used on a - * partially constructed proof. It is intended for debugging only and attempts - * to pretty-print itself using indentation. - */ -std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); - -} // namespace theory -} // namespace cvc5 - -#endif diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 8e802f875..b681dad17 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -18,8 +18,8 @@ #ifndef CVC5__THEORY__OUTPUT_CHANNEL_H #define CVC5__THEORY__OUTPUT_CHANNEL_H +#include "proof/trust_node.h" #include "theory/incomplete_id.h" -#include "theory/trust_node.h" #include "util/resource_manager.h" namespace cvc5 { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 9effdbec7..71f4028ec 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -15,12 +15,12 @@ #include "theory/quantifiers/instantiate.h" -#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 9b410dd08..95a396d51 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -22,7 +22,7 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof.h" +#include "proof/proof.h" #include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index 618ac8301..23441772e 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__QUANTIFIERS__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/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index cfc4eca2e..ae7f75f34 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -18,8 +18,8 @@ #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#include "proof/trust_node.h" #include "theory/theory_rewriter.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index c9234db2c..fa91b1782 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -17,11 +17,11 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "proof/proof.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_registry.h" diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 2a09913a9..c8e6ec7dd 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -24,8 +24,8 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/type_node.h" -#include "theory/eager_proof_generator.h" -#include "theory/trust_node.h" +#include "proof/eager_proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6bfedb0a2..c74146c9c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -15,8 +15,8 @@ #include "theory/quantifiers/theory_quantifiers.h" -#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" +#include "proof/proof_node_manager.h" #include "theory/quantifiers/quantifiers_macros.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 1094d5920..eeb2f166d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -15,8 +15,8 @@ #include "theory/rewriter.h" -#include "expr/term_conversion_proof_generator.h" #include "options/theory_options.h" +#include "proof/conv_proof_generator.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 87f25341e..f88596ffe 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -22,7 +22,7 @@ #include <vector> #include "context/cdhashmap.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" #include "theory/sets/inference_manager.h" #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 40f6080e5..b684ff56f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" #include "theory/ee_setup_info.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" #include "util/statistics_stats.h" diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index 2cb1c6738..277daf88c 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -19,7 +19,7 @@ #define CVC5__THEORY__SKOLEM_LEMMA_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 29a4187ec..d214babae 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -15,10 +15,10 @@ #include "theory/strings/infer_proof_cons.h" -#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/strings_options.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" #include "theory/strings/regexp_operation.h" diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index af905cbad..bba03dd28 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -21,12 +21,12 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_rule.h" +#include "proof/proof_checker.h" +#include "proof/proof_rule.h" +#include "proof/theory_proof_step_buffer.h" #include "theory/builtin/proof_checker.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" -#include "theory/theory_proof_step_buffer.h" #include "theory/uf/proof_equality_engine.h" namespace cvc5 { diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index cf9c64bb1..da44100f9 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -24,7 +24,7 @@ #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" -#include "expr/proof_node_manager.h" +#include "proof/proof_node_manager.h" #include "theory/ext_theory.h" #include "theory/inference_manager_buffered.h" #include "theory/output_channel.h" diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index d3ede53ec..56afaed84 100644 --- a/src/theory/strings/proof_checker.h +++ b/src/theory/strings/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__STRINGS__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/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index b9af7a23f..c3580d963 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -15,8 +15,8 @@ #include "theory/strings/regexp_elim.h" -#include "expr/proof_node_manager.h" #include "options/strings_options.h" +#include "proof/proof_node_manager.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 5387548de..6187a7137 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -18,8 +18,8 @@ #define CVC5__THEORY__STRINGS__REGEXP_ELIM_H #include "expr/node.h" -#include "theory/eager_proof_generator.h" -#include "theory/trust_node.h" +#include "proof/eager_proof_generator.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 7c399759b..7d660e019 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -20,8 +20,8 @@ #include "context/cdhashset.h" #include "context/cdlist.h" -#include "expr/proof_node_manager.h" -#include "theory/eager_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node_manager.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 8f69d4cb2..d71348ce3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,12 +28,12 @@ #include "context/context.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" #include "theory/theory_id.h" -#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_stats.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index abbca451a..676351dd5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -20,15 +20,15 @@ #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" -#include "expr/lazy_proof.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" -#include "expr/proof_checker.h" -#include "expr/proof_ensure_closed.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" +#include "proof/lazy_proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_ensure_closed.h" #include "prop/prop_engine.h" #include "smt/dump.h" #include "smt/env.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6887959ed..ffcaf392f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -25,6 +25,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "options/theory_options.h" +#include "proof/trust_node.h" #include "theory/atom_requests.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" @@ -32,7 +33,6 @@ #include "theory/sort_inference.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" -#include "theory/trust_node.h" #include "theory/trust_substitutions.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 609d7ae8a..f10716bd9 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -17,7 +17,7 @@ #include <sstream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" using namespace cvc5::kind; diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 48969aa21..ab0f616fe 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "theory/trust_node.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 2cb7d9d30..06806f8d4 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -22,10 +22,10 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "expr/proof_rule.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" #include "theory/inference_id.h" #include "theory/output_channel.h" -#include "theory/trust_node.h" #include "util/statistics_stats.h" namespace cvc5 { diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 65bd160fc..230c23424 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -15,8 +15,8 @@ #include "theory/theory_preprocessor.h" -#include "expr/lazy_proof.h" #include "expr/skolem_manager.h" +#include "proof/lazy_proof.h" #include "smt/logic_exception.h" #include "theory/logic_info.h" #include "theory/rewriter.h" diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 58dd763e0..6015f2b07 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -22,13 +22,13 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/tconv_seq_proof_generator.h" -#include "expr/term_conversion_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/conv_seq_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/trust_node.h" #include "smt/term_formula_removal.h" #include "theory/skolem_lemma.h" -#include "theory/trust_node.h" namespace cvc5 { diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp deleted file mode 100644 index 667c8d114..000000000 --- a/src/theory/theory_proof_step_buffer.cpp +++ /dev/null @@ -1,240 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Haniel Barbosa, Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of theory proof step buffer utility. - */ - -#include "theory/theory_proof_step_buffer.h" - -#include "expr/proof.h" - -using namespace cvc5::kind; - -namespace cvc5 { -namespace theory { - -TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) - : ProofStepBuffer(pc) -{ -} - -bool TheoryProofStepBuffer::applyEqIntro(Node src, - Node tgt, - const std::vector<Node>& exp, - MethodId ids, - MethodId ida, - MethodId idr) -{ - std::vector<Node> args; - args.push_back(src); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); - Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args); - if (res.isNull()) - { - // failed to apply - return false; - } - // should have concluded the expected equality - Node expected = src.eqNode(tgt); - if (res != expected) - { - // did not provide the correct target - popStep(); - return false; - } - // successfully proved src == tgt. - return true; -} - -bool TheoryProofStepBuffer::applyPredTransform(Node src, - Node tgt, - const std::vector<Node>& exp, - MethodId ids, - MethodId ida, - MethodId idr) -{ - // symmetric equalities - if (CDProof::isSame(src, tgt)) - { - return true; - } - std::vector<Node> children; - children.push_back(src); - std::vector<Node> args; - // try to prove that tgt rewrites to src - children.insert(children.end(), exp.begin(), exp.end()); - args.push_back(tgt); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); - Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); - if (res.isNull()) - { - // failed to apply - return false; - } - // should definitely have concluded tgt - Assert(res == tgt); - return true; -} - -bool TheoryProofStepBuffer::applyPredIntro(Node tgt, - const std::vector<Node>& exp, - MethodId ids, - MethodId ida, - MethodId idr) -{ - std::vector<Node> args; - args.push_back(tgt); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); - Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); - if (res.isNull()) - { - return false; - } - Assert(res == tgt); - return true; -} - -Node TheoryProofStepBuffer::applyPredElim(Node src, - const std::vector<Node>& exp, - MethodId ids, - MethodId ida, - MethodId idr) -{ - std::vector<Node> children; - children.push_back(src); - children.insert(children.end(), exp.begin(), exp.end()); - std::vector<Node> args; - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); - Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); - if (CDProof::isSame(src, srcRew)) - { - popStep(); - } - return srcRew; -} - -Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n) -{ - if (n.getKind() != kind::OR) - { - return elimDoubleNegLit(n); - } - NodeManager* nm = NodeManager::currentNM(); - std::vector<Node> children{n.begin(), n.end()}; - std::vector<Node> childrenEqs; - // eliminate double neg for each lit. Do it first because it may expose - // duplicates - bool hasDoubleNeg = false; - for (unsigned i = 0; i < children.size(); ++i) - { - if (children[i].getKind() == kind::NOT - && children[i][0].getKind() == kind::NOT) - { - hasDoubleNeg = true; - childrenEqs.push_back(children[i].eqNode(children[i][0][0])); - addStep(PfRule::MACRO_SR_PRED_INTRO, - {}, - {childrenEqs.back()}, - childrenEqs.back()); - // update child - children[i] = children[i][0][0]; - } - else - { - childrenEqs.push_back(children[i].eqNode(children[i])); - addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back()); - } - } - if (hasDoubleNeg) - { - Node oldn = n; - n = nm->mkNode(kind::OR, children); - // Create a congruence step to justify replacement of each doubly negated - // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM - // from the old clause to the new one, which, under the standard rewriter, - // may not hold. An example is - // - // --------------------------------------------------------------------- - // (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2) - // - // which fails due to factoring not happening after flattening. - // - // Using congruence only the - // - // ------------------ MACRO_SR_PRED_INTRO - // (not (not t)) = t - // - // steps are added, which, since double negation is eliminated in a - // pre-rewrite in the Boolean rewriter, will always hold under the - // standard rewriter. - Node congEq = oldn.eqNode(n); - addStep(PfRule::CONG, - childrenEqs, - {ProofRuleChecker::mkKindNode(kind::OR)}, - congEq); - // add an equality resolution step to derive normalize clause - addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n); - } - children.clear(); - // remove duplicates while keeping the order of children - std::unordered_set<TNode> clauseSet; - unsigned size = n.getNumChildren(); - for (unsigned i = 0; i < size; ++i) - { - if (clauseSet.count(n[i])) - { - continue; - } - children.push_back(n[i]); - clauseSet.insert(n[i]); - } - // if factoring changed - if (children.size() < size) - { - Node factored = children.empty() - ? nm->mkConst<bool>(false) - : children.size() == 1 ? children[0] - : nm->mkNode(kind::OR, children); - // don't overwrite what already has a proof step to avoid cycles - addStep(PfRule::FACTORING, {n}, {}, factored); - n = factored; - } - // nothing to order - if (children.size() < 2) - { - return n; - } - // order - std::sort(children.begin(), children.end()); - Node ordered = nm->mkNode(kind::OR, children); - // if ordering changed - if (ordered != n) - { - // don't overwrite what already has a proof step to avoid cycles - addStep(PfRule::REORDERING, {n}, {ordered}, ordered); - } - return ordered; -} - -Node TheoryProofStepBuffer::elimDoubleNegLit(Node n) -{ - // eliminate double neg - if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT) - { - addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]); - return n[0][0]; - } - return n; -} - -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h deleted file mode 100644 index 1832ddb08..000000000 --- a/src/theory/theory_proof_step_buffer.h +++ /dev/null @@ -1,120 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Theory proof step buffer utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H -#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H - -#include <vector> - -#include "expr/node.h" -#include "expr/proof_step_buffer.h" -#include "theory/builtin/proof_checker.h" - -namespace cvc5 { -namespace theory { -/** - * Class used to speculatively try and buffer a set of proof steps before - * sending them to a proof object, extended with theory-specfic proof rule - * utilities. - */ -class TheoryProofStepBuffer : public ProofStepBuffer -{ - public: - TheoryProofStepBuffer(ProofChecker* pc = nullptr); - ~TheoryProofStepBuffer() {} - //---------------------------- utilities builtin proof rules - /** - * Apply equality introduction. If this method returns true, it adds proof - * step(s) to the buffer that conclude (= src tgt) from premises exp. In - * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This - * method should be applied when tgt is equivalent to src assuming exp. - */ - bool applyEqIntro(Node src, - Node tgt, - const std::vector<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId ida = MethodId::SBA_SEQUENTIAL, - MethodId idr = MethodId::RW_REWRITE); - /** - * Apply predicate transform. If this method returns true, it adds (at most - * one) proof step to the buffer that conclude tgt from premises src, exp. In - * particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method - * should be applied when src and tgt are equivalent formulas assuming exp. - */ - bool applyPredTransform(Node src, - Node tgt, - const std::vector<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId ida = MethodId::SBA_SEQUENTIAL, - MethodId idr = MethodId::RW_REWRITE); - /** - * Apply predicate introduction. If this method returns true, it adds proof - * step(s) to the buffer that conclude tgt from premises exp. In particular, - * it may attempt to apply the rule MACRO_SR_PRED_INTRO. This method should be - * applied when tgt is equivalent to true assuming exp. - */ - bool applyPredIntro(Node tgt, - const std::vector<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId ida = MethodId::SBA_SEQUENTIAL, - MethodId idr = MethodId::RW_REWRITE); - /** - * Apply predicate elimination. This method returns the result of applying - * the rule MACRO_SR_PRED_ELIM on src, exp. The returned formula is equivalent - * to src assuming exp. If the return value is equivalent to src, then no - * proof step is added to this buffer, since this step is a no-op in this - * case. - * - * Notice that in contrast to the other rules above, predicate elimination - * never fails and proves a formula that is not explicitly given as an - * argument tgt. Thus, the return value of this method is Node not bool. - */ - Node applyPredElim(Node src, - const std::vector<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId ida = MethodId::SBA_SEQUENTIAL, - MethodId idr = MethodId::RW_REWRITE); - //---------------------------- end utilities builtin proof rules - - //---------------------------- utility methods for normalizing clauses - /** - * Normalizes a non-unit clause (an OR node) according to factoring and - * reordering, i.e. removes duplicates and reorders literals (according to - * node ids). Moreover it eliminates double negations, which can be done also - * for unit clauses (a arbitrary Boolean node). All normalization steps are - * tracked via proof steps added to this proof step buffer. - * - * @param n the clause to be normalized - * @return the normalized clause node - */ - Node factorReorderElimDoubleNeg(Node n); - - /** - * Eliminates double negation of a literal if it has the form - * (not (not t)) - * If the elimination happens, a step is added to this proof step buffer. - * - * @param n the node to have the top-level double negation eliminated - * @return the normalized clause node - */ - Node elimDoubleNegLit(Node n); -}; - -} // namespace theory -} // namespace cvc5 - -#endif /* CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H */ diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index 031e32db4..eca1e4e56 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -21,7 +21,7 @@ #define CVC5__THEORY__THEORY_REWRITER_H #include "expr/node.h" -#include "theory/trust_node.h" +#include "proof/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp deleted file mode 100644 index 4086d6e86..000000000 --- a/src/theory/trust_node.cpp +++ /dev/null @@ -1,150 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of the trust node utility. - */ - -#include "theory/trust_node.h" - -#include "expr/proof_ensure_closed.h" -#include "expr/proof_generator.h" - -namespace cvc5 { -namespace theory { - -const char* toString(TrustNodeKind tnk) -{ - switch (tnk) - { - case TrustNodeKind::CONFLICT: return "CONFLICT"; - case TrustNodeKind::LEMMA: return "LEMMA"; - case TrustNodeKind::PROP_EXP: return "PROP_EXP"; - case TrustNodeKind::REWRITE: return "REWRITE"; - default: return "?"; - } -} - -std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk) -{ - out << toString(tnk); - return out; -} - -TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g) -{ - Node ckey = getConflictProven(conf); - // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(ckey)); - return TrustNode(TrustNodeKind::CONFLICT, ckey, g); -} - -TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g) -{ - Node lkey = getLemmaProven(lem); - // if a generator is provided, should confirm that it can prove it - Assert(g == nullptr || g->hasProofFor(lkey)); - return TrustNode(TrustNodeKind::LEMMA, lkey, g); -} - -TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g) -{ - Node pekey = getPropExpProven(lit, exp); - Assert(g == nullptr || g->hasProofFor(pekey)); - return TrustNode(TrustNodeKind::PROP_EXP, pekey, g); -} - -TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g) -{ - Node rkey = getRewriteProven(n, nr); - Assert(g == nullptr || g->hasProofFor(rkey)); - return TrustNode(TrustNodeKind::REWRITE, rkey, g); -} - -TrustNode TrustNode::null() -{ - return TrustNode(TrustNodeKind::INVALID, Node::null()); -} - -TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) - : d_tnk(tnk), d_proven(p), d_gen(g) -{ - // does not make sense to provide null node with generator - Assert(!d_proven.isNull() || d_gen == nullptr); -} - -TrustNodeKind TrustNode::getKind() const { return d_tnk; } - -Node TrustNode::getNode() const -{ - switch (d_tnk) - { - // the node of lemma is the node itself - case TrustNodeKind::LEMMA: return d_proven; - // the node of the rewrite is the right hand side of EQUAL - case TrustNodeKind::REWRITE: return d_proven[1]; - // the node of an explained propagation is the antecendant of an IMPLIES - // the node of a conflict is underneath a NOT - default: return d_proven[0]; - } -} - -Node TrustNode::getProven() const { return d_proven; } - -ProofGenerator* TrustNode::getGenerator() const { return d_gen; } - -bool TrustNode::isNull() const { return d_proven.isNull(); } - -std::shared_ptr<ProofNode> TrustNode::toProofNode() const -{ - if (d_gen == nullptr) - { - return nullptr; - } - return d_gen->getProofFor(d_proven); -} - -Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } - -Node TrustNode::getLemmaProven(Node lem) { return lem; } - -Node TrustNode::getPropExpProven(TNode lit, Node exp) -{ - return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit); -} - -Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } - -void TrustNode::debugCheckClosed(const char* c, - const char* ctx, - bool reqNullGen) -{ - pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen); -} - -std::string TrustNode::identifyGenerator() const -{ - if (d_gen == nullptr) - { - return "null"; - } - return d_gen->identify(); -} - -std::ostream& operator<<(std::ostream& out, TrustNode n) -{ - out << "(" << n.getKind() << " " << n.getProven() << " " - << n.identifyGenerator() << ")"; - return out; -} - -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h deleted file mode 100644 index 0a4f20c34..000000000 --- a/src/theory/trust_node.h +++ /dev/null @@ -1,178 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The trust node utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__TRUST_NODE_H -#define CVC5__THEORY__TRUST_NODE_H - -#include "expr/node.h" - -namespace cvc5 { - -class ProofGenerator; -class ProofNode; - -namespace theory { - -/** A kind for trust nodes */ -enum class TrustNodeKind : uint32_t -{ - CONFLICT, - LEMMA, - PROP_EXP, - REWRITE, - INVALID -}; -/** - * Converts a proof rule to a string. Note: This function is also used in - * `safe_print()`. Changing this function name or signature will result in - * `safe_print()` printing "<unsupported>" instead of the proper strings for - * the enum values. - * - * Returns a string with static lifetime: it should not be freed. - * - * @param tnk The trust node kind - * @return The name of the trust node kind - */ -const char* toString(TrustNodeKind tnk); - -/** - * Writes a trust node kind name to a stream. - * - * @param out The stream to write to - * @param tnk The trust node kind to write to the stream - * @return The stream - */ -std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk); - -/** - * A trust node is a pair (F, G) where F is a formula and G is a proof - * generator that can construct a proof for F if asked. - * - * More generally, a trust node is any node that can be used for a specific - * purpose that requires justification, such as being passed to - * OutputChannel::lemma. That justification is intended to be given by the - * generator that is required to construct this object. - * - * They are intended to be constructed by ProofGenerator objects themselves (a - * proof generator wraps itself in TrustNode it returns) and passed - * to ProofOutputChannel by theory solvers. - * - * The static functions for constructing them check that the generator, if - * provided, is capable of proving the given conflict or lemma, or an assertion - * failure occurs. Otherwise an assertion error is given. - * - * While this is not enforced, a `TrustNode` generally encapsulates a **closed** proof - * of the formula: one without free assumptions. - */ -class TrustNode -{ - public: - TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {} - /** Make a proven node for conflict */ - static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr); - /** Make a proven node for lemma */ - static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr); - /** Make a proven node for explanation of propagated literal */ - static TrustNode mkTrustPropExp(TNode lit, - Node exp, - ProofGenerator* g = nullptr); - /** Make a proven node for rewrite */ - static TrustNode mkTrustRewrite(TNode n, - Node nr, - ProofGenerator* g = nullptr); - /** The null proven node */ - static TrustNode null(); - ~TrustNode() {} - /** get kind */ - TrustNodeKind getKind() const; - /** get node - * - * This is the node that is used in a common interface, either: - * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict, - * (2) A valid T-formula lem to pass to OutputChannel::lemma, - * (3) A conjunction of literals exp to return in Theory::explain(lit), or - * (4) A result of rewriting a term n into an equivalent one nr. - * - * Notice that this node does not necessarily correspond to a valid formula. - * The call getProven() below retrieves a valid formula corresponding to - * the above calls. - */ - Node getNode() const; - /** get proven - * - * This is the corresponding formula that is proven by the proof generator - * for the above cases: - * (1) (not conf), for conflicts, - * (2) lem, for lemmas, - * (3) (=> exp lit), for propagations from explanations, - * (4) (= n nr), for results of rewriting. - * - * When constructing this trust node, the proof generator should be able to - * provide a proof for this fact. - */ - Node getProven() const; - /** get generator */ - ProofGenerator* getGenerator() const; - /** is null? */ - bool isNull() const; - /** - * Gets the proof node for this trust node, which is obtained by - * calling the generator's getProofFor method on the proven node. - */ - std::shared_ptr<ProofNode> toProofNode() const; - - /** Get the proven formula corresponding to a conflict call */ - static Node getConflictProven(Node conf); - /** Get the proven formula corresponding to a lemma call */ - static Node getLemmaProven(Node lem); - /** Get the proven formula corresponding to explanations for propagation */ - static Node getPropExpProven(TNode lit, Node exp); - /** Get the proven formula corresponding to a rewrite */ - static Node getRewriteProven(TNode n, Node nr); - /** For debugging */ - std::string identifyGenerator() const; - - /** - * debug check closed on Trace c, context ctx is string for debugging - * - * @param reqNullGen Whether we consider a null generator to be a failure. - */ - void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true); - - private: - TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr); - /** The kind */ - TrustNodeKind d_tnk; - /** The proven node */ - Node d_proven; - /** The generator */ - ProofGenerator* d_gen; -}; - -/** - * Writes a trust node to a stream. - * - * @param out The stream to write to - * @param n The trust node to write to the stream - * @return The stream - */ -std::ostream& operator<<(std::ostream& out, TrustNode n); - -} // namespace theory -} // namespace cvc5 - -#endif /* CVC5__THEORY__TRUST_NODE_H */ diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 136992fbe..2a6997d1d 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -21,14 +21,14 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "context/context.h" -#include "expr/lazy_proof.h" -#include "expr/proof_node_manager.h" -#include "expr/proof_set.h" -#include "expr/term_conversion_proof_generator.h" -#include "theory/eager_proof_generator.h" +#include "proof/conv_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" +#include "proof/proof_node_manager.h" +#include "proof/proof_set.h" +#include "proof/theory_proof_step_buffer.h" +#include "proof/trust_node.h" #include "theory/substitutions.h" -#include "theory/theory_proof_step_buffer.h" -#include "theory/trust_node.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index c63f8b51d..fbed7ffb5 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -16,9 +16,9 @@ #include "theory/uf/eq_proof.h" #include "base/configuration.h" -#include "expr/proof.h" -#include "expr/proof_checker.h" #include "options/uf_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h index 55f7db3ba..caeda828e 100644 --- a/src/theory/uf/proof_checker.h +++ b/src/theory/uf/proof_checker.h @@ -19,8 +19,8 @@ #define CVC5__THEORY__UF__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/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index ab36cd9df..b4522d9df 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -15,9 +15,9 @@ #include "theory/uf/proof_equality_engine.h" -#include "expr/lazy_proof_chain.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" +#include "proof/lazy_proof_chain.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 4ca13d93f..0c093d4b2 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -22,10 +22,10 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" -#include "expr/buffered_proof_generator.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "theory/eager_proof_generator.h" +#include "proof/buffered_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "proof/lazy_proof.h" namespace cvc5 { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9cf47bab3..1afb8cc31 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -21,11 +21,11 @@ #include <sstream> #include "expr/node_algorithm.h" -#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "proof/proof_node_manager.h" #include "smt/logic_exception.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" |