quantifiers « theory « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	Makefile	85	log plain
-rw-r--r--	Makefile.am	1263	log plain
-rwxr-xr-x	bounded_integers.cpp	15160	log plain
-rwxr-xr-x	bounded_integers.h	4404	log plain
-rw-r--r--	candidate_generator.cpp	6484	log plain
-rw-r--r--	candidate_generator.h	4181	log plain
-rw-r--r--	first_order_model.cpp	22655	log plain
-rw-r--r--	first_order_model.h	5386	log plain
-rwxr-xr-x	first_order_reasoning.cpp	5785	log plain
-rwxr-xr-x	first_order_reasoning.h	1206	log plain
-rwxr-xr-x	full_model_check.cpp	50572	log plain
-rwxr-xr-x	full_model_check.h	6044	log plain
-rw-r--r--	inst_gen.cpp	12341	log plain
-rw-r--r--	inst_gen.h	2055	log plain
-rw-r--r--	inst_match.cpp	11150	log plain
-rw-r--r--	inst_match.h	7401	log plain
-rw-r--r--	inst_match_generator.cpp	26849	log plain
-rw-r--r--	inst_match_generator.h	7715	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	12504	log plain
-rw-r--r--	inst_strategy_cbqi.h	3349	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	15675	log plain
-rw-r--r--	inst_strategy_e_matching.h	4693	log plain
-rw-r--r--	instantiation_engine.cpp	17497	log plain
-rw-r--r--	instantiation_engine.h	5138	log plain
-rw-r--r--	kinds	1822	log plain
-rw-r--r--	macros.cpp	13881	log plain
-rw-r--r--	macros.h	2032	log plain
-rw-r--r--	model_builder.cpp	46734	log plain
-rw-r--r--	model_builder.h	9738	log plain
-rw-r--r--	model_engine.cpp	10902	log plain
-rw-r--r--	model_engine.h	2154	log plain
-rw-r--r--	modes.cpp	2193	log plain
-rw-r--r--	modes.h	2101	log plain
-rw-r--r--	options	6835	log plain
-rw-r--r--	options_handlers.h	4925	log plain
-rw-r--r--	quant_util.cpp	7430	log plain
-rw-r--r--	quant_util.h	3657	log plain
-rw-r--r--	quantifiers_attributes.cpp	1353	log plain
-rw-r--r--	quantifiers_attributes.h	1448	log plain
-rw-r--r--	quantifiers_rewriter.cpp	33463	log plain
-rw-r--r--	quantifiers_rewriter.h	3235	log plain
-rwxr-xr-x	rewrite_engine.cpp	4256	log plain
-rwxr-xr-x	rewrite_engine.h	1457	log plain
-rw-r--r--	term_database.cpp	21417	log plain
-rw-r--r--	term_database.h	9833	log plain
-rw-r--r--	theory_quantifiers.cpp	6391	log plain
-rw-r--r--	theory_quantifiers.h	2567	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	4368	log plain
-rw-r--r--	trigger.cpp	17452	log plain
-rw-r--r--	trigger.h	5717	log plain