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--	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	7508	log plain
-rw-r--r--	lazy_proof.h	4406	log plain
-rw-r--r--	lazy_proof_chain.cpp	11411	log plain
-rw-r--r--	lazy_proof_chain.h	6239	log plain
-rw-r--r--	lazy_tree_proof_generator.cpp	3999	log plain
-rw-r--r--	lazy_tree_proof_generator.h	7740	log plain
-rw-r--r--	method_id.cpp	3302	log plain
-rw-r--r--	method_id.h	3848	log plain
-rw-r--r--	proof.cpp	13696	log plain
-rw-r--r--	proof.h	12412	log plain
-rw-r--r--	proof_checker.cpp	10153	log plain
-rw-r--r--	proof_checker.h	7721	log plain
-rw-r--r--	proof_ensure_closed.cpp	5285	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_node.cpp	1813	log plain
-rw-r--r--	proof_node.h	5185	log plain
-rw-r--r--	proof_node_algorithm.cpp	5401	log plain
-rw-r--r--	proof_node_algorithm.h	2413	log plain
-rw-r--r--	proof_node_manager.cpp	12377	log plain
-rw-r--r--	proof_node_manager.h	8447	log plain
-rw-r--r--	proof_node_to_sexpr.cpp	4370	log plain
-rw-r--r--	proof_node_to_sexpr.h	2127	log plain
-rw-r--r--	proof_node_updater.cpp	8910	log plain
-rw-r--r--	proof_node_updater.h	6176	log plain
-rw-r--r--	proof_rule.cpp	13401	log plain
-rw-r--r--	proof_rule.h	53587	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	4119	log plain
-rw-r--r--	trust_node.h	5948	log plain
-rw-r--r--	unsat_core.cpp	1772	log plain
-rw-r--r--	unsat_core.h	2077	log plain