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	4132	log plain
-rw-r--r--	alpha_equivalence.h	1776	log plain
-rw-r--r--	ambqi_builder.cpp	36829	log plain
-rw-r--r--	ambqi_builder.h	4432	log plain
-rw-r--r--	anti_skolem.cpp	10791	log plain
-rw-r--r--	anti_skolem.h	2366	log plain
-rw-r--r--	bounded_integers.cpp	25047	log plain
-rw-r--r--	bounded_integers.h	6066	log plain
-rw-r--r--	candidate_generator.cpp	10033	log plain
-rw-r--r--	candidate_generator.h	5075	log plain
-rw-r--r--	ce_guided_instantiation.cpp	37012	log plain
-rw-r--r--	ce_guided_instantiation.h	6352	log plain
-rw-r--r--	ce_guided_single_inv.cpp	52239	log plain
-rw-r--r--	ce_guided_single_inv.h	8438	log plain
-rw-r--r--	ce_guided_single_inv_ei.cpp	1527	log plain
-rw-r--r--	ce_guided_single_inv_ei.h	1172	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	47992	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3691	log plain
-rw-r--r--	ceg_instantiator.cpp	75743	log plain
-rw-r--r--	ceg_instantiator.h	5676	log plain
-rw-r--r--	conjecture_generator.cpp	85013	log plain
-rw-r--r--	conjecture_generator.h	15658	log plain
-rw-r--r--	equality_infer.cpp	16757	log plain
-rw-r--r--	equality_infer.h	3582	log plain
-rw-r--r--	first_order_model.cpp	32092	log plain
-rw-r--r--	first_order_model.h	8217	log plain
-rw-r--r--	full_model_check.cpp	55337	log plain
-rw-r--r--	full_model_check.h	6512	log plain
-rw-r--r--	fun_def_engine.cpp	1554	log plain
-rw-r--r--	fun_def_engine.h	1696	log plain
-rw-r--r--	fun_def_process.cpp	9450	log plain
-rw-r--r--	fun_def_process.h	1594	log plain
-rw-r--r--	inst_match.cpp	14454	log plain
-rw-r--r--	inst_match.h	9781	log plain
-rw-r--r--	inst_match_generator.cpp	34200	log plain
-rw-r--r--	inst_match_generator.h	10299	log plain
-rw-r--r--	inst_propagator.cpp	30587	log plain
-rw-r--r--	inst_propagator.h	6573	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	28016	log plain
-rw-r--r--	inst_strategy_cbqi.h	5538	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	31324	log plain
-rw-r--r--	inst_strategy_e_matching.h	4724	log plain
-rw-r--r--	instantiation_engine.cpp	7635	log plain
-rw-r--r--	instantiation_engine.h	3233	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9376	log plain
-rw-r--r--	local_theory_ext.h	2750	log plain
-rw-r--r--	macros.cpp	20155	log plain
-rw-r--r--	macros.h	2612	log plain
-rw-r--r--	model_builder.cpp	32948	log plain
-rw-r--r--	model_builder.h	6821	log plain
-rw-r--r--	model_engine.cpp	12777	log plain
-rw-r--r--	model_engine.h	2358	log plain
-rw-r--r--	quant_conflict_find.cpp	85560	log plain
-rw-r--r--	quant_conflict_find.h	9748	log plain
-rw-r--r--	quant_equality_engine.cpp	7078	log plain
-rw-r--r--	quant_equality_engine.h	3778	log plain
-rw-r--r--	quant_split.cpp	5245	log plain
-rw-r--r--	quant_split.h	1730	log plain
-rw-r--r--	quant_util.cpp	13246	log plain
-rw-r--r--	quant_util.h	6573	log plain
-rw-r--r--	quantifiers_attributes.cpp	2942	log plain
-rw-r--r--	quantifiers_attributes.h	1408	log plain
-rw-r--r--	quantifiers_rewriter.cpp	64992	log plain
-rw-r--r--	quantifiers_rewriter.h	4834	log plain
-rw-r--r--	relevant_domain.cpp	10991	log plain
-rw-r--r--	relevant_domain.h	2526	log plain
-rw-r--r--	rewrite_engine.cpp	12049	log plain
-rw-r--r--	rewrite_engine.h	2125	log plain
-rw-r--r--	symmetry_breaking.cpp	12331	log plain
-rw-r--r--	symmetry_breaking.h	3618	log plain
-rw-r--r--	term_database.cpp	113964	log plain
-rw-r--r--	term_database.h	26893	log plain
-rw-r--r--	theory_quantifiers.cpp	6206	log plain
-rw-r--r--	theory_quantifiers.h	2558	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9316	log plain
-rw-r--r--	trigger.cpp	26647	log plain
-rw-r--r--	trigger.h	7016	log plain