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	4315	log plain
-rw-r--r--	alpha_equivalence.h	3707	log plain
-rw-r--r--	anti_skolem.cpp	11350	log plain
-rw-r--r--	anti_skolem.h	2714	log plain
-rw-r--r--	bv_inverter.cpp	13195	log plain
-rw-r--r--	bv_inverter.h	4059	log plain
-rw-r--r--	bv_inverter_utils.cpp	75901	log plain
-rw-r--r--	bv_inverter_utils.h	2425	log plain
-rw-r--r--	candidate_rewrite_database.cpp	11293	log plain
-rw-r--r--	candidate_rewrite_database.h	5698	log plain
-rw-r--r--	candidate_rewrite_filter.cpp	13635	log plain
-rw-r--r--	candidate_rewrite_filter.h	8466	log plain
d---------	cegqi	714	log plain
-rw-r--r--	conjecture_generator.cpp	87020	log plain
-rw-r--r--	conjecture_generator.h	16662	log plain
-rw-r--r--	dynamic_rewrite.cpp	4710	log plain
-rw-r--r--	dynamic_rewrite.h	4317	log plain
d---------	ematching	572	log plain
-rw-r--r--	equality_infer.cpp	16894	log plain
-rw-r--r--	equality_infer.h	3540	log plain
-rw-r--r--	equality_query.cpp	10301	log plain
-rw-r--r--	equality_query.h	4851	log plain
-rw-r--r--	expr_miner.cpp	4270	log plain
-rw-r--r--	expr_miner.h	3885	log plain
-rw-r--r--	expr_miner_manager.cpp	4440	log plain
-rw-r--r--	expr_miner_manager.h	4782	log plain
-rw-r--r--	extended_rewrite.cpp	48826	log plain
-rw-r--r--	extended_rewrite.h	9354	log plain
-rw-r--r--	first_order_model.cpp	16814	log plain
-rw-r--r--	first_order_model.h	7338	log plain
d---------	fmf	362	log plain
-rw-r--r--	fun_def_process.cpp	14068	log plain
-rw-r--r--	fun_def_process.h	3088	log plain
-rw-r--r--	inst_match.cpp	2789	log plain
-rw-r--r--	inst_match.h	3113	log plain
-rw-r--r--	inst_match_trie.cpp	13517	log plain
-rw-r--r--	inst_match_trie.h	15279	log plain
-rw-r--r--	inst_propagator.cpp	31117	log plain
-rw-r--r--	inst_propagator.h	7160	log plain
-rw-r--r--	inst_strategy_enumerative.cpp	9306	log plain
-rw-r--r--	inst_strategy_enumerative.h	3530	log plain
-rw-r--r--	instantiate.cpp	23635	log plain
-rw-r--r--	instantiate.h	14703	log plain
-rw-r--r--	kinds	3403	log plain
-rw-r--r--	lazy_trie.cpp	4953	log plain
-rw-r--r--	lazy_trie.h	5651	log plain
-rw-r--r--	local_theory_ext.cpp	9989	log plain
-rw-r--r--	local_theory_ext.h	2967	log plain
-rw-r--r--	quant_conflict_find.cpp	82640	log plain
-rw-r--r--	quant_conflict_find.h	9580	log plain
-rw-r--r--	quant_epr.cpp	5434	log plain
-rw-r--r--	quant_epr.h	3185	log plain
-rw-r--r--	quant_relevance.cpp	1473	log plain
-rw-r--r--	quant_relevance.h	2121	log plain
-rw-r--r--	quant_split.cpp	5877	log plain
-rw-r--r--	quant_split.h	1813	log plain
-rw-r--r--	quant_util.cpp	5467	log plain
-rw-r--r--	quant_util.h	8433	log plain
-rw-r--r--	quantifiers_attributes.cpp	14746	log plain
-rw-r--r--	quantifiers_attributes.h	7971	log plain
-rw-r--r--	quantifiers_rewriter.cpp	77358	log plain
-rw-r--r--	quantifiers_rewriter.h	9038	log plain
-rw-r--r--	query_generator.cpp	12861	log plain
-rw-r--r--	query_generator.h	4369	log plain
-rw-r--r--	relevant_domain.cpp	11874	log plain
-rw-r--r--	relevant_domain.h	5576	log plain
-rw-r--r--	rewrite_engine.cpp	12079	log plain
-rw-r--r--	rewrite_engine.h	2172	log plain
-rw-r--r--	single_inv_partition.cpp	18495	log plain
-rw-r--r--	single_inv_partition.h	10800	log plain
-rw-r--r--	skolemize.cpp	11869	log plain
-rw-r--r--	skolemize.h	5296	log plain
-rw-r--r--	solution_filter.cpp	3303	log plain
-rw-r--r--	solution_filter.h	2530	log plain
d---------	sygus	2134	log plain
-rw-r--r--	sygus_sampler.cpp	23077	log plain
-rw-r--r--	sygus_sampler.h	13278	log plain
-rw-r--r--	term_canonize.cpp	5638	log plain
-rw-r--r--	term_canonize.h	3280	log plain
-rw-r--r--	term_database.cpp	33982	log plain
-rw-r--r--	term_database.h	15209	log plain
-rw-r--r--	term_enumeration.cpp	2602	log plain
-rw-r--r--	term_enumeration.h	2473	log plain
-rw-r--r--	term_util.cpp	28773	log plain
-rw-r--r--	term_util.h	14411	log plain
-rw-r--r--	theory_quantifiers.cpp	6128	log plain
-rw-r--r--	theory_quantifiers.h	2270	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	9052	log plain