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	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	6430	log plain
-rw-r--r--	bv_inverter.cpp	68999	log plain
-rw-r--r--	bv_inverter.h	3065	log plain
-rw-r--r--	candidate_generator.cpp	10088	log plain
-rw-r--r--	candidate_generator.h	5075	log plain
-rw-r--r--	ce_guided_conjecture.cpp	25254	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	86507	log plain
-rw-r--r--	ce_guided_pbe.h	30756	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	48025	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3658	log plain
-rw-r--r--	ceg_instantiator.cpp	50716	log plain
-rw-r--r--	ceg_instantiator.h	29131	log plain
-rw-r--r--	ceg_t_instantiator.cpp	70869	log plain
-rw-r--r--	ceg_t_instantiator.h	13038	log plain
-rw-r--r--	conjecture_generator.cpp	85385	log plain
-rw-r--r--	conjecture_generator.h	15575	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	9026	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	55697	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--	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	10180	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	41865	log plain
-rw-r--r--	inst_match_generator.h	26824	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	31977	log plain
-rw-r--r--	inst_strategy_cbqi.h	5591	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	6737	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	87046	log plain
-rw-r--r--	quant_conflict_find.h	9874	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	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	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	12065	log plain
-rw-r--r--	rewrite_engine.h	2154	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	16992	log plain
-rw-r--r--	sygus_grammar_norm.h	15525	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	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	72723	log plain
-rw-r--r--	term_database_sygus.h	11285	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	2501	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9471	log plain
-rw-r--r--	trigger.cpp	31959	log plain
-rw-r--r--	trigger.h	19866	log plain