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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 27 May 2021 21:28:58 +0000 (16:28 -0500)
committer	GitHub <noreply@github.com>
	Thu, 27 May 2021 21:28:58 +0000 (21:28 +0000)
commit	8b3de13131d24bf400ba5f36fc234008d950f345
tree	0de3a60dcdad716cede78b8fe024996690399a2f	tree
parent	b9062490a7590708bcf158d4670a23d859fe3355	commit \| diff

Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

49 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.cpp		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.h		diff \| blob \| history
src/proof/conv_seq_proof_generator.cpp		diff \| blob \| history
src/proof/conv_seq_proof_generator.h		diff \| blob \| history
src/proof/eager_proof_generator.cpp		diff \| blob \| history
src/proof/eager_proof_generator.h		diff \| blob \| history
src/proof/lazy_tree_proof_generator.cpp		diff \| blob \| history
src/proof/lazy_tree_proof_generator.h		diff \| blob \| history
src/proof/method_id.cpp	[new file with mode: 0644]	blob
src/proof/method_id.h	[new file with mode: 0644]	blob
src/proof/theory_proof_step_buffer.cpp		diff \| blob \| history
src/proof/theory_proof_step_buffer.h		diff \| blob \| history
src/proof/trust_node.cpp		diff \| blob \| history
src/proof/trust_node.h		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/proof_cnf_stream.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		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_post_processor.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/builtin/proof_checker.cpp		diff \| blob \| history
src/theory/builtin/proof_checker.h		diff \| blob \| history
src/theory/combination_engine.h		diff \| blob \| history
src/theory/datatypes/inference_manager.h		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.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
test/unit/test_smt.h		diff \| blob \| history

RSS Atom