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--	command.cpp	80937	log plain
-rw-r--r--	command.h	46117	log plain
-rw-r--r--	command_list.cpp	938	log plain
-rw-r--r--	command_list.h	1072	log plain
-rw-r--r--	defined_function.h	1749	log plain
-rw-r--r--	dump.cpp	9473	log plain
-rw-r--r--	dump.h	3012	log plain
-rw-r--r--	logic_exception.h	1391	log plain
-rw-r--r--	logic_request.cpp	1265	log plain
-rw-r--r--	logic_request.h	1662	log plain
-rw-r--r--	managed_ostreams.cpp	5007	log plain
-rw-r--r--	managed_ostreams.h	4955	log plain
-rw-r--r--	model.cpp	1623	log plain
-rw-r--r--	model.h	4554	log plain
-rw-r--r--	model_blocker.cpp	8926	log plain
-rw-r--r--	model_blocker.h	2605	log plain
-rw-r--r--	model_core_builder.cpp	3315	log plain
-rw-r--r--	model_core_builder.h	2216	log plain
-rw-r--r--	preprocess_proof_generator.cpp	3972	log plain
-rw-r--r--	preprocess_proof_generator.h	2783	log plain
-rw-r--r--	process_assertions.cpp	27240	log plain
-rw-r--r--	process_assertions.h	5071	log plain
-rw-r--r--	set_defaults.cpp	48808	log plain
-rw-r--r--	set_defaults.h	1421	log plain
-rw-r--r--	smt_engine.cpp	125490	log plain
-rw-r--r--	smt_engine.h	48451	log plain
-rw-r--r--	smt_engine_scope.cpp	2248	log plain
-rw-r--r--	smt_engine_scope.h	1687	log plain
-rw-r--r--	smt_engine_stats.cpp	3509	log plain
-rw-r--r--	smt_engine_stats.h	2038	log plain
-rw-r--r--	smt_statistics_registry.cpp	890	log plain
-rw-r--r--	smt_statistics_registry.h	958	log plain
-rw-r--r--	term_formula_removal.cpp	10051	log plain
-rw-r--r--	term_formula_removal.h	5043	log plain
-rw-r--r--	update_ostream.h	3962	log plain