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--	ambqi_builder.cpp	36736	log plain
-rw-r--r--	ambqi_builder.h	4345	log plain
-rw-r--r--	bounded_integers.cpp	17459	log plain
-rw-r--r--	bounded_integers.h	4663	log plain
-rw-r--r--	candidate_generator.cpp	6847	log plain
-rw-r--r--	candidate_generator.h	4520	log plain
-rw-r--r--	ce_guided_instantiation.cpp	21592	log plain
-rw-r--r--	ce_guided_instantiation.h	4670	log plain
-rw-r--r--	ce_guided_single_inv.cpp	35154	log plain
-rw-r--r--	ce_guided_single_inv.h	4022	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	40568	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3295	log plain
-rwxr-xr-x	conjecture_generator.cpp	87119	log plain
-rwxr-xr-x	conjecture_generator.h	16221	log plain
-rw-r--r--	first_order_model.cpp	30434	log plain
-rw-r--r--	first_order_model.h	8237	log plain
-rw-r--r--	first_order_reasoning.cpp	5680	log plain
-rw-r--r--	first_order_reasoning.h	1222	log plain
-rw-r--r--	full_model_check.cpp	54755	log plain
-rw-r--r--	full_model_check.h	6356	log plain
-rw-r--r--	fun_def_process.cpp	8001	log plain
-rw-r--r--	fun_def_process.h	1450	log plain
-rw-r--r--	inst_match.cpp	8796	log plain
-rw-r--r--	inst_match.h	7165	log plain
-rw-r--r--	inst_match_generator.cpp	30924	log plain
-rw-r--r--	inst_match_generator.h	9623	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	14145	log plain
-rw-r--r--	inst_strategy_cbqi.h	2654	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	23657	log plain
-rw-r--r--	inst_strategy_e_matching.h	4967	log plain
-rw-r--r--	instantiation_engine.cpp	17136	log plain
-rw-r--r--	instantiation_engine.h	4594	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9180	log plain
-rw-r--r--	local_theory_ext.h	2678	log plain
-rw-r--r--	macros.cpp	10582	log plain
-rw-r--r--	macros.h	1894	log plain
-rw-r--r--	model_builder.cpp	32486	log plain
-rw-r--r--	model_builder.h	7270	log plain
-rw-r--r--	model_engine.cpp	11705	log plain
-rw-r--r--	model_engine.h	2156	log plain
-rw-r--r--	modes.cpp	2731	log plain
-rw-r--r--	modes.h	4336	log plain
-rw-r--r--	options	14668	log plain
-rw-r--r--	options_handlers.h	13647	log plain
-rwxr-xr-x	quant_conflict_find.cpp	83647	log plain
-rwxr-xr-x	quant_conflict_find.h	8505	log plain
-rw-r--r--	quant_util.cpp	11544	log plain
-rw-r--r--	quant_util.h	4072	log plain
-rw-r--r--	quantifiers_attributes.cpp	2500	log plain
-rw-r--r--	quantifiers_attributes.h	1347	log plain
-rw-r--r--	quantifiers_rewriter.cpp	44985	log plain
-rw-r--r--	quantifiers_rewriter.h	3412	log plain
-rw-r--r--	relevant_domain.cpp	8497	log plain
-rw-r--r--	relevant_domain.h	2059	log plain
-rw-r--r--	rewrite_engine.cpp	11966	log plain
-rw-r--r--	rewrite_engine.h	2052	log plain
-rw-r--r--	symmetry_breaking.cpp	12270	log plain
-rw-r--r--	symmetry_breaking.h	3698	log plain
-rw-r--r--	term_database.cpp	66945	log plain
-rw-r--r--	term_database.h	17770	log plain
-rw-r--r--	theory_quantifiers.cpp	5795	log plain
-rw-r--r--	theory_quantifiers.h	2493	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9258	log plain
-rw-r--r--	trigger.cpp	20125	log plain
-rw-r--r--	trigger.h	6224	log plain