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

drwxr-xr-x		..
-rw-r--r--	3366	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	3140	alpha_equivalence.h	blob \| history \| raw
-rw-r--r--	13178	bv_inverter.cpp	blob \| history \| raw
-rw-r--r--	4055	bv_inverter.h	blob \| history \| raw
-rw-r--r--	75816	bv_inverter_utils.cpp	blob \| history \| raw
-rw-r--r--	2437	bv_inverter_utils.h	blob \| history \| raw
-rw-r--r--	10005	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	5335	candidate_rewrite_database.h	blob \| history \| raw
-rw-r--r--	8748	candidate_rewrite_filter.cpp	blob \| history \| raw
-rw-r--r--	6884	candidate_rewrite_filter.h	blob \| history \| raw
drwxr-xr-x	-	cegqi	tree \| history
-rw-r--r--	87092	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16408	conjecture_generator.h	blob \| history \| raw
-rw-r--r--	4683	dynamic_rewrite.cpp	blob \| history \| raw
-rw-r--r--	4301	dynamic_rewrite.h	blob \| history \| raw
drwxr-xr-x	-	ematching	tree \| history
-rw-r--r--	5818	equality_query.cpp	blob \| history \| raw
-rw-r--r--	3545	equality_query.h	blob \| history \| raw
-rw-r--r--	2884	expr_miner.cpp	blob \| history \| raw
-rw-r--r--	3190	expr_miner.h	blob \| history \| raw
-rw-r--r--	4435	expr_miner_manager.cpp	blob \| history \| raw
-rw-r--r--	4694	expr_miner_manager.h	blob \| history \| raw
-rw-r--r--	49985	extended_rewrite.cpp	blob \| history \| raw
-rw-r--r--	9557	extended_rewrite.h	blob \| history \| raw
-rw-r--r--	11282	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	7436	first_order_model.h	blob \| history \| raw
drwxr-xr-x	-	fmf	tree \| history
-rw-r--r--	9175	fun_def_evaluator.cpp	blob \| history \| raw
-rw-r--r--	2021	fun_def_evaluator.h	blob \| history \| raw
-rw-r--r--	3274	index_trie.cpp	blob \| history \| raw
-rw-r--r--	4162	index_trie.h	blob \| history \| raw
-rw-r--r--	2249	inst_match.cpp	blob \| history \| raw
-rw-r--r--	2798	inst_match.h	blob \| history \| raw
-rw-r--r--	9903	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	8002	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	6978	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	4199	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	23636	instantiate.cpp	blob \| history \| raw
-rw-r--r--	13961	instantiate.h	blob \| history \| raw
-rw-r--r--	1028	instantiation_list.cpp	blob \| history \| raw
-rw-r--r--	1706	instantiation_list.h	blob \| history \| raw
-rw-r--r--	2778	kinds	blob \| history \| raw
-rw-r--r--	4926	lazy_trie.cpp	blob \| history \| raw
-rw-r--r--	5625	lazy_trie.h	blob \| history \| raw
-rw-r--r--	3569	proof_checker.cpp	blob \| history \| raw
-rw-r--r--	1500	proof_checker.h	blob \| history \| raw
-rw-r--r--	3317	quant_bound_inference.cpp	blob \| history \| raw
-rw-r--r--	4225	quant_bound_inference.h	blob \| history \| raw
-rw-r--r--	84467	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	11062	quant_conflict_find.h	blob \| history \| raw
-rw-r--r--	1892	quant_module.cpp	blob \| history \| raw
-rw-r--r--	6196	quant_module.h	blob \| history \| raw
-rw-r--r--	1679	quant_relevance.cpp	blob \| history \| raw
-rw-r--r--	2049	quant_relevance.h	blob \| history \| raw
-rw-r--r--	2571	quant_rep_bound_ext.cpp	blob \| history \| raw
-rw-r--r--	2287	quant_rep_bound_ext.h	blob \| history \| raw
-rw-r--r--	7140	quant_split.cpp	blob \| history \| raw
-rw-r--r--	2655	quant_split.h	blob \| history \| raw
-rw-r--r--	4473	quant_util.cpp	blob \| history \| raw
-rw-r--r--	2768	quant_util.h	blob \| history \| raw
-rw-r--r--	11774	quantifiers_attributes.cpp	blob \| history \| raw
-rw-r--r--	8148	quantifiers_attributes.h	blob \| history \| raw
-rw-r--r--	1593	quantifiers_inference_manager.cpp	blob \| history \| raw
-rw-r--r--	1947	quantifiers_inference_manager.h	blob \| history \| raw
-rw-r--r--	4046	quantifiers_modules.cpp	blob \| history \| raw
-rw-r--r--	3471	quantifiers_modules.h	blob \| history \| raw
-rw-r--r--	5968	quantifiers_registry.cpp	blob \| history \| raw
-rw-r--r--	5194	quantifiers_registry.h	blob \| history \| raw
-rw-r--r--	67574	quantifiers_rewriter.cpp	blob \| history \| raw
-rw-r--r--	12702	quantifiers_rewriter.h	blob \| history \| raw
-rw-r--r--	4902	quantifiers_state.cpp	blob \| history \| raw
-rw-r--r--	3147	quantifiers_state.h	blob \| history \| raw
-rw-r--r--	2790	quantifiers_statistics.cpp	blob \| history \| raw
-rw-r--r--	1490	quantifiers_statistics.h	blob \| history \| raw
-rw-r--r--	12990	query_generator.cpp	blob \| history \| raw
-rw-r--r--	4584	query_generator.h	blob \| history \| raw
-rw-r--r--	12365	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5823	relevant_domain.h	blob \| history \| raw
-rw-r--r--	18645	single_inv_partition.cpp	blob \| history \| raw
-rw-r--r--	10809	single_inv_partition.h	blob \| history \| raw
-rw-r--r--	12837	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5804	skolemize.h	blob \| history \| raw
-rw-r--r--	3342	solution_filter.cpp	blob \| history \| raw
-rw-r--r--	2540	solution_filter.h	blob \| history \| raw
drwxr-xr-x	-	sygus	tree \| history
-rw-r--r--	17083	sygus_inst.cpp	blob \| history \| raw
-rw-r--r--	4949	sygus_inst.h	blob \| history \| raw
-rw-r--r--	23436	sygus_sampler.cpp	blob \| history \| raw
-rw-r--r--	13253	sygus_sampler.h	blob \| history \| raw
-rw-r--r--	36570	term_database.cpp	blob \| history \| raw
-rw-r--r--	17241	term_database.h	blob \| history \| raw
-rw-r--r--	2022	term_enumeration.cpp	blob \| history \| raw
-rw-r--r--	2359	term_enumeration.h	blob \| history \| raw
-rw-r--r--	4057	term_registry.cpp	blob \| history \| raw
-rw-r--r--	3211	term_registry.h	blob \| history \| raw
-rw-r--r--	16871	term_tuple_enumerator.cpp	blob \| history \| raw
-rw-r--r--	3770	term_tuple_enumerator.h	blob \| history \| raw
-rw-r--r--	14561	term_util.cpp	blob \| history \| raw
-rw-r--r--	7133	term_util.h	blob \| history \| raw
-rw-r--r--	5996	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	3736	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	4665	theory_quantifiers_type_rules.h	blob \| history \| raw