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--	alpha_equivalence.cpp	3680	log plain
-rw-r--r--	alpha_equivalence.h	1630	log plain
-rw-r--r--	ambqi_builder.cpp	36737	log plain
-rw-r--r--	ambqi_builder.h	4376	log plain
-rw-r--r--	anti_skolem.cpp	10734	log plain
-rw-r--r--	anti_skolem.h	2314	log plain
-rw-r--r--	bounded_integers.cpp	17533	log plain
-rw-r--r--	bounded_integers.h	4695	log plain
-rw-r--r--	candidate_generator.cpp	7825	log plain
-rw-r--r--	candidate_generator.h	4669	log plain
-rw-r--r--	ce_guided_instantiation.cpp	29861	log plain
-rw-r--r--	ce_guided_instantiation.h	6098	log plain
-rw-r--r--	ce_guided_single_inv.cpp	49874	log plain
-rw-r--r--	ce_guided_single_inv.h	8333	log plain
-rw-r--r--	ce_guided_single_inv_ei.cpp	1475	log plain
-rw-r--r--	ce_guided_single_inv_ei.h	1120	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	47936	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3639	log plain
-rw-r--r--	ceg_instantiator.cpp	73254	log plain
-rw-r--r--	ceg_instantiator.h	5614	log plain
-rw-r--r--	conjecture_generator.cpp	84866	log plain
-rw-r--r--	conjecture_generator.h	15587	log plain
-rw-r--r--	first_order_model.cpp	29172	log plain
-rw-r--r--	first_order_model.h	7919	log plain
-rw-r--r--	full_model_check.cpp	55027	log plain
-rw-r--r--	full_model_check.h	6454	log plain
-rw-r--r--	fun_def_engine.cpp	1503	log plain
-rw-r--r--	fun_def_engine.h	1644	log plain
-rw-r--r--	fun_def_process.cpp	9417	log plain
-rw-r--r--	fun_def_process.h	1551	log plain
-rw-r--r--	inst_match.cpp	10170	log plain
-rw-r--r--	inst_match.h	7739	log plain
-rw-r--r--	inst_match_generator.cpp	31715	log plain
-rw-r--r--	inst_match_generator.h	9835	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	27672	log plain
-rw-r--r--	inst_strategy_cbqi.h	5480	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	25651	log plain
-rw-r--r--	inst_strategy_e_matching.h	4282	log plain
-rw-r--r--	instantiation_engine.cpp	6909	log plain
-rw-r--r--	instantiation_engine.h	3139	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9324	log plain
-rw-r--r--	local_theory_ext.h	2698	log plain
-rw-r--r--	macros.cpp	20113	log plain
-rw-r--r--	macros.h	2554	log plain
-rw-r--r--	model_builder.cpp	32532	log plain
-rw-r--r--	model_builder.h	7074	log plain
-rw-r--r--	model_engine.cpp	12658	log plain
-rw-r--r--	model_engine.h	2300	log plain
-rw-r--r--	quant_conflict_find.cpp	83591	log plain
-rw-r--r--	quant_conflict_find.h	8760	log plain
-rw-r--r--	quant_equality_engine.cpp	7026	log plain
-rw-r--r--	quant_equality_engine.h	3726	log plain
-rw-r--r--	quant_split.cpp	5163	log plain
-rw-r--r--	quant_split.h	1678	log plain
-rw-r--r--	quant_util.cpp	11267	log plain
-rw-r--r--	quant_util.h	4149	log plain
-rw-r--r--	quantifiers_attributes.cpp	2884	log plain
-rw-r--r--	quantifiers_attributes.h	1350	log plain
-rw-r--r--	quantifiers_rewriter.cpp	73152	log plain
-rw-r--r--	quantifiers_rewriter.h	5266	log plain
-rw-r--r--	relevant_domain.cpp	10908	log plain
-rw-r--r--	relevant_domain.h	2333	log plain
-rw-r--r--	rewrite_engine.cpp	11962	log plain
-rw-r--r--	rewrite_engine.h	2067	log plain
-rw-r--r--	symmetry_breaking.cpp	12273	log plain
-rw-r--r--	symmetry_breaking.h	3699	log plain
-rw-r--r--	term_database.cpp	99919	log plain
-rw-r--r--	term_database.h	23930	log plain
-rw-r--r--	theory_quantifiers.cpp	6001	log plain
-rw-r--r--	theory_quantifiers.h	2533	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9258	log plain
-rw-r--r--	trigger.cpp	22851	log plain
-rw-r--r--	trigger.h	6659	log plain