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	32325	log plain
-rw-r--r--	arith_proof.h	3394	log plain
-rw-r--r--	arith_proof_recorder.cpp	2493	log plain
-rw-r--r--	arith_proof_recorder.h	3674	log plain
-rw-r--r--	array_proof.cpp	47321	log plain
-rw-r--r--	array_proof.h	3894	log plain
-rw-r--r--	bitvector_proof.cpp	23656	log plain
-rw-r--r--	bitvector_proof.h	7320	log plain
-rw-r--r--	clause_id.h	953	log plain
-rw-r--r--	cnf_proof.cpp	31800	log plain
-rw-r--r--	cnf_proof.h	6993	log plain
-rw-r--r--	lemma_proof.cpp	7586	log plain
-rw-r--r--	lemma_proof.h	3588	log plain
-rw-r--r--	lfsc_proof_printer.cpp	5623	log plain
-rw-r--r--	lfsc_proof_printer.h	3417	log plain
-rw-r--r--	proof.h	2343	log plain
-rw-r--r--	proof_manager.cpp	38433	log plain
-rw-r--r--	proof_manager.h	10422	log plain
-rw-r--r--	proof_output_channel.cpp	2996	log plain
-rw-r--r--	proof_output_channel.h	2270	log plain
-rw-r--r--	proof_utils.cpp	3517	log plain
-rw-r--r--	proof_utils.h	5326	log plain
-rw-r--r--	resolution_bitvector_proof.cpp	16874	log plain
-rw-r--r--	resolution_bitvector_proof.h	3772	log plain
-rw-r--r--	sat_proof.h	11548	log plain
-rw-r--r--	sat_proof_implementation.h	34486	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	2328	log plain
-rw-r--r--	skolemization_manager.h	1531	log plain
-rw-r--r--	theory_proof.cpp	57036	log plain
-rw-r--r--	theory_proof.h	12835	log plain
-rw-r--r--	uf_proof.cpp	26704	log plain
-rw-r--r--	uf_proof.h	3399	log plain
-rw-r--r--	unsat_core.cpp	1465	log plain
-rw-r--r--	unsat_core.h	1925	log plain
-rw-r--r--	unsat_core.i	2278	log plain