git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 24 May 2021 18:51:09 +0000 (13:51 -0500)
committer	GitHub <noreply@github.com>
	Mon, 24 May 2021 18:51:09 +0000 (15:51 -0300)
commit	bd33d20609999f6f847aeb63a42350aeb3041406
tree	8b4a3ccb0ab48b65bd70222dbfd572de8743bcd9	tree
parent	1516e3b5d9436be86841a52002fc728fcd52dd34	commit \| diff

Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

202 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/buffered_proof_generator.cpp	[deleted file]	blob \| history
src/expr/buffered_proof_generator.h	[deleted file]	blob \| history
src/expr/lazy_proof.cpp	[deleted file]	blob \| history
src/expr/lazy_proof.h	[deleted file]	blob \| history
src/expr/lazy_proof_chain.cpp	[deleted file]	blob \| history
src/expr/lazy_proof_chain.h	[deleted file]	blob \| history
src/expr/proof.cpp	[deleted file]	blob \| history
src/expr/proof.h	[deleted file]	blob \| history
src/expr/proof_checker.cpp	[deleted file]	blob \| history
src/expr/proof_checker.h	[deleted file]	blob \| history
src/expr/proof_ensure_closed.cpp	[deleted file]	blob \| history
src/expr/proof_ensure_closed.h	[deleted file]	blob \| history
src/expr/proof_generator.cpp	[deleted file]	blob \| history
src/expr/proof_generator.h	[deleted file]	blob \| history
src/expr/proof_node.cpp	[deleted file]	blob \| history
src/expr/proof_node.h	[deleted file]	blob \| history
src/expr/proof_node_algorithm.cpp	[deleted file]	blob \| history
src/expr/proof_node_algorithm.h	[deleted file]	blob \| history
src/expr/proof_node_manager.cpp	[deleted file]	blob \| history
src/expr/proof_node_manager.h	[deleted file]	blob \| history
src/expr/proof_node_to_sexpr.cpp	[deleted file]	blob \| history
src/expr/proof_node_to_sexpr.h	[deleted file]	blob \| history
src/expr/proof_node_updater.cpp	[deleted file]	blob \| history
src/expr/proof_node_updater.h	[deleted file]	blob \| history
src/expr/proof_rule.cpp	[deleted file]	blob \| history
src/expr/proof_rule.h	[deleted file]	blob \| history
src/expr/proof_set.h	[deleted file]	blob \| history
src/expr/proof_step_buffer.cpp	[deleted file]	blob \| history
src/expr/proof_step_buffer.h	[deleted file]	blob \| history
src/expr/tconv_seq_proof_generator.cpp	[deleted file]	blob \| history
src/expr/tconv_seq_proof_generator.h	[deleted file]	blob \| history
src/expr/term_conversion_proof_generator.cpp	[deleted file]	blob \| history
src/expr/term_conversion_proof_generator.h	[deleted file]	blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.h		diff \| blob \| history
src/proof/buffered_proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/buffered_proof_generator.h	[new file with mode: 0644]	blob
src/proof/conv_proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/conv_proof_generator.h	[new file with mode: 0644]	blob
src/proof/conv_seq_proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/conv_seq_proof_generator.h	[new file with mode: 0644]	blob
src/proof/dot/dot_printer.cpp		diff \| blob \| history
src/proof/dot/dot_printer.h		diff \| blob \| history
src/proof/eager_proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/eager_proof_generator.h	[new file with mode: 0644]	blob
src/proof/lazy_proof.cpp	[new file with mode: 0644]	blob
src/proof/lazy_proof.h	[new file with mode: 0644]	blob
src/proof/lazy_proof_chain.cpp	[new file with mode: 0644]	blob
src/proof/lazy_proof_chain.h	[new file with mode: 0644]	blob
src/proof/lazy_tree_proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/lazy_tree_proof_generator.h	[new file with mode: 0644]	blob
src/proof/proof.cpp	[new file with mode: 0644]	blob
src/proof/proof.h	[new file with mode: 0644]	blob
src/proof/proof_checker.cpp	[new file with mode: 0644]	blob
src/proof/proof_checker.h	[new file with mode: 0644]	blob
src/proof/proof_ensure_closed.cpp	[new file with mode: 0644]	blob
src/proof/proof_ensure_closed.h	[new file with mode: 0644]	blob
src/proof/proof_generator.cpp	[new file with mode: 0644]	blob
src/proof/proof_generator.h	[new file with mode: 0644]	blob
src/proof/proof_node.cpp	[new file with mode: 0644]	blob
src/proof/proof_node.h	[new file with mode: 0644]	blob
src/proof/proof_node_algorithm.cpp	[new file with mode: 0644]	blob
src/proof/proof_node_algorithm.h	[new file with mode: 0644]	blob
src/proof/proof_node_manager.cpp	[new file with mode: 0644]	blob
src/proof/proof_node_manager.h	[new file with mode: 0644]	blob
src/proof/proof_node_to_sexpr.cpp	[new file with mode: 0644]	blob
src/proof/proof_node_to_sexpr.h	[new file with mode: 0644]	blob
src/proof/proof_node_updater.cpp	[new file with mode: 0644]	blob
src/proof/proof_node_updater.h	[new file with mode: 0644]	blob
src/proof/proof_rule.cpp	[new file with mode: 0644]	blob
src/proof/proof_rule.h	[new file with mode: 0644]	blob
src/proof/proof_set.h	[new file with mode: 0644]	blob
src/proof/proof_step_buffer.cpp	[new file with mode: 0644]	blob
src/proof/proof_step_buffer.h	[new file with mode: 0644]	blob
src/proof/theory_proof_step_buffer.cpp	[new file with mode: 0644]	blob
src/proof/theory_proof_step_buffer.h	[new file with mode: 0644]	blob
src/proof/trust_node.cpp	[new file with mode: 0644]	blob
src/proof/trust_node.h	[new file with mode: 0644]	blob
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/proof_cnf_stream.h		diff \| blob \| history
src/prop/proof_post_processor.h		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/prop_proof_manager.h		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/env.cpp		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/expand_definitions.h		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.h		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/smt/unsat_core_manager.cpp		diff \| blob \| history
src/smt/unsat_core_manager.h		diff \| blob \| history
src/smt/witness_form.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/nl/cad/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.h		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/operator_elim.h		diff \| blob \| history
src/theory/arith/proof_checker.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arrays/inference_manager.h		diff \| blob \| history
src/theory/arrays/proof_checker.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/proof_checker.h		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/builtin/proof_checker.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/bv/bv_solver_simple.cpp		diff \| blob \| history
src/theory/bv/proof_checker.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/combination_engine.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/inference.h		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/datatypes/proof_checker.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/eager_proof_generator.cpp	[deleted file]	blob \| history
src/theory/eager_proof_generator.h	[deleted file]	blob \| history
src/theory/fp/fp_expand_defs.h		diff \| blob \| history
src/theory/lazy_tree_proof_generator.cpp	[deleted file]	blob \| history
src/theory/lazy_tree_proof_generator.h	[deleted file]	blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/proof_checker.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sets/term_registry.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/skolem_lemma.h		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.h		diff \| blob \| history
src/theory/strings/inference_manager.h		diff \| blob \| history
src/theory/strings/proof_checker.h		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.h		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_engine_proof_generator.cpp		diff \| blob \| history
src/theory/theory_engine_proof_generator.h		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/theory_preprocessor.h		diff \| blob \| history
src/theory/theory_proof_step_buffer.cpp	[deleted file]	blob \| history
src/theory/theory_proof_step_buffer.h	[deleted file]	blob \| history
src/theory/theory_rewriter.h		diff \| blob \| history
src/theory/trust_node.cpp	[deleted file]	blob \| history
src/theory/trust_node.h	[deleted file]	blob \| history
src/theory/trust_substitutions.h		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/proof_checker.h		diff \| blob \| history
src/theory/uf/proof_equality_engine.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/util/stats_black.cpp		diff \| blob \| history

RSS Atom