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	74601	log plain
-rw-r--r--	command.h	35810	log plain
-rw-r--r--	command.i	2743	log plain
-rw-r--r--	command_list.cpp	948	log plain
-rw-r--r--	command_list.h	1061	log plain
-rw-r--r--	dump.cpp	8925	log plain
-rw-r--r--	dump.h	3030	log plain
-rw-r--r--	logic_exception.h	1390	log plain
-rw-r--r--	logic_exception.i	133	log plain
-rw-r--r--	logic_request.cpp	1234	log plain
-rw-r--r--	logic_request.h	1651	log plain
-rw-r--r--	managed_ostreams.cpp	5741	log plain
-rw-r--r--	managed_ostreams.h	5642	log plain
-rw-r--r--	model.cpp	1604	log plain
-rw-r--r--	model.h	3733	log plain
-rw-r--r--	model_core_builder.cpp	2858	log plain
-rw-r--r--	model_core_builder.h	1754	log plain
-rw-r--r--	smt_engine.cpp	171266	log plain
-rw-r--r--	smt_engine.h	31975	log plain
-rw-r--r--	smt_engine.i	1330	log plain
-rw-r--r--	smt_engine_check_proof.cpp	3578	log plain
-rw-r--r--	smt_engine_scope.cpp	2040	log plain
-rw-r--r--	smt_engine_scope.h	1502	log plain
-rw-r--r--	smt_statistics_registry.cpp	890	log plain
-rw-r--r--	smt_statistics_registry.h	2362	log plain
-rw-r--r--	term_formula_removal.cpp	9918	log plain
-rw-r--r--	term_formula_removal.h	5042	log plain
-rw-r--r--	update_ostream.h	3974	log plain