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	37359	log plain
-rw-r--r--	ambqi_builder.h	4466	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	6430	log plain
-rw-r--r--	bv_inverter.cpp	89653	log plain
-rw-r--r--	bv_inverter.h	3824	log plain
-rw-r--r--	candidate_generator.cpp	10088	log plain
-rw-r--r--	candidate_generator.h	5022	log plain
-rw-r--r--	ce_guided_conjecture.cpp	32576	log plain
-rw-r--r--	ce_guided_conjecture.h	11827	log plain
-rw-r--r--	ce_guided_instantiation.cpp	14320	log plain
-rw-r--r--	ce_guided_instantiation.h	3119	log plain
-rw-r--r--	ce_guided_pbe.cpp	87657	log plain
-rw-r--r--	ce_guided_pbe.h	33156	log plain
-rw-r--r--	ce_guided_single_inv.cpp	38659	log plain
-rw-r--r--	ce_guided_single_inv.h	9246	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	57874	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7497	log plain
-rw-r--r--	ceg_instantiator.cpp	50716	log plain
-rw-r--r--	ceg_instantiator.h	29163	log plain
-rw-r--r--	ceg_t_instantiator.cpp	70460	log plain
-rw-r--r--	ceg_t_instantiator.h	12810	log plain
-rw-r--r--	conjecture_generator.cpp	85385	log plain
-rw-r--r--	conjecture_generator.h	15540	log plain
-rw-r--r--	dynamic_rewrite.cpp	3336	log plain
-rw-r--r--	dynamic_rewrite.h	3988	log plain
-rw-r--r--	equality_infer.cpp	16875	log plain
-rw-r--r--	equality_infer.h	3519	log plain
-rw-r--r--	equality_query.cpp	13397	log plain
-rw-r--r--	equality_query.h	4873	log plain
-rw-r--r--	extended_rewrite.cpp	9167	log plain
-rw-r--r--	extended_rewrite.h	2097	log plain
-rw-r--r--	first_order_model.cpp	37335	log plain
-rw-r--r--	first_order_model.h	10620	log plain
-rw-r--r--	full_model_check.cpp	55697	log plain
-rw-r--r--	full_model_check.h	6306	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--	global_negate.cpp	2698	log plain
-rw-r--r--	global_negate.h	1494	log plain
-rw-r--r--	ho_trigger.cpp	16114	log plain
-rw-r--r--	ho_trigger.h	10181	log plain
-rw-r--r--	inst_match.cpp	2899	log plain
-rw-r--r--	inst_match.h	3216	log plain
-rw-r--r--	inst_match_generator.cpp	41771	log plain
-rw-r--r--	inst_match_generator.h	26807	log plain
-rw-r--r--	inst_match_trie.cpp	13512	log plain
-rw-r--r--	inst_match_trie.h	15280	log plain
-rw-r--r--	inst_propagator.cpp	31101	log plain
-rw-r--r--	inst_propagator.h	7120	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	31919	log plain
-rw-r--r--	inst_strategy_cbqi.h	5619	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	25027	log plain
-rw-r--r--	inst_strategy_e_matching.h	4165	log plain
-rw-r--r--	inst_strategy_enumerative.cpp	9344	log plain
-rw-r--r--	inst_strategy_enumerative.h	3604	log plain
-rw-r--r--	instantiate.cpp	23975	log plain
-rw-r--r--	instantiate.h	14703	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	34389	log plain
-rw-r--r--	model_builder.h	6687	log plain
-rw-r--r--	model_engine.cpp	12185	log plain
-rw-r--r--	model_engine.h	2193	log plain
-rw-r--r--	quant_conflict_find.cpp	87049	log plain
-rw-r--r--	quant_conflict_find.h	9841	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	3742	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	5477	log plain
-rw-r--r--	quant_util.h	8228	log plain
-rw-r--r--	quantifiers_attributes.cpp	14377	log plain
-rw-r--r--	quantifiers_attributes.h	7269	log plain
-rw-r--r--	quantifiers_rewriter.cpp	76076	log plain
-rw-r--r--	quantifiers_rewriter.h	5607	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	12065	log plain
-rw-r--r--	rewrite_engine.h	2124	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	11869	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	28574	log plain
-rw-r--r--	sygus_grammar_cons.h	5646	log plain
-rw-r--r--	sygus_grammar_norm.cpp	18464	log plain
-rw-r--r--	sygus_grammar_norm.h	16349	log plain
-rw-r--r--	sygus_grammar_red.cpp	4359	log plain
-rw-r--r--	sygus_grammar_red.h	4099	log plain
-rw-r--r--	sygus_invariance.cpp	7588	log plain
-rw-r--r--	sygus_invariance.h	8420	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--	sygus_sampler.cpp	19427	log plain
-rw-r--r--	sygus_sampler.h	13302	log plain
-rw-r--r--	symmetry_breaking.cpp	12327	log plain
-rw-r--r--	symmetry_breaking.h	3584	log plain
-rw-r--r--	term_database.cpp	32323	log plain
-rw-r--r--	term_database.h	15461	log plain
-rw-r--r--	term_database_sygus.cpp	52726	log plain
-rw-r--r--	term_database_sygus.h	12055	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	34170	log plain
-rw-r--r--	term_util.h	14738	log plain
-rw-r--r--	theory_quantifiers.cpp	6664	log plain
-rw-r--r--	theory_quantifiers.h	2679	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9053	log plain
-rw-r--r--	trigger.cpp	31959	log plain
-rw-r--r--	trigger.h	19866	log plain