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

Mode	Name	Size
d---------	alethe	304	log plain
-rw-r--r--	assumption_proof_generator.cpp	998	log plain
-rw-r--r--	assumption_proof_generator.h	1361	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	7776	log plain
-rw-r--r--	lazy_proof.h	4611	log plain
-rw-r--r--	lazy_proof_chain.cpp	11422	log plain
-rw-r--r--	lazy_proof_chain.h	6239	log plain
-rw-r--r--	lazy_tree_proof_generator.cpp	4084	log plain
-rw-r--r--	lazy_tree_proof_generator.h	8006	log plain
d---------	lfsc	580	log plain
-rw-r--r--	method_id.cpp	3302	log plain
-rw-r--r--	method_id.h	3861	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	13843	log plain
-rw-r--r--	proof.h	12412	log plain
-rw-r--r--	proof_checker.cpp	10421	log plain
-rw-r--r--	proof_checker.h	8048	log plain
-rw-r--r--	proof_ensure_closed.cpp	5310	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	1842	log plain
-rw-r--r--	proof_node.h	5267	log plain
-rw-r--r--	proof_node_algorithm.cpp	10369	log plain
-rw-r--r--	proof_node_algorithm.h	4641	log plain
-rw-r--r--	proof_node_manager.cpp	14426	log plain
-rw-r--r--	proof_node_manager.h	9365	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	8575	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	11160	log plain
-rw-r--r--	proof_rule.h	54474	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	1775	log plain
-rw-r--r--	unsat_core.h	2077	log plain