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	42990	log plain
-rw-r--r--	arith_proof.h	5498	log plain
-rw-r--r--	arith_proof_recorder.cpp	2862	log plain
-rw-r--r--	arith_proof_recorder.h	3670	log plain
-rw-r--r--	array_proof.cpp	47327	log plain
-rw-r--r--	array_proof.h	3889	log plain
-rw-r--r--	bitvector_proof.cpp	23903	log plain
-rw-r--r--	bitvector_proof.h	9626	log plain
-rw-r--r--	clausal_bitvector_proof.cpp	11105	log plain
-rw-r--r--	clausal_bitvector_proof.h	4397	log plain
-rw-r--r--	clause_id.h	947	log plain
-rw-r--r--	cnf_proof.cpp	34942	log plain
-rw-r--r--	cnf_proof.h	7889	log plain
-rw-r--r--	dimacs.cpp	2697	log plain
-rw-r--r--	dimacs.h	1845	log plain
d---------	drat	82	log plain
d---------	er	78	log plain
-rw-r--r--	lemma_proof.cpp	7600	log plain
-rw-r--r--	lemma_proof.h	3596	log plain
-rw-r--r--	lfsc_proof_printer.cpp	7176	log plain
-rw-r--r--	lfsc_proof_printer.h	5229	log plain
d---------	lrat	82	log plain
-rw-r--r--	proof.h	2337	log plain
-rw-r--r--	proof_manager.cpp	38869	log plain
-rw-r--r--	proof_manager.h	10864	log plain
-rw-r--r--	proof_output_channel.cpp	3012	log plain
-rw-r--r--	proof_output_channel.h	2280	log plain
-rw-r--r--	proof_utils.cpp	3517	log plain
-rw-r--r--	proof_utils.h	5333	log plain
-rw-r--r--	resolution_bitvector_proof.cpp	16965	log plain
-rw-r--r--	resolution_bitvector_proof.h	3496	log plain
-rw-r--r--	sat_proof.h	11548	log plain
-rw-r--r--	sat_proof_implementation.h	34480	log plain
-rw-r--r--	simplify_boolean_node.cpp	6929	log plain
-rw-r--r--	simplify_boolean_node.h	821	log plain
-rw-r--r--	skolemization_manager.cpp	2328	log plain
-rw-r--r--	skolemization_manager.h	1525	log plain
-rw-r--r--	theory_proof.cpp	58089	log plain
-rw-r--r--	theory_proof.h	12829	log plain
-rw-r--r--	uf_proof.cpp	26770	log plain
-rw-r--r--	uf_proof.h	3393	log plain
-rw-r--r--	unsat_core.cpp	1465	log plain
-rw-r--r--	unsat_core.h	1919	log plain
-rw-r--r--	unsat_core.i	2088	log plain