quantifiers « theory « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rwxr-xr-x	alpha_equivalence.cpp	3681	log plain
-rwxr-xr-x	alpha_equivalence.h	1632	log plain
-rw-r--r--	ambqi_builder.cpp	36736	log plain
-rw-r--r--	ambqi_builder.h	4376	log plain
-rw-r--r--	bounded_integers.cpp	17533	log plain
-rw-r--r--	bounded_integers.h	4695	log plain
-rw-r--r--	candidate_generator.cpp	7140	log plain
-rw-r--r--	candidate_generator.h	4573	log plain
-rw-r--r--	ce_guided_instantiation.cpp	25174	log plain
-rw-r--r--	ce_guided_instantiation.h	5247	log plain
-rw-r--r--	ce_guided_single_inv.cpp	37864	log plain
-rw-r--r--	ce_guided_single_inv.h	5269	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	47935	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	3639	log plain
-rw-r--r--	ceg_instantiator.cpp	63118	log plain
-rw-r--r--	ceg_instantiator.h	5227	log plain
-rw-r--r--	conjecture_generator.cpp	84865	log plain
-rw-r--r--	conjecture_generator.h	15587	log plain
-rw-r--r--	first_order_model.cpp	29517	log plain
-rw-r--r--	first_order_model.h	8160	log plain
-rw-r--r--	full_model_check.cpp	54805	log plain
-rw-r--r--	full_model_check.h	6333	log plain
-rw-r--r--	fun_def_engine.cpp	1503	log plain
-rw-r--r--	fun_def_engine.h	1644	log plain
-rw-r--r--	fun_def_process.cpp	9417	log plain
-rw-r--r--	fun_def_process.h	1551	log plain
-rw-r--r--	inst_match.cpp	8863	log plain
-rw-r--r--	inst_match.h	7165	log plain
-rw-r--r--	inst_match_generator.cpp	31808	log plain
-rw-r--r--	inst_match_generator.h	9812	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	24558	log plain
-rw-r--r--	inst_strategy_cbqi.h	5032	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	24314	log plain
-rw-r--r--	inst_strategy_e_matching.h	4362	log plain
-rw-r--r--	instantiation_engine.cpp	10782	log plain
-rw-r--r--	instantiation_engine.h	4151	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	local_theory_ext.cpp	9180	log plain
-rw-r--r--	local_theory_ext.h	2678	log plain
-rw-r--r--	macros.cpp	17975	log plain
-rw-r--r--	macros.h	2554	log plain
-rw-r--r--	model_builder.cpp	32330	log plain
-rw-r--r--	model_builder.h	7015	log plain
-rw-r--r--	model_engine.cpp	12057	log plain
-rw-r--r--	model_engine.h	2300	log plain
-rw-r--r--	modes.cpp	2254	log plain
-rw-r--r--	modes.h	4923	log plain
-rw-r--r--	options	18478	log plain
-rw-r--r--	options_handlers.h	15757	log plain
-rw-r--r--	quant_conflict_find.cpp	81445	log plain
-rw-r--r--	quant_conflict_find.h	8285	log plain
-rwxr-xr-x	quant_equality_engine.cpp	4543	log plain
-rwxr-xr-x	quant_equality_engine.h	3345	log plain
-rw-r--r--	quant_util.cpp	10689	log plain
-rw-r--r--	quant_util.h	4043	log plain
-rw-r--r--	quantifiers_attributes.cpp	2500	log plain
-rw-r--r--	quantifiers_attributes.h	1347	log plain
-rw-r--r--	quantifiers_rewriter.cpp	53578	log plain
-rw-r--r--	quantifiers_rewriter.h	3517	log plain
-rw-r--r--	relevant_domain.cpp	8497	log plain
-rw-r--r--	relevant_domain.h	2059	log plain
-rw-r--r--	rewrite_engine.cpp	11947	log plain
-rw-r--r--	rewrite_engine.h	2067	log plain
-rw-r--r--	symmetry_breaking.cpp	12270	log plain
-rw-r--r--	symmetry_breaking.h	3698	log plain
-rw-r--r--	term_database.cpp	92987	log plain
-rw-r--r--	term_database.h	21546	log plain
-rw-r--r--	theory_quantifiers.cpp	5891	log plain
-rw-r--r--	theory_quantifiers.h	2493	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9258	log plain
-rw-r--r--	trigger.cpp	21162	log plain
-rw-r--r--	trigger.h	6415	log plain