git.libre-soc.org Git - cvc5.git/tree - src/theory/quantifiers/

drwxr-xr-x		..
-rw-r--r--	4107	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	1777	alpha_equivalence.h	blob \| history \| raw
-rw-r--r--	11323	anti_skolem.cpp	blob \| history \| raw
-rw-r--r--	2714	anti_skolem.h	blob \| history \| raw
-rw-r--r--	89158	bv_inverter.cpp	blob \| history \| raw
-rw-r--r--	4059	bv_inverter.h	blob \| history \| raw
-rw-r--r--	12713	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	6590	candidate_rewrite_database.h	blob \| history \| raw
-rw-r--r--	12578	candidate_rewrite_filter.cpp	blob \| history \| raw
-rw-r--r--	8393	candidate_rewrite_filter.h	blob \| history \| raw
drwxr-xr-x	-	cegqi	tree \| history
-rw-r--r--	86820	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16421	conjecture_generator.h	blob \| history \| raw
-rw-r--r--	4657	dynamic_rewrite.cpp	blob \| history \| raw
-rw-r--r--	4317	dynamic_rewrite.h	blob \| history \| raw
drwxr-xr-x	-	ematching	tree \| history
-rw-r--r--	16865	equality_infer.cpp	blob \| history \| raw
-rw-r--r--	3525	equality_infer.h	blob \| history \| raw
-rw-r--r--	13510	equality_query.cpp	blob \| history \| raw
-rw-r--r--	4956	equality_query.h	blob \| history \| raw
-rw-r--r--	45441	extended_rewrite.cpp	blob \| history \| raw
-rw-r--r--	8883	extended_rewrite.h	blob \| history \| raw
-rw-r--r--	34684	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	10206	first_order_model.h	blob \| history \| raw
drwxr-xr-x	-	fmf	tree \| history
-rw-r--r--	13401	fun_def_process.cpp	blob \| history \| raw
-rw-r--r--	2957	fun_def_process.h	blob \| history \| raw
-rw-r--r--	2698	global_negate.cpp	blob \| history \| raw
-rw-r--r--	1494	global_negate.h	blob \| history \| raw
-rw-r--r--	2904	inst_match.cpp	blob \| history \| raw
-rw-r--r--	3216	inst_match.h	blob \| history \| raw
-rw-r--r--	13492	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	15254	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	31111	inst_propagator.cpp	blob \| history \| raw
-rw-r--r--	7144	inst_propagator.h	blob \| history \| raw
-rw-r--r--	9291	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	3530	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	23635	instantiate.cpp	blob \| history \| raw
-rw-r--r--	14688	instantiate.h	blob \| history \| raw
-rw-r--r--	3426	kinds	blob \| history \| raw
-rw-r--r--	4936	lazy_trie.cpp	blob \| history \| raw
-rw-r--r--	5624	lazy_trie.h	blob \| history \| raw
-rw-r--r--	9392	local_theory_ext.cpp	blob \| history \| raw
-rw-r--r--	2752	local_theory_ext.h	blob \| history \| raw
-rw-r--r--	19242	macros.cpp	blob \| history \| raw
-rw-r--r--	2573	macros.h	blob \| history \| raw
-rw-r--r--	82438	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	9587	quant_conflict_find.h	blob \| history \| raw
-rw-r--r--	5434	quant_epr.cpp	blob \| history \| raw
-rw-r--r--	3185	quant_epr.h	blob \| history \| raw
-rw-r--r--	2342	quant_relevance.cpp	blob \| history \| raw
-rw-r--r--	2407	quant_relevance.h	blob \| history \| raw
-rw-r--r--	5862	quant_split.cpp	blob \| history \| raw
-rw-r--r--	1813	quant_split.h	blob \| history \| raw
-rw-r--r--	5452	quant_util.cpp	blob \| history \| raw
-rw-r--r--	8605	quant_util.h	blob \| history \| raw
-rw-r--r--	15238	quantifiers_attributes.cpp	blob \| history \| raw
-rw-r--r--	7835	quantifiers_attributes.h	blob \| history \| raw
-rw-r--r--	76649	quantifiers_rewriter.cpp	blob \| history \| raw
-rw-r--r--	6084	quantifiers_rewriter.h	blob \| history \| raw
-rw-r--r--	11816	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5576	relevant_domain.h	blob \| history \| raw
-rw-r--r--	12064	rewrite_engine.cpp	blob \| history \| raw
-rw-r--r--	2182	rewrite_engine.h	blob \| history \| raw
-rw-r--r--	17102	single_inv_partition.cpp	blob \| history \| raw
-rw-r--r--	10710	single_inv_partition.h	blob \| history \| raw
-rw-r--r--	11869	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5296	skolemize.h	blob \| history \| raw
drwxr-xr-x	-	sygus	tree \| history
-rw-r--r--	8867	sygus_inference.cpp	blob \| history \| raw
-rw-r--r--	1935	sygus_inference.h	blob \| history \| raw
-rw-r--r--	21206	sygus_sampler.cpp	blob \| history \| raw
-rw-r--r--	11930	sygus_sampler.h	blob \| history \| raw
-rw-r--r--	35334	term_database.cpp	blob \| history \| raw
-rw-r--r--	17383	term_database.h	blob \| history \| raw
-rw-r--r--	3803	term_enumeration.cpp	blob \| history \| raw
-rw-r--r--	2646	term_enumeration.h	blob \| history \| raw
-rw-r--r--	33985	term_util.cpp	blob \| history \| raw
-rw-r--r--	15088	term_util.h	blob \| history \| raw
-rw-r--r--	6318	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	2330	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	9052	theory_quantifiers_type_rules.h	blob \| history \| raw