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--	anti_skolem.cpp	11323	log plain
-rw-r--r--	anti_skolem.h	2697	log plain
-rw-r--r--	bv_inverter.cpp	88725	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
d---------	cegqi	290	log plain
-rw-r--r--	conjecture_generator.cpp	85395	log plain
-rw-r--r--	conjecture_generator.h	15857	log plain
-rw-r--r--	dynamic_rewrite.cpp	3738	log plain
-rw-r--r--	dynamic_rewrite.h	4142	log plain
d---------	ematching	472	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	4939	log plain
-rw-r--r--	extended_rewrite.cpp	8550	log plain
-rw-r--r--	extended_rewrite.h	2626	log plain
-rw-r--r--	first_order_model.cpp	37351	log plain
-rw-r--r--	first_order_model.h	10617	log plain
d---------	fmf	450	log plain
-rw-r--r--	fun_def_engine.cpp	1552	log plain
-rw-r--r--	fun_def_engine.h	1740	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--	inst_match.cpp	2899	log plain
-rw-r--r--	inst_match.h	3216	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	7127	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	23981	log plain
-rw-r--r--	instantiate.h	14671	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	2871	log plain
-rw-r--r--	macros.cpp	20367	log plain
-rw-r--r--	macros.h	2598	log plain
-rw-r--r--	quant_conflict_find.cpp	87059	log plain
-rw-r--r--	quant_conflict_find.h	9889	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	4070	log plain
-rw-r--r--	quant_relevance.cpp	2342	log plain
-rw-r--r--	quant_relevance.h	2390	log plain
-rw-r--r--	quant_split.cpp	5912	log plain
-rw-r--r--	quant_split.h	1813	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	14844	log plain
-rw-r--r--	quantifiers_attributes.h	7269	log plain
-rw-r--r--	quantifiers_rewriter.cpp	77085	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	5584	log plain
-rw-r--r--	rewrite_engine.cpp	12079	log plain
-rw-r--r--	rewrite_engine.h	2180	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
d---------	sygus	1332	log plain
-rw-r--r--	sygus_sampler.cpp	20886	log plain
-rw-r--r--	sygus_sampler.h	14580	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	32333	log plain
-rw-r--r--	term_database.h	15437	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	14714	log plain
-rw-r--r--	theory_quantifiers.cpp	6678	log plain
-rw-r--r--	theory_quantifiers.h	2679	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9053	log plain