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

drwxr-xr-x		..
-rw-r--r--	3432	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	3142	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--	10177	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	5548	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--	87182	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16394	conjecture_generator.h	blob \| history \| raw
-rw-r--r--	4709	dynamic_rewrite.cpp	blob \| history \| raw
-rw-r--r--	4327	dynamic_rewrite.h	blob \| history \| raw
drwxr-xr-x	-	ematching	tree \| history
-rw-r--r--	6231	equality_query.cpp	blob \| history \| raw
-rw-r--r--	3700	equality_query.h	blob \| history \| raw
-rw-r--r--	2909	expr_miner.cpp	blob \| history \| raw
-rw-r--r--	3190	expr_miner.h	blob \| history \| raw
-rw-r--r--	4552	expr_miner_manager.cpp	blob \| history \| raw
-rw-r--r--	4780	expr_miner_manager.h	blob \| history \| raw
-rw-r--r--	49991	extended_rewrite.cpp	blob \| history \| raw
-rw-r--r--	9583	extended_rewrite.h	blob \| history \| raw
-rw-r--r--	10492	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	7050	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--	2400	inst_match.cpp	blob \| history \| raw
-rw-r--r--	2898	inst_match.h	blob \| history \| raw
-rw-r--r--	9954	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	8140	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	6909	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	4230	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	23508	instantiate.cpp	blob \| history \| raw
-rw-r--r--	14029	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--	2397	kinds	blob \| history \| raw
-rw-r--r--	4952	lazy_trie.cpp	blob \| history \| raw
-rw-r--r--	5651	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--	84371	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	10925	quant_conflict_find.h	blob \| history \| raw
-rw-r--r--	2167	quant_module.cpp	blob \| history \| raw
-rw-r--r--	6258	quant_module.h	blob \| history \| raw
-rw-r--r--	1705	quant_relevance.cpp	blob \| history \| raw
-rw-r--r--	2075	quant_relevance.h	blob \| history \| raw
-rw-r--r--	2517	quant_rep_bound_ext.cpp	blob \| history \| raw
-rw-r--r--	2203	quant_rep_bound_ext.h	blob \| history \| raw
-rw-r--r--	7132	quant_split.cpp	blob \| history \| raw
-rw-r--r--	2641	quant_split.h	blob \| history \| raw
-rw-r--r--	4483	quant_util.cpp	blob \| history \| raw
-rw-r--r--	3458	quant_util.h	blob \| history \| raw
-rw-r--r--	11800	quantifiers_attributes.cpp	blob \| history \| raw
-rw-r--r--	8129	quantifiers_attributes.h	blob \| history \| raw
-rw-r--r--	1154	quantifiers_inference_manager.cpp	blob \| history \| raw
-rw-r--r--	1457	quantifiers_inference_manager.h	blob \| history \| raw
-rw-r--r--	3564	quantifiers_modules.cpp	blob \| history \| raw
-rw-r--r--	3331	quantifiers_modules.h	blob \| history \| raw
-rw-r--r--	5702	quantifiers_registry.cpp	blob \| history \| raw
-rw-r--r--	4938	quantifiers_registry.h	blob \| history \| raw
-rw-r--r--	67597	quantifiers_rewriter.cpp	blob \| history \| raw
-rw-r--r--	12725	quantifiers_rewriter.h	blob \| history \| raw
-rw-r--r--	4824	quantifiers_state.cpp	blob \| history \| raw
-rw-r--r--	2970	quantifiers_state.h	blob \| history \| raw
-rw-r--r--	12996	query_generator.cpp	blob \| history \| raw
-rw-r--r--	4584	query_generator.h	blob \| history \| raw
-rw-r--r--	12225	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5683	relevant_domain.h	blob \| history \| raw
-rw-r--r--	18671	single_inv_partition.cpp	blob \| history \| raw
-rw-r--r--	10835	single_inv_partition.h	blob \| history \| raw
-rw-r--r--	12807	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5830	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--	17164	sygus_inst.cpp	blob \| history \| raw
-rw-r--r--	4954	sygus_inst.h	blob \| history \| raw
-rw-r--r--	23442	sygus_sampler.cpp	blob \| history \| raw
-rw-r--r--	13279	sygus_sampler.h	blob \| history \| raw
-rw-r--r--	36584	term_database.cpp	blob \| history \| raw
-rw-r--r--	17265	term_database.h	blob \| history \| raw
-rw-r--r--	2939	term_enumeration.cpp	blob \| history \| raw
-rw-r--r--	2744	term_enumeration.h	blob \| history \| raw
-rw-r--r--	2653	term_registry.cpp	blob \| history \| raw
-rw-r--r--	2362	term_registry.h	blob \| history \| raw
-rw-r--r--	16722	term_tuple_enumerator.cpp	blob \| history \| raw
-rw-r--r--	3221	term_tuple_enumerator.h	blob \| history \| raw
-rw-r--r--	14857	term_util.cpp	blob \| history \| raw
-rw-r--r--	7156	term_util.h	blob \| history \| raw
-rw-r--r--	5627	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	3529	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	5246	theory_quantifiers_type_rules.h	blob \| history \| raw