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	88765	log plain
-rw-r--r--	bv_inverter.h	3824	log plain
-rw-r--r--	candidate_rewrite_database.cpp	8235	log plain
-rw-r--r--	candidate_rewrite_database.h	3344	log plain
d---------	cegqi	290	log plain
-rw-r--r--	conjecture_generator.cpp	85762	log plain
-rw-r--r--	conjecture_generator.h	15883	log plain
-rw-r--r--	dynamic_rewrite.cpp	3581	log plain
-rw-r--r--	dynamic_rewrite.h	4117	log plain
d---------	ematching	572	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	32542	log plain
-rw-r--r--	extended_rewrite.h	8330	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_process.cpp	13284	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	23635	log plain
-rw-r--r--	instantiate.h	14671	log plain
-rw-r--r--	kinds	3426	log plain
-rw-r--r--	lazy_trie.cpp	1778	log plain
-rw-r--r--	lazy_trie.h	3171	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	20381	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_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	15243	log plain
-rw-r--r--	quantifiers_attributes.h	7861	log plain
-rw-r--r--	quantifiers_rewriter.cpp	76982	log plain
-rw-r--r--	quantifiers_rewriter.h	6084	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	17112	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	1766	log plain
-rw-r--r--	sygus_inference.cpp	6352	log plain
-rw-r--r--	sygus_inference.h	1367	log plain
-rw-r--r--	sygus_sampler.cpp	30666	log plain
-rw-r--r--	sygus_sampler.h	16896	log plain
-rw-r--r--	term_database.cpp	35334	log plain
-rw-r--r--	term_database.h	17325	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	33904	log plain
-rw-r--r--	term_util.h	15207	log plain
-rw-r--r--	theory_quantifiers.cpp	6725	log plain
-rw-r--r--	theory_quantifiers.h	2545	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9053	log plain