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	7287	log plain
-rw-r--r--	abduction_solver.h	4718	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	7097	log plain
-rw-r--r--	assertions.h	6444	log plain
-rw-r--r--	check_models.cpp	5630	log plain
-rw-r--r--	check_models.h	1422	log plain
-rw-r--r--	command.cpp	81229	log plain
-rw-r--r--	command.h	47063	log plain
-rw-r--r--	difficulty_post_processor.cpp	2224	log plain
-rw-r--r--	difficulty_post_processor.h	3299	log plain
-rw-r--r--	dump.cpp	7340	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	3861	log plain
-rw-r--r--	env.h	6868	log plain
-rw-r--r--	env_obj.cpp	1393	log plain
-rw-r--r--	env_obj.h	1863	log plain
-rw-r--r--	expand_definitions.cpp	5680	log plain
-rw-r--r--	expand_definitions.h	2222	log plain
-rw-r--r--	interpolation_solver.cpp	4731	log plain
-rw-r--r--	interpolation_solver.h	3050	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--	model.cpp	2228	log plain
-rw-r--r--	model.h	3862	log plain
-rw-r--r--	model_blocker.cpp	8652	log plain
-rw-r--r--	model_blocker.h	2644	log plain
-rw-r--r--	model_core_builder.cpp	3168	log plain
-rw-r--r--	model_core_builder.h	2251	log plain
-rw-r--r--	node_command.cpp	5467	log plain
-rw-r--r--	node_command.h	3951	log plain
-rw-r--r--	optimization_solver.cpp	12725	log plain
-rw-r--r--	optimization_solver.h	10270	log plain
-rw-r--r--	output_manager.cpp	971	log plain
-rw-r--r--	output_manager.h	1421	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	4632	log plain
-rw-r--r--	preprocessor.h	4022	log plain
-rw-r--r--	process_assertions.cpp	14198	log plain
-rw-r--r--	process_assertions.h	3775	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	8010	log plain
-rw-r--r--	proof_manager.h	5071	log plain
-rw-r--r--	proof_post_processor.cpp	45567	log plain
-rw-r--r--	proof_post_processor.h	11846	log plain
-rw-r--r--	quant_elim_solver.cpp	4918	log plain
-rw-r--r--	quant_elim_solver.h	3817	log plain
-rw-r--r--	set_defaults.cpp	54958	log plain
-rw-r--r--	set_defaults.h	5395	log plain
-rw-r--r--	smt_engine.cpp	61265	log plain
-rw-r--r--	smt_engine.h	39342	log plain
-rw-r--r--	smt_engine_scope.cpp	1915	log plain
-rw-r--r--	smt_engine_scope.h	1595	log plain
-rw-r--r--	smt_engine_state.cpp	7803	log plain
-rw-r--r--	smt_engine_state.h	8703	log plain
-rw-r--r--	smt_engine_stats.cpp	1861	log plain
-rw-r--r--	smt_engine_stats.h	1761	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	7940	log plain
-rw-r--r--	smt_solver.h	4969	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	15582	log plain
-rw-r--r--	sygus_solver.h	7250	log plain
-rw-r--r--	term_formula_removal.cpp	19387	log plain
-rw-r--r--	term_formula_removal.h	7278	log plain
-rw-r--r--	unsat_core_manager.cpp	3654	log plain
-rw-r--r--	unsat_core_manager.h	2386	log plain
-rw-r--r--	witness_form.cpp	4357	log plain
-rw-r--r--	witness_form.h	3662	log plain