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	88297	log plain
-rw-r--r--	command.h	46576	log plain
-rw-r--r--	command.i	2477	log plain
-rw-r--r--	command_list.cpp	938	log plain
-rw-r--r--	command_list.h	1055	log plain
-rw-r--r--	dump.cpp	9472	log plain
-rw-r--r--	dump.h	3012	log plain
-rw-r--r--	logic_exception.h	1374	log plain
-rw-r--r--	logic_exception.i	133	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	5765	log plain
-rw-r--r--	managed_ostreams.h	5636	log plain
-rw-r--r--	model.cpp	1623	log plain
-rw-r--r--	model.h	4537	log plain
-rw-r--r--	model_blocker.cpp	8909	log plain
-rw-r--r--	model_blocker.h	2588	log plain
-rw-r--r--	model_core_builder.cpp	3298	log plain
-rw-r--r--	model_core_builder.h	2199	log plain
-rw-r--r--	smt_engine.cpp	197506	log plain
-rw-r--r--	smt_engine.h	43918	log plain
-rw-r--r--	smt_engine.i	1390	log plain
-rw-r--r--	smt_engine_scope.cpp	2054	log plain
-rw-r--r--	smt_engine_scope.h	1496	log plain
-rw-r--r--	smt_statistics_registry.cpp	890	log plain
-rw-r--r--	smt_statistics_registry.h	973	log plain
-rw-r--r--	term_formula_removal.cpp	10033	log plain
-rw-r--r--	term_formula_removal.h	5042	log plain
-rw-r--r--	update_ostream.h	3962	log plain