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	3836	log plain
-rw-r--r--	alpha_equivalence.h	1776	log plain
-rw-r--r--	ambqi_builder.cpp	36822	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	17581	log plain
-rw-r--r--	bounded_integers.h	4753	log plain
-rw-r--r--	candidate_generator.cpp	9978	log plain
-rw-r--r--	candidate_generator.h	5170	log plain
-rw-r--r--	ce_guided_instantiation.cpp	29921	log plain
-rw-r--r--	ce_guided_instantiation.h	6150	log plain
-rw-r--r--	ce_guided_single_inv.cpp	49919	log plain
-rw-r--r--	ce_guided_single_inv.h	8404	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	73359	log plain
-rw-r--r--	ceg_instantiator.h	5676	log plain
-rw-r--r--	conjecture_generator.cpp	85190	log plain
-rw-r--r--	conjecture_generator.h	15658	log plain
-rw-r--r--	equality_infer.cpp	16788	log plain
-rw-r--r--	equality_infer.h	3480	log plain
-rw-r--r--	first_order_model.cpp	32083	log plain
-rw-r--r--	first_order_model.h	8217	log plain
-rw-r--r--	full_model_check.cpp	55169	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	10444	log plain
-rw-r--r--	inst_match.h	7760	log plain
-rw-r--r--	inst_match_generator.cpp	32441	log plain
-rw-r--r--	inst_match_generator.h	9953	log plain
-rw-r--r--	inst_propagator.cpp	29247	log plain
-rw-r--r--	inst_propagator.h	6229	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	27965	log plain
-rw-r--r--	inst_strategy_cbqi.h	5538	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	28114	log plain
-rw-r--r--	inst_strategy_e_matching.h	4546	log plain
-rw-r--r--	instantiation_engine.cpp	7799	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	32757	log plain
-rw-r--r--	model_builder.h	7132	log plain
-rw-r--r--	model_engine.cpp	13097	log plain
-rw-r--r--	model_engine.h	2358	log plain
-rw-r--r--	quant_conflict_find.cpp	84724	log plain
-rw-r--r--	quant_conflict_find.h	9408	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	5215	log plain
-rw-r--r--	quant_split.h	1730	log plain
-rw-r--r--	quant_util.cpp	13221	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	73568	log plain
-rw-r--r--	quantifiers_rewriter.h	5324	log plain
-rw-r--r--	relevant_domain.cpp	11005	log plain
-rw-r--r--	relevant_domain.h	2526	log plain
-rw-r--r--	rewrite_engine.cpp	12034	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	3742	log plain
-rw-r--r--	term_database.cpp	107619	log plain
-rw-r--r--	term_database.h	25937	log plain
-rw-r--r--	theory_quantifiers.cpp	6048	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	26349	log plain
-rw-r--r--	trigger.h	6926	log plain