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	6922	log plain
-rw-r--r--	abduction_solver.h	4372	log plain
-rw-r--r--	abstract_values.cpp	1683	log plain
-rw-r--r--	abstract_values.h	2455	log plain
-rw-r--r--	assertions.cpp	7020	log plain
-rw-r--r--	assertions.h	6666	log plain
-rw-r--r--	check_models.cpp	5785	log plain
-rw-r--r--	check_models.h	1360	log plain
-rw-r--r--	command.cpp	84481	log plain
-rw-r--r--	command.h	48495	log plain
-rw-r--r--	defined_function.h	1768	log plain
-rw-r--r--	dump.cpp	7470	log plain
-rw-r--r--	dump.h	3190	log plain
-rw-r--r--	dump_manager.cpp	1863	log plain
-rw-r--r--	dump_manager.h	2066	log plain
-rw-r--r--	env.cpp	2874	log plain
-rw-r--r--	env.h	5823	log plain
-rw-r--r--	expand_definitions.cpp	12649	log plain
-rw-r--r--	expand_definitions.h	2854	log plain
-rw-r--r--	interpolation_solver.cpp	4502	log plain
-rw-r--r--	interpolation_solver.h	2906	log plain
-rw-r--r--	listeners.cpp	3115	log plain
-rw-r--r--	listeners.h	2323	log plain
-rw-r--r--	logic_exception.h	1287	log plain
-rw-r--r--	managed_ostreams.cpp	5080	log plain
-rw-r--r--	managed_ostreams.h	4620	log plain
-rw-r--r--	model.cpp	2054	log plain
-rw-r--r--	model.h	3869	log plain
-rw-r--r--	model_blocker.cpp	8745	log plain
-rw-r--r--	model_blocker.h	2644	log plain
-rw-r--r--	model_core_builder.cpp	3109	log plain
-rw-r--r--	model_core_builder.h	2251	log plain
-rw-r--r--	node_command.cpp	5491	log plain
-rw-r--r--	node_command.h	3882	log plain
-rw-r--r--	optimization_solver.cpp	2805	log plain
-rw-r--r--	optimization_solver.h	4407	log plain
-rw-r--r--	options_manager.cpp	4359	log plain
-rw-r--r--	options_manager.h	2824	log plain
-rw-r--r--	output_manager.cpp	937	log plain
-rw-r--r--	output_manager.h	1421	log plain
-rw-r--r--	preprocess_proof_generator.cpp	7948	log plain
-rw-r--r--	preprocess_proof_generator.h	5586	log plain
-rw-r--r--	preprocessor.cpp	4601	log plain
-rw-r--r--	preprocessor.h	4144	log plain
-rw-r--r--	process_assertions.cpp	14236	log plain
-rw-r--r--	process_assertions.h	3923	log plain
-rw-r--r--	proof_manager.cpp	7970	log plain
-rw-r--r--	proof_manager.h	5357	log plain
-rw-r--r--	proof_post_processor.cpp	44727	log plain
-rw-r--r--	proof_post_processor.h	13232	log plain
-rw-r--r--	quant_elim_solver.cpp	5156	log plain
-rw-r--r--	quant_elim_solver.h	3763	log plain
-rw-r--r--	set_defaults.cpp	51574	log plain
-rw-r--r--	set_defaults.h	1436	log plain
-rw-r--r--	smt_engine.cpp	62011	log plain
-rw-r--r--	smt_engine.h	41813	log plain
-rw-r--r--	smt_engine_scope.cpp	2044	log plain
-rw-r--r--	smt_engine_scope.h	1689	log plain
-rw-r--r--	smt_engine_state.cpp	7851	log plain
-rw-r--r--	smt_engine_state.h	9244	log plain
-rw-r--r--	smt_engine_stats.cpp	1966	log plain
-rw-r--r--	smt_engine_stats.h	1832	log plain
-rw-r--r--	smt_mode.cpp	1165	log plain
-rw-r--r--	smt_mode.h	1637	log plain
-rw-r--r--	smt_solver.cpp	9091	log plain
-rw-r--r--	smt_solver.h	5547	log plain
-rw-r--r--	smt_statistics_registry.cpp	831	log plain
-rw-r--r--	smt_statistics_registry.h	940	log plain
-rw-r--r--	sygus_solver.cpp	14087	log plain
-rw-r--r--	sygus_solver.h	6950	log plain
-rw-r--r--	term_formula_removal.cpp	19412	log plain
-rw-r--r--	term_formula_removal.h	7411	log plain
-rw-r--r--	unsat_core_manager.cpp	2884	log plain
-rw-r--r--	unsat_core_manager.h	2267	log plain
-rw-r--r--	update_ostream.h	3855	log plain
-rw-r--r--	witness_form.cpp	4394	log plain
-rw-r--r--	witness_form.h	3725	log plain