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	7457	log plain
-rw-r--r--	abduction_solver.h	4730	log plain
-rw-r--r--	abstract_values.cpp	1717	log plain
-rw-r--r--	abstract_values.h	2438	log plain
-rw-r--r--	assertions.cpp	7658	log plain
-rw-r--r--	assertions.h	7280	log plain
-rw-r--r--	check_models.cpp	5912	log plain
-rw-r--r--	check_models.h	1379	log plain
-rw-r--r--	command.cpp	79545	log plain
-rw-r--r--	command.h	45837	log plain
-rw-r--r--	difficulty_post_processor.cpp	2240	log plain
-rw-r--r--	difficulty_post_processor.h	3299	log plain
-rw-r--r--	env.cpp	6586	log plain
-rw-r--r--	env.h	11138	log plain
-rw-r--r--	env_obj.cpp	2538	log plain
-rw-r--r--	env_obj.h	3199	log plain
-rw-r--r--	expand_definitions.cpp	5597	log plain
-rw-r--r--	expand_definitions.h	2094	log plain
-rw-r--r--	interpolation_solver.cpp	4796	log plain
-rw-r--r--	interpolation_solver.h	3056	log plain
-rw-r--r--	listeners.cpp	983	log plain
-rw-r--r--	listeners.h	1175	log plain
-rw-r--r--	logic_exception.h	1287	log plain
-rw-r--r--	model.cpp	2228	log plain
-rw-r--r--	model.h	3862	log plain
-rw-r--r--	model_blocker.cpp	8685	log plain
-rw-r--r--	model_blocker.h	2705	log plain
-rw-r--r--	model_core_builder.cpp	3201	log plain
-rw-r--r--	model_core_builder.h	2304	log plain
-rw-r--r--	optimization_solver.cpp	12740	log plain
-rw-r--r--	optimization_solver.h	10291	log plain
-rw-r--r--	preprocess_proof_generator.cpp	8558	log plain
-rw-r--r--	preprocess_proof_generator.h	5541	log plain
-rw-r--r--	preprocessor.cpp	4395	log plain
-rw-r--r--	preprocessor.h	4030	log plain
-rw-r--r--	print_benchmark.cpp	8155	log plain
-rw-r--r--	print_benchmark.h	5103	log plain
-rw-r--r--	process_assertions.cpp	15484	log plain
-rw-r--r--	process_assertions.h	3714	log plain
-rw-r--r--	proof_final_callback.cpp	3313	log plain
-rw-r--r--	proof_final_callback.h	2439	log plain
-rw-r--r--	proof_manager.cpp	10767	log plain
-rw-r--r--	proof_manager.h	5906	log plain
-rw-r--r--	proof_post_processor.cpp	47276	log plain
-rw-r--r--	proof_post_processor.h	11858	log plain
-rw-r--r--	quant_elim_solver.cpp	5183	log plain
-rw-r--r--	quant_elim_solver.h	3826	log plain
-rw-r--r--	set_defaults.cpp	55212	log plain
-rw-r--r--	set_defaults.h	5464	log plain
-rw-r--r--	smt_mode.cpp	1168	log plain
-rw-r--r--	smt_mode.h	1640	log plain
-rw-r--r--	smt_solver.cpp	8137	log plain
-rw-r--r--	smt_solver.h	4939	log plain
-rw-r--r--	smt_statistics_registry.cpp	846	log plain
-rw-r--r--	smt_statistics_registry.h	958	log plain
-rw-r--r--	solver_engine.cpp	55838	log plain
-rw-r--r--	solver_engine.h	39295	log plain
-rw-r--r--	solver_engine_scope.cpp	1980	log plain
-rw-r--r--	solver_engine_scope.h	1635	log plain
-rw-r--r--	solver_engine_state.cpp	7715	log plain
-rw-r--r--	solver_engine_state.h	8603	log plain
-rw-r--r--	solver_engine_stats.cpp	1870	log plain
-rw-r--r--	solver_engine_stats.h	1779	log plain
-rw-r--r--	sygus_solver.cpp	15787	log plain
-rw-r--r--	sygus_solver.h	7211	log plain
-rw-r--r--	term_formula_removal.cpp	18418	log plain
-rw-r--r--	term_formula_removal.h	8046	log plain
-rw-r--r--	unsat_core_manager.cpp	3572	log plain
-rw-r--r--	unsat_core_manager.h	2392	log plain
-rw-r--r--	witness_form.cpp	4512	log plain
-rw-r--r--	witness_form.h	3767	log plain