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	4117	log plain
-rw-r--r--	alpha_equivalence.h	1777	log plain
-rw-r--r--	ambqi_builder.cpp	37291	log plain
-rw-r--r--	ambqi_builder.h	4417	log plain
-rw-r--r--	anti_skolem.cpp	11323	log plain
-rw-r--r--	anti_skolem.h	2665	log plain
-rw-r--r--	bounded_integers.cpp	35683	log plain
-rw-r--r--	bounded_integers.h	6464	log plain
-rw-r--r--	bv_inverter.cpp	23852	log plain
-rw-r--r--	bv_inverter.h	3456	log plain
-rw-r--r--	candidate_generator.cpp	10026	log plain
-rw-r--r--	candidate_generator.h	5075	log plain
-rw-r--r--	ce_guided_conjecture.cpp	25171	log plain
-rw-r--r--	ce_guided_conjecture.h	8552	log plain
-rw-r--r--	ce_guided_instantiation.cpp	13741	log plain
-rw-r--r--	ce_guided_instantiation.h	2664	log plain
-rw-r--r--	ce_guided_pbe.cpp	82262	log plain
-rw-r--r--	ce_guided_pbe.h	22411	log plain
-rw-r--r--	ce_guided_single_inv.cpp	38659	log plain
-rw-r--r--	ce_guided_single_inv.h	9235	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	48025	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3692	log plain
-rw-r--r--	ceg_instantiator.cpp	49836	log plain
-rw-r--r--	ceg_instantiator.h	28855	log plain
-rw-r--r--	ceg_t_instantiator.cpp	60176	log plain
-rw-r--r--	ceg_t_instantiator.h	12841	log plain
-rw-r--r--	conjecture_generator.cpp	85385	log plain
-rw-r--r--	conjecture_generator.h	15656	log plain
-rw-r--r--	equality_infer.cpp	16875	log plain
-rw-r--r--	equality_infer.h	3558	log plain
-rw-r--r--	equality_query.cpp	13342	log plain
-rw-r--r--	equality_query.h	4873	log plain
-rw-r--r--	extended_rewrite.cpp	10502	log plain
-rw-r--r--	extended_rewrite.h	2097	log plain
-rw-r--r--	first_order_model.cpp	37351	log plain
-rw-r--r--	first_order_model.h	10634	log plain
-rw-r--r--	full_model_check.cpp	55498	log plain
-rw-r--r--	full_model_check.h	6339	log plain
-rw-r--r--	fun_def_engine.cpp	1552	log plain
-rw-r--r--	fun_def_engine.h	1694	log plain
-rw-r--r--	fun_def_process.cpp	13274	log plain
-rw-r--r--	fun_def_process.h	2968	log plain
-rw-r--r--	ho_trigger.cpp	15109	log plain
-rw-r--r--	ho_trigger.h	10055	log plain
-rw-r--r--	inst_match.cpp	14685	log plain
-rw-r--r--	inst_match.h	9678	log plain
-rw-r--r--	inst_match_generator.cpp	42116	log plain
-rw-r--r--	inst_match_generator.h	27409	log plain
-rw-r--r--	inst_propagator.cpp	31012	log plain
-rw-r--r--	inst_propagator.h	7076	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	31947	log plain
-rw-r--r--	inst_strategy_cbqi.h	5591	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	25125	log plain
-rw-r--r--	inst_strategy_e_matching.h	4165	log plain
-rw-r--r--	inst_strategy_enumerative.cpp	9282	log plain
-rw-r--r--	inst_strategy_enumerative.h	3604	log plain
-rw-r--r--	instantiation_engine.cpp	7561	log plain
-rw-r--r--	instantiation_engine.h	3247	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9401	log plain
-rw-r--r--	local_theory_ext.h	2819	log plain
-rw-r--r--	macros.cpp	20357	log plain
-rw-r--r--	macros.h	2598	log plain
-rw-r--r--	model_builder.cpp	34189	log plain
-rw-r--r--	model_builder.h	6737	log plain
-rw-r--r--	model_engine.cpp	12033	log plain
-rw-r--r--	model_engine.h	2193	log plain
-rw-r--r--	quant_conflict_find.cpp	86838	log plain
-rw-r--r--	quant_conflict_find.h	9927	log plain
-rw-r--r--	quant_epr.cpp	5459	log plain
-rw-r--r--	quant_epr.h	3185	log plain
-rw-r--r--	quant_equality_engine.cpp	7111	log plain
-rw-r--r--	quant_equality_engine.h	3786	log plain
-rw-r--r--	quant_relevance.cpp	2342	log plain
-rw-r--r--	quant_relevance.h	2414	log plain
-rw-r--r--	quant_split.cpp	5912	log plain
-rw-r--r--	quant_split.h	1762	log plain
-rw-r--r--	quant_util.cpp	12576	log plain
-rw-r--r--	quant_util.h	13656	log plain
-rw-r--r--	quantifiers_attributes.cpp	13133	log plain
-rw-r--r--	quantifiers_attributes.h	6942	log plain
-rw-r--r--	quantifiers_rewriter.cpp	72715	log plain
-rw-r--r--	quantifiers_rewriter.h	5252	log plain
-rw-r--r--	relevant_domain.cpp	11841	log plain
-rw-r--r--	relevant_domain.h	5608	log plain
-rw-r--r--	rewrite_engine.cpp	11989	log plain
-rw-r--r--	rewrite_engine.h	2188	log plain
-rw-r--r--	single_inv_partition.cpp	17380	log plain
-rw-r--r--	single_inv_partition.h	10720	log plain
-rw-r--r--	skolemize.cpp	11824	log plain
-rw-r--r--	skolemize.h	5296	log plain
-rw-r--r--	sygus_explain.cpp	8712	log plain
-rw-r--r--	sygus_explain.h	7880	log plain
-rw-r--r--	sygus_grammar_cons.cpp	26431	log plain
-rw-r--r--	sygus_grammar_cons.h	5646	log plain
-rw-r--r--	sygus_grammar_norm.cpp	6639	log plain
-rw-r--r--	sygus_grammar_norm.h	5038	log plain
-rw-r--r--	sygus_invariance.cpp	7408	log plain
-rw-r--r--	sygus_invariance.h	8520	log plain
-rw-r--r--	sygus_process_conj.cpp	24576	log plain
-rw-r--r--	sygus_process_conj.h	12715	log plain
-rw-r--r--	symmetry_breaking.cpp	12327	log plain
-rw-r--r--	symmetry_breaking.h	3618	log plain
-rw-r--r--	term_database.cpp	32325	log plain
-rw-r--r--	term_database.h	15461	log plain
-rw-r--r--	term_database_sygus.cpp	72317	log plain
-rw-r--r--	term_database_sygus.h	11029	log plain
-rw-r--r--	term_enumeration.cpp	3668	log plain
-rw-r--r--	term_enumeration.h	2646	log plain
-rw-r--r--	term_util.cpp	37323	log plain
-rw-r--r--	term_util.h	15228	log plain
-rw-r--r--	theory_quantifiers.cpp	6563	log plain
-rw-r--r--	theory_quantifiers.h	2494	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9471	log plain
-rw-r--r--	trigger.cpp	26906	log plain
-rw-r--r--	trigger.h	18873	log plain