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--	arith_proof.cpp	31774	log plain
-rw-r--r--	arith_proof.h	2764	log plain
-rw-r--r--	array_proof.cpp	54242	log plain
-rw-r--r--	array_proof.h	4505	log plain
-rw-r--r--	bitvector_proof.cpp	36895	log plain
-rw-r--r--	bitvector_proof.h	6182	log plain
-rw-r--r--	clause_id.h	953	log plain
-rw-r--r--	cnf_proof.cpp	31458	log plain
-rw-r--r--	cnf_proof.h	6818	log plain
-rw-r--r--	lemma_proof.cpp	6176	log plain
-rw-r--r--	lemma_proof.h	2669	log plain
-rw-r--r--	proof.h	2339	log plain
-rw-r--r--	proof_manager.cpp	38126	log plain
-rw-r--r--	proof_manager.h	10255	log plain
-rw-r--r--	proof_output_channel.cpp	2726	log plain
-rw-r--r--	proof_output_channel.h	1776	log plain
-rw-r--r--	proof_utils.cpp	3517	log plain
-rw-r--r--	proof_utils.h	5458	log plain
-rw-r--r--	sat_proof.h	13481	log plain
-rw-r--r--	sat_proof_implementation.h	38943	log plain
-rw-r--r--	simplify_boolean_node.cpp	6896	log plain
-rw-r--r--	simplify_boolean_node.h	827	log plain
-rw-r--r--	skolemization_manager.cpp	2318	log plain
-rw-r--r--	skolemization_manager.h	1521	log plain
-rw-r--r--	theory_proof.cpp	44664	log plain
-rw-r--r--	theory_proof.h	11028	log plain
-rw-r--r--	uf_proof.cpp	33942	log plain
-rw-r--r--	uf_proof.h	2757	log plain
-rw-r--r--	unsat_core.cpp	1653	log plain
-rw-r--r--	unsat_core.h	1874	log plain
-rw-r--r--	unsat_core.i	2278	log plain