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	37208	log plain
-rw-r--r--	ambqi_builder.h	4417	log plain
-rw-r--r--	anti_skolem.cpp	11168	log plain
-rw-r--r--	anti_skolem.h	2668	log plain
-rw-r--r--	bounded_integers.cpp	35782	log plain
-rw-r--r--	bounded_integers.h	6467	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	10050	log plain
-rw-r--r--	candidate_generator.h	5075	log plain
-rw-r--r--	ce_guided_conjecture.cpp	24857	log plain
-rw-r--r--	ce_guided_conjecture.h	8326	log plain
-rw-r--r--	ce_guided_instantiation.cpp	13670	log plain
-rw-r--r--	ce_guided_instantiation.h	2670	log plain
-rw-r--r--	ce_guided_pbe.cpp	86609	log plain
-rw-r--r--	ce_guided_pbe.h	22514	log plain
-rw-r--r--	ce_guided_single_inv.cpp	54797	log plain
-rw-r--r--	ce_guided_single_inv.h	11450	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	48184	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3692	log plain
-rw-r--r--	ceg_instantiator.cpp	45768	log plain
-rw-r--r--	ceg_instantiator.h	18503	log plain
-rw-r--r--	ceg_t_instantiator.cpp	52681	log plain
-rw-r--r--	ceg_t_instantiator.h	7104	log plain
-rw-r--r--	conjecture_generator.cpp	85243	log plain
-rw-r--r--	conjecture_generator.h	15659	log plain
-rw-r--r--	equality_infer.cpp	16757	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--	first_order_model.cpp	31125	log plain
-rw-r--r--	first_order_model.h	7679	log plain
-rw-r--r--	full_model_check.cpp	54388	log plain
-rw-r--r--	full_model_check.h	6339	log plain
-rw-r--r--	fun_def_engine.cpp	1555	log plain
-rw-r--r--	fun_def_engine.h	1697	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--	inst_match.cpp	14685	log plain
-rw-r--r--	inst_match.h	9678	log plain
-rw-r--r--	inst_match_generator.cpp	39473	log plain
-rw-r--r--	inst_match_generator.h	11193	log plain
-rw-r--r--	inst_propagator.cpp	30784	log plain
-rw-r--r--	inst_propagator.h	6788	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	31945	log plain
-rw-r--r--	inst_strategy_cbqi.h	5597	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	24969	log plain
-rw-r--r--	inst_strategy_e_matching.h	4165	log plain
-rw-r--r--	inst_strategy_enumerative.cpp	9347	log plain
-rw-r--r--	inst_strategy_enumerative.h	3605	log plain
-rw-r--r--	instantiation_engine.cpp	7535	log plain
-rw-r--r--	instantiation_engine.h	3248	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9419	log plain
-rw-r--r--	local_theory_ext.h	2822	log plain
-rw-r--r--	macros.cpp	20339	log plain
-rw-r--r--	macros.h	2598	log plain
-rw-r--r--	model_builder.cpp	33913	log plain
-rw-r--r--	model_builder.h	6778	log plain
-rw-r--r--	model_engine.cpp	12101	log plain
-rw-r--r--	model_engine.h	2199	log plain
-rw-r--r--	quant_conflict_find.cpp	86096	log plain
-rw-r--r--	quant_conflict_find.h	9694	log plain
-rw-r--r--	quant_equality_engine.cpp	7114	log plain
-rw-r--r--	quant_equality_engine.h	3789	log plain
-rw-r--r--	quant_split.cpp	5930	log plain
-rw-r--r--	quant_split.h	1765	log plain
-rw-r--r--	quant_util.cpp	19808	log plain
-rw-r--r--	quant_util.h	16120	log plain
-rw-r--r--	quantifiers_attributes.cpp	13133	log plain
-rw-r--r--	quantifiers_attributes.h	6616	log plain
-rw-r--r--	quantifiers_rewriter.cpp	72487	log plain
-rw-r--r--	quantifiers_rewriter.h	5251	log plain
-rw-r--r--	relevant_domain.cpp	11757	log plain
-rw-r--r--	relevant_domain.h	5565	log plain
-rw-r--r--	rewrite_engine.cpp	11970	log plain
-rw-r--r--	rewrite_engine.h	2191	log plain
-rw-r--r--	sygus_grammar_cons.cpp	25074	log plain
-rw-r--r--	sygus_grammar_cons.h	4641	log plain
-rw-r--r--	sygus_process_conj.cpp	2544	log plain
-rw-r--r--	sygus_process_conj.h	3306	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	34763	log plain
-rw-r--r--	term_database.h	15316	log plain
-rw-r--r--	term_database_sygus.cpp	96668	log plain
-rw-r--r--	term_database_sygus.h	12979	log plain
-rw-r--r--	term_util.cpp	40824	log plain
-rw-r--r--	term_util.h	13999	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	27032	log plain
-rw-r--r--	trigger.h	6750	log plain