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	6910	log plain
-rw-r--r--	abduction_solver.h	4358	log plain
-rw-r--r--	abstract_values.cpp	1671	log plain
-rw-r--r--	abstract_values.h	2441	log plain
-rw-r--r--	assertions.cpp	6982	log plain
-rw-r--r--	assertions.h	6647	log plain
-rw-r--r--	check_models.cpp	5770	log plain
-rw-r--r--	check_models.h	1342	log plain
-rw-r--r--	command.cpp	82730	log plain
-rw-r--r--	command.h	47709	log plain
-rw-r--r--	defined_function.h	1754	log plain
-rw-r--r--	dump.cpp	7490	log plain
-rw-r--r--	dump.h	3204	log plain
-rw-r--r--	dump_manager.cpp	1848	log plain
-rw-r--r--	dump_manager.h	2049	log plain
-rw-r--r--	env.cpp	2866	log plain
-rw-r--r--	env.h	5790	log plain
-rw-r--r--	expand_definitions.cpp	12596	log plain
-rw-r--r--	expand_definitions.h	2843	log plain
-rw-r--r--	interpolation_solver.cpp	4500	log plain
-rw-r--r--	interpolation_solver.h	2896	log plain
-rw-r--r--	listeners.cpp	3097	log plain
-rw-r--r--	listeners.h	2303	log plain
-rw-r--r--	logic_exception.h	1378	log plain
-rw-r--r--	managed_ostreams.cpp	5032	log plain
-rw-r--r--	managed_ostreams.h	4610	log plain
-rw-r--r--	model.cpp	2031	log plain
-rw-r--r--	model.h	3844	log plain
-rw-r--r--	model_blocker.cpp	8721	log plain
-rw-r--r--	model_blocker.h	2627	log plain
-rw-r--r--	model_core_builder.cpp	3085	log plain
-rw-r--r--	model_core_builder.h	2239	log plain
-rw-r--r--	node_command.cpp	5525	log plain
-rw-r--r--	node_command.h	3927	log plain
-rw-r--r--	optimization_solver.cpp	2782	log plain
-rw-r--r--	optimization_solver.h	4383	log plain
-rw-r--r--	options_manager.cpp	4985	log plain
-rw-r--r--	options_manager.h	2920	log plain
-rw-r--r--	output_manager.cpp	958	log plain
-rw-r--r--	output_manager.h	1409	log plain
-rw-r--r--	preprocess_proof_generator.cpp	7948	log plain
-rw-r--r--	preprocess_proof_generator.h	5583	log plain
-rw-r--r--	preprocessor.cpp	4592	log plain
-rw-r--r--	preprocessor.h	4127	log plain
-rw-r--r--	process_assertions.cpp	14397	log plain
-rw-r--r--	process_assertions.h	3930	log plain
-rw-r--r--	proof_manager.cpp	7828	log plain
-rw-r--r--	proof_manager.h	4121	log plain
-rw-r--r--	proof_post_processor.cpp	44307	log plain
-rw-r--r--	proof_post_processor.h	13269	log plain
-rw-r--r--	quant_elim_solver.cpp	5131	log plain
-rw-r--r--	quant_elim_solver.h	3750	log plain
-rw-r--r--	set_defaults.cpp	48481	log plain
-rw-r--r--	set_defaults.h	1419	log plain
-rw-r--r--	smt_engine.cpp	60923	log plain
-rw-r--r--	smt_engine.h	41277	log plain
-rw-r--r--	smt_engine_scope.cpp	2039	log plain
-rw-r--r--	smt_engine_scope.h	1679	log plain
-rw-r--r--	smt_engine_state.cpp	7840	log plain
-rw-r--r--	smt_engine_state.h	9230	log plain
-rw-r--r--	smt_engine_stats.cpp	3464	log plain
-rw-r--r--	smt_engine_stats.h	2060	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	9616	log plain
-rw-r--r--	smt_solver.h	5478	log plain
-rw-r--r--	smt_statistics_registry.cpp	887	log plain
-rw-r--r--	smt_statistics_registry.h	956	log plain
-rw-r--r--	sygus_solver.cpp	14071	log plain
-rw-r--r--	sygus_solver.h	6932	log plain
-rw-r--r--	term_formula_removal.cpp	19438	log plain
-rw-r--r--	term_formula_removal.h	7435	log plain
-rw-r--r--	unsat_core_manager.cpp	2875	log plain
-rw-r--r--	unsat_core_manager.h	2256	log plain
-rw-r--r--	update_ostream.h	3823	log plain
-rw-r--r--	witness_form.cpp	4378	log plain
-rw-r--r--	witness_form.h	3707	log plain