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

drwxr-xr-x		..
-rw-r--r--	7264	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	4624	alpha_equivalence.h	blob \| history \| raw
-rw-r--r--	13343	bv_inverter.cpp	blob \| history \| raw
-rw-r--r--	4055	bv_inverter.h	blob \| history \| raw
-rw-r--r--	75836	bv_inverter_utils.cpp	blob \| history \| raw
-rw-r--r--	2450	bv_inverter_utils.h	blob \| history \| raw
-rw-r--r--	9929	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	5406	candidate_rewrite_database.h	blob \| history \| raw
-rw-r--r--	8751	candidate_rewrite_filter.cpp	blob \| history \| raw
-rw-r--r--	6912	candidate_rewrite_filter.h	blob \| history \| raw
drwxr-xr-x	-	cegqi	tree \| history
-rw-r--r--	87366	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16438	conjecture_generator.h	blob \| history \| raw
-rw-r--r--	4870	dynamic_rewrite.cpp	blob \| history \| raw
-rw-r--r--	4334	dynamic_rewrite.h	blob \| history \| raw
drwxr-xr-x	-	ematching	tree \| history
-rw-r--r--	12351	entailment_check.cpp	blob \| history \| raw
-rw-r--r--	5654	entailment_check.h	blob \| history \| raw
-rw-r--r--	5878	equality_query.cpp	blob \| history \| raw
-rw-r--r--	3586	equality_query.h	blob \| history \| raw
-rw-r--r--	2660	expr_miner.cpp	blob \| history \| raw
-rw-r--r--	3424	expr_miner.h	blob \| history \| raw
-rw-r--r--	4584	expr_miner_manager.cpp	blob \| history \| raw
-rw-r--r--	4617	expr_miner_manager.h	blob \| history \| raw
-rw-r--r--	50046	extended_rewrite.cpp	blob \| history \| raw
-rw-r--r--	10093	extended_rewrite.h	blob \| history \| raw
-rw-r--r--	11990	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	8365	first_order_model.h	blob \| history \| raw
drwxr-xr-x	-	fmf	tree \| history
-rw-r--r--	9505	fun_def_evaluator.cpp	blob \| history \| raw
-rw-r--r--	2329	fun_def_evaluator.h	blob \| history \| raw
-rw-r--r--	7438	ho_term_database.cpp	blob \| history \| raw
-rw-r--r--	4644	ho_term_database.h	blob \| history \| raw
-rw-r--r--	3288	index_trie.cpp	blob \| history \| raw
-rw-r--r--	4179	index_trie.h	blob \| history \| raw
-rw-r--r--	2267	inst_match.cpp	blob \| history \| raw
-rw-r--r--	2818	inst_match.h	blob \| history \| raw
-rw-r--r--	10110	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	8139	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	7044	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	4273	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	4725	inst_strategy_pool.cpp	blob \| history \| raw
-rw-r--r--	2490	inst_strategy_pool.h	blob \| history \| raw
-rw-r--r--	24204	instantiate.cpp	blob \| history \| raw
-rw-r--r--	13935	instantiate.h	blob \| history \| raw
-rw-r--r--	1317	instantiation_list.cpp	blob \| history \| raw
-rw-r--r--	2045	instantiation_list.h	blob \| history \| raw
-rw-r--r--	2779	kinds	blob \| history \| raw
-rw-r--r--	4945	lazy_trie.cpp	blob \| history \| raw
-rw-r--r--	5646	lazy_trie.h	blob \| history \| raw
-rw-r--r--	987	master_eq_notify.cpp	blob \| history \| raw
-rw-r--r--	1926	master_eq_notify.h	blob \| history \| raw
-rw-r--r--	4942	proof_checker.cpp	blob \| history \| raw
-rw-r--r--	1519	proof_checker.h	blob \| history \| raw
-rw-r--r--	3474	quant_bound_inference.cpp	blob \| history \| raw
-rw-r--r--	4212	quant_bound_inference.h	blob \| history \| raw
-rw-r--r--	84321	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	11068	quant_conflict_find.h	blob \| history \| raw
-rw-r--r--	2035	quant_module.cpp	blob \| history \| raw
-rw-r--r--	6502	quant_module.h	blob \| history \| raw
-rw-r--r--	1759	quant_relevance.cpp	blob \| history \| raw
-rw-r--r--	2069	quant_relevance.h	blob \| history \| raw
-rw-r--r--	2579	quant_rep_bound_ext.cpp	blob \| history \| raw
-rw-r--r--	2298	quant_rep_bound_ext.h	blob \| history \| raw
-rw-r--r--	7316	quant_split.cpp	blob \| history \| raw
-rw-r--r--	2704	quant_split.h	blob \| history \| raw
-rw-r--r--	4577	quant_util.cpp	blob \| history \| raw
-rw-r--r--	4116	quant_util.h	blob \| history \| raw
-rw-r--r--	13896	quantifiers_attributes.cpp	blob \| history \| raw
-rw-r--r--	7648	quantifiers_attributes.h	blob \| history \| raw
-rw-r--r--	1612	quantifiers_inference_manager.cpp	blob \| history \| raw
-rw-r--r--	1988	quantifiers_inference_manager.h	blob \| history \| raw
-rw-r--r--	8243	quantifiers_macros.cpp	blob \| history \| raw
-rw-r--r--	3387	quantifiers_macros.h	blob \| history \| raw
-rw-r--r--	4024	quantifiers_modules.cpp	blob \| history \| raw
-rw-r--r--	3614	quantifiers_modules.h	blob \| history \| raw
-rw-r--r--	8156	quantifiers_preprocess.cpp	blob \| history \| raw
-rw-r--r--	2624	quantifiers_preprocess.h	blob \| history \| raw
-rw-r--r--	6218	quantifiers_registry.cpp	blob \| history \| raw
-rw-r--r--	5426	quantifiers_registry.h	blob \| history \| raw
-rw-r--r--	65469	quantifiers_rewriter.cpp	blob \| history \| raw
-rw-r--r--	12690	quantifiers_rewriter.h	blob \| history \| raw
-rw-r--r--	5068	quantifiers_state.cpp	blob \| history \| raw
-rw-r--r--	3105	quantifiers_state.h	blob \| history \| raw
-rw-r--r--	2020	quantifiers_statistics.cpp	blob \| history \| raw
-rw-r--r--	1462	quantifiers_statistics.h	blob \| history \| raw
-rw-r--r--	12966	query_generator.cpp	blob \| history \| raw
-rw-r--r--	4587	query_generator.h	blob \| history \| raw
-rw-r--r--	13628	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5688	relevant_domain.h	blob \| history \| raw
-rw-r--r--	18567	single_inv_partition.cpp	blob \| history \| raw
-rw-r--r--	10760	single_inv_partition.h	blob \| history \| raw
-rw-r--r--	12593	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5865	skolemize.h	blob \| history \| raw
-rw-r--r--	3378	solution_filter.cpp	blob \| history \| raw
-rw-r--r--	2562	solution_filter.h	blob \| history \| raw
drwxr-xr-x	-	sygus	tree \| history
-rw-r--r--	17261	sygus_inst.cpp	blob \| history \| raw
-rw-r--r--	4753	sygus_inst.h	blob \| history \| raw
-rw-r--r--	23052	sygus_sampler.cpp	blob \| history \| raw
-rw-r--r--	13429	sygus_sampler.h	blob \| history \| raw
-rw-r--r--	19936	term_database.cpp	blob \| history \| raw
-rw-r--r--	11826	term_database.h	blob \| history \| raw
-rw-r--r--	2020	term_enumeration.cpp	blob \| history \| raw
-rw-r--r--	2323	term_enumeration.h	blob \| history \| raw
-rw-r--r--	4177	term_pools.cpp	blob \| history \| raw
-rw-r--r--	3316	term_pools.h	blob \| history \| raw
-rw-r--r--	4464	term_registry.cpp	blob \| history \| raw
-rw-r--r--	3848	term_registry.h	blob \| history \| raw
-rw-r--r--	18625	term_tuple_enumerator.cpp	blob \| history \| raw
-rw-r--r--	3972	term_tuple_enumerator.h	blob \| history \| raw
-rw-r--r--	14558	term_util.cpp	blob \| history \| raw
-rw-r--r--	7154	term_util.h	blob \| history \| raw
-rw-r--r--	5548	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	3753	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	4694	theory_quantifiers_type_rules.cpp	blob \| history \| raw
-rw-r--r--	1602	theory_quantifiers_type_rules.h	blob \| history \| raw