smt « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	abduction_solver.cpp	7059	log plain
-rw-r--r--	abduction_solver.h	4358	log plain
-rw-r--r--	abstract_values.cpp	1680	log plain
-rw-r--r--	abstract_values.h	2441	log plain
-rw-r--r--	assertions.cpp	6877	log plain
-rw-r--r--	assertions.h	6686	log plain
-rw-r--r--	command.cpp	98750	log plain
-rw-r--r--	command.h	54665	log plain
-rw-r--r--	defined_function.h	1748	log plain
-rw-r--r--	dump.cpp	7256	log plain
-rw-r--r--	dump.h	3253	log plain
-rw-r--r--	dump_manager.cpp	4170	log plain
-rw-r--r--	dump_manager.h	3252	log plain
-rw-r--r--	expr_names.cpp	1045	log plain
-rw-r--r--	expr_names.h	1598	log plain
-rw-r--r--	interpolation_solver.cpp	4644	log plain
-rw-r--r--	interpolation_solver.h	2865	log plain
-rw-r--r--	listeners.cpp	3285	log plain
-rw-r--r--	listeners.h	2299	log plain
-rw-r--r--	logic_exception.h	1390	log plain
-rw-r--r--	logic_request.cpp	1264	log plain
-rw-r--r--	logic_request.h	1661	log plain
-rw-r--r--	managed_ostreams.cpp	5006	log plain
-rw-r--r--	managed_ostreams.h	4641	log plain
-rw-r--r--	model.cpp	1395	log plain
-rw-r--r--	model.h	4412	log plain
-rw-r--r--	model_blocker.cpp	8925	log plain
-rw-r--r--	model_blocker.h	2604	log plain
-rw-r--r--	model_core_builder.cpp	3314	log plain
-rw-r--r--	model_core_builder.h	2215	log plain
-rw-r--r--	node_command.cpp	6137	log plain
-rw-r--r--	node_command.h	4217	log plain
-rw-r--r--	options_manager.cpp	5575	log plain
-rw-r--r--	options_manager.h	2919	log plain
-rw-r--r--	output_manager.cpp	961	log plain
-rw-r--r--	output_manager.h	1409	log plain
-rw-r--r--	preprocess_proof_generator.cpp	3971	log plain
-rw-r--r--	preprocess_proof_generator.h	2782	log plain
-rw-r--r--	preprocessor.cpp	4341	log plain
-rw-r--r--	preprocessor.h	4427	log plain
-rw-r--r--	process_assertions.cpp	26872	log plain
-rw-r--r--	process_assertions.h	5121	log plain
-rw-r--r--	proof_manager.cpp	5102	log plain
-rw-r--r--	proof_manager.h	3308	log plain
-rw-r--r--	proof_post_processor.cpp	22866	log plain
-rw-r--r--	proof_post_processor.h	7943	log plain
-rw-r--r--	quant_elim_solver.cpp	3734	log plain
-rw-r--r--	quant_elim_solver.h	3204	log plain
-rw-r--r--	set_defaults.cpp	46615	log plain
-rw-r--r--	set_defaults.h	1419	log plain
-rw-r--r--	smt_engine.cpp	71529	log plain
-rw-r--r--	smt_engine.h	41917	log plain
-rw-r--r--	smt_engine_scope.cpp	2222	log plain
-rw-r--r--	smt_engine_scope.h	1688	log plain
-rw-r--r--	smt_engine_state.cpp	7794	log plain
-rw-r--r--	smt_engine_state.h	9219	log plain
-rw-r--r--	smt_engine_stats.cpp	2954	log plain
-rw-r--r--	smt_engine_stats.h	1798	log plain
-rw-r--r--	smt_mode.cpp	1146	log plain
-rw-r--r--	smt_mode.h	1616	log plain
-rw-r--r--	smt_solver.cpp	8435	log plain
-rw-r--r--	smt_solver.h	5229	log plain
-rw-r--r--	smt_statistics_registry.cpp	889	log plain
-rw-r--r--	smt_statistics_registry.h	957	log plain
-rw-r--r--	sygus_solver.cpp	14073	log plain
-rw-r--r--	sygus_solver.h	6848	log plain
-rw-r--r--	term_formula_removal.cpp	19350	log plain
-rw-r--r--	term_formula_removal.h	7023	log plain
-rw-r--r--	update_ostream.h	3961	log plain
-rw-r--r--	witness_form.cpp	4135	log plain
-rw-r--r--	witness_form.h	3526	log plain