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	7028	log plain
-rw-r--r--	abduction_solver.h	4330	log plain
-rw-r--r--	abstract_values.cpp	1666	log plain
-rw-r--r--	abstract_values.h	2417	log plain
-rw-r--r--	assertions.cpp	6918	log plain
-rw-r--r--	assertions.h	6656	log plain
-rw-r--r--	command.cpp	99013	log plain
-rw-r--r--	command.h	54662	log plain
-rw-r--r--	defined_function.h	1749	log plain
-rw-r--r--	dump.cpp	9473	log plain
-rw-r--r--	dump.h	3487	log plain
-rw-r--r--	dump_manager.cpp	4114	log plain
-rw-r--r--	dump_manager.h	3227	log plain
-rw-r--r--	expr_names.cpp	1046	log plain
-rw-r--r--	expr_names.h	1569	log plain
-rw-r--r--	listeners.cpp	3069	log plain
-rw-r--r--	listeners.h	2153	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	4642	log plain
-rw-r--r--	model.cpp	1396	log plain
-rw-r--r--	model.h	4413	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--	node_command.cpp	6003	log plain
-rw-r--r--	node_command.h	4218	log plain
-rw-r--r--	options_manager.cpp	5576	log plain
-rw-r--r--	options_manager.h	2910	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--	preprocessor.cpp	4227	log plain
-rw-r--r--	preprocessor.h	4397	log plain
-rw-r--r--	process_assertions.cpp	26773	log plain
-rw-r--r--	process_assertions.h	5122	log plain
-rw-r--r--	proof_manager.cpp	5103	log plain
-rw-r--r--	proof_manager.h	3309	log plain
-rw-r--r--	proof_post_processor.cpp	22362	log plain
-rw-r--r--	proof_post_processor.h	7476	log plain
-rw-r--r--	quant_elim_solver.cpp	3718	log plain
-rw-r--r--	quant_elim_solver.h	3205	log plain
-rw-r--r--	set_defaults.cpp	46469	log plain
-rw-r--r--	set_defaults.h	1420	log plain
-rw-r--r--	smt_engine.cpp	69561	log plain
-rw-r--r--	smt_engine.h	41411	log plain
-rw-r--r--	smt_engine_scope.cpp	2223	log plain
-rw-r--r--	smt_engine_scope.h	1687	log plain
-rw-r--r--	smt_engine_state.cpp	7486	log plain
-rw-r--r--	smt_engine_state.h	8496	log plain
-rw-r--r--	smt_engine_stats.cpp	2954	log plain
-rw-r--r--	smt_engine_stats.h	1805	log plain
-rw-r--r--	smt_mode.cpp	1147	log plain
-rw-r--r--	smt_mode.h	1590	log plain
-rw-r--r--	smt_solver.cpp	8015	log plain
-rw-r--r--	smt_solver.h	5201	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--	sygus_solver.cpp	13835	log plain
-rw-r--r--	sygus_solver.h	6644	log plain
-rw-r--r--	term_formula_removal.cpp	17162	log plain
-rw-r--r--	term_formula_removal.h	6665	log plain
-rw-r--r--	update_ostream.h	3962	log plain
-rw-r--r--	witness_form.cpp	3990	log plain
-rw-r--r--	witness_form.h	3527	log plain