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	32038	log plain
-rw-r--r--	arith_proof.h	2739	log plain
-rw-r--r--	array_proof.cpp	53143	log plain
-rw-r--r--	array_proof.h	4443	log plain
-rw-r--r--	bitvector_proof.cpp	36908	log plain
-rw-r--r--	bitvector_proof.h	6172	log plain
-rw-r--r--	clause_id.h	952	log plain
-rw-r--r--	cnf_proof.cpp	31333	log plain
-rw-r--r--	cnf_proof.h	6819	log plain
-rw-r--r--	lemma_proof.cpp	5888	log plain
-rw-r--r--	lemma_proof.h	2382	log plain
-rw-r--r--	proof.h	2351	log plain
-rw-r--r--	proof_manager.cpp	35875	log plain
-rw-r--r--	proof_manager.h	9813	log plain
-rw-r--r--	proof_output_channel.cpp	2342	log plain
-rw-r--r--	proof_output_channel.h	1329	log plain
-rw-r--r--	proof_utils.cpp	3291	log plain
-rw-r--r--	proof_utils.h	5369	log plain
-rw-r--r--	sat_proof.h	13233	log plain
-rw-r--r--	sat_proof_implementation.h	38169	log plain
-rw-r--r--	skolemization_manager.cpp	2307	log plain
-rw-r--r--	skolemization_manager.h	1490	log plain
-rw-r--r--	theory_proof.cpp	42690	log plain
-rw-r--r--	theory_proof.h	10920	log plain
-rw-r--r--	uf_proof.cpp	31005	log plain
-rw-r--r--	uf_proof.h	2587	log plain
-rw-r--r--	unsat_core.cpp	1657	log plain
-rw-r--r--	unsat_core.h	1892	log plain
-rw-r--r--	unsat_core.i	2278	log plain