proof « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	annotation_proof_generator.cpp	2586	log plain
-rw-r--r--	annotation_proof_generator.h	3073	log plain
-rw-r--r--	buffered_proof_generator.cpp	2870	log plain
-rw-r--r--	buffered_proof_generator.h	2109	log plain
-rw-r--r--	clause_id.h	1315	log plain
-rw-r--r--	conv_proof_generator.cpp	20693	log plain
-rw-r--r--	conv_proof_generator.h	10843	log plain
-rw-r--r--	conv_seq_proof_generator.cpp	5266	log plain
-rw-r--r--	conv_seq_proof_generator.h	4889	log plain
d---------	dot	84	log plain
-rw-r--r--	eager_proof_generator.cpp	4814	log plain
-rw-r--r--	eager_proof_generator.h	7393	log plain
-rw-r--r--	lazy_proof.cpp	7508	log plain
-rw-r--r--	lazy_proof.h	4406	log plain
-rw-r--r--	lazy_proof_chain.cpp	11411	log plain
-rw-r--r--	lazy_proof_chain.h	6239	log plain
-rw-r--r--	lazy_tree_proof_generator.cpp	3999	log plain
-rw-r--r--	lazy_tree_proof_generator.h	7740	log plain
d---------	lean	226	log plain
d---------	lfsc	580	log plain
-rw-r--r--	method_id.cpp	3302	log plain
-rw-r--r--	method_id.h	3848	log plain
-rw-r--r--	print_expr.cpp	1365	log plain
-rw-r--r--	print_expr.h	2377	log plain
-rw-r--r--	proof.cpp	13696	log plain
-rw-r--r--	proof.h	12412	log plain
-rw-r--r--	proof_checker.cpp	10382	log plain
-rw-r--r--	proof_checker.h	7924	log plain
-rw-r--r--	proof_ensure_closed.cpp	5285	log plain
-rw-r--r--	proof_ensure_closed.h	2592	log plain
-rw-r--r--	proof_generator.cpp	2271	log plain
-rw-r--r--	proof_generator.h	4078	log plain
-rw-r--r--	proof_letify.cpp	3633	log plain
-rw-r--r--	proof_letify.h	3380	log plain
-rw-r--r--	proof_node.cpp	1813	log plain
-rw-r--r--	proof_node.h	5185	log plain
-rw-r--r--	proof_node_algorithm.cpp	7230	log plain
-rw-r--r--	proof_node_algorithm.h	3245	log plain
-rw-r--r--	proof_node_manager.cpp	12377	log plain
-rw-r--r--	proof_node_manager.h	8447	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	8689	log plain
-rw-r--r--	proof_node_to_sexpr.h	3908	log plain
-rw-r--r--	proof_node_updater.cpp	10245	log plain
-rw-r--r--	proof_node_updater.h	6190	log plain
-rw-r--r--	proof_rule.cpp	11592	log plain
-rw-r--r--	proof_rule.h	55847	log plain
-rw-r--r--	proof_set.h	2216	log plain
-rw-r--r--	proof_step_buffer.cpp	2983	log plain
-rw-r--r--	proof_step_buffer.h	2895	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	7260	log plain
-rw-r--r--	theory_proof_step_buffer.h	4930	log plain
-rw-r--r--	trust_node.cpp	4309	log plain
-rw-r--r--	trust_node.h	6134	log plain
-rw-r--r--	unsat_core.cpp	1772	log plain
-rw-r--r--	unsat_core.h	2077	log plain
d---------	verit	284	log plain