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

drwxr-xr-x		..
-rw-r--r--	4600	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	3767	alpha_equivalence.h	blob \| history \| raw
-rw-r--r--	11338	anti_skolem.cpp	blob \| history \| raw
-rw-r--r--	2713	anti_skolem.h	blob \| history \| raw
-rw-r--r--	13202	bv_inverter.cpp	blob \| history \| raw
-rw-r--r--	4055	bv_inverter.h	blob \| history \| raw
-rw-r--r--	75900	bv_inverter_utils.cpp	blob \| history \| raw
-rw-r--r--	2437	bv_inverter_utils.h	blob \| history \| raw
-rw-r--r--	9916	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	5351	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--	87015	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16177	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--	16875	equality_infer.cpp	blob \| history \| raw
-rw-r--r--	3536	equality_infer.h	blob \| history \| raw
-rw-r--r--	8177	equality_query.cpp	blob \| history \| raw
-rw-r--r--	4812	equality_query.h	blob \| history \| raw
-rw-r--r--	2858	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--	49953	extended_rewrite.cpp	blob \| history \| raw
-rw-r--r--	9583	extended_rewrite.h	blob \| history \| raw
-rw-r--r--	14458	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	7641	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--	2866	inst_match.cpp	blob \| history \| raw
-rw-r--r--	3114	inst_match.h	blob \| history \| raw
-rw-r--r--	15043	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	15799	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	10464	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	4157	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	28309	instantiate.cpp	blob \| history \| raw
-rw-r--r--	14663	instantiate.h	blob \| history \| raw
-rw-r--r--	2563	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--	3894	proof_checker.cpp	blob \| history \| raw
-rw-r--r--	1500	proof_checker.h	blob \| history \| raw
-rw-r--r--	84024	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	10835	quant_conflict_find.h	blob \| history \| raw
-rw-r--r--	1472	quant_relevance.cpp	blob \| history \| raw
-rw-r--r--	2114	quant_relevance.h	blob \| history \| raw
-rw-r--r--	2467	quant_rep_bound_ext.cpp	blob \| history \| raw
-rw-r--r--	2203	quant_rep_bound_ext.h	blob \| history \| raw
-rw-r--r--	6932	quant_split.cpp	blob \| history \| raw
-rw-r--r--	2540	quant_split.h	blob \| history \| raw
-rw-r--r--	5593	quant_util.cpp	blob \| history \| raw
-rw-r--r--	9194	quant_util.h	blob \| history \| raw
-rw-r--r--	11998	quantifiers_attributes.cpp	blob \| history \| raw
-rw-r--r--	8248	quantifiers_attributes.h	blob \| history \| raw
-rw-r--r--	3542	quantifiers_modules.cpp	blob \| history \| raw
-rw-r--r--	3492	quantifiers_modules.h	blob \| history \| raw
-rw-r--r--	67298	quantifiers_rewriter.cpp	blob \| history \| raw
-rw-r--r--	12512	quantifiers_rewriter.h	blob \| history \| raw
-rw-r--r--	940	quantifiers_state.cpp	blob \| history \| raw
-rw-r--r--	1119	quantifiers_state.h	blob \| history \| raw
-rw-r--r--	12981	query_generator.cpp	blob \| history \| raw
-rw-r--r--	4584	query_generator.h	blob \| history \| raw
-rw-r--r--	12158	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5569	relevant_domain.h	blob \| history \| raw
-rw-r--r--	18622	single_inv_partition.cpp	blob \| history \| raw
-rw-r--r--	10835	single_inv_partition.h	blob \| history \| raw
-rw-r--r--	12853	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5659	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--	16847	sygus_inst.cpp	blob \| history \| raw
-rw-r--r--	4780	sygus_inst.h	blob \| history \| raw
-rw-r--r--	23384	sygus_sampler.cpp	blob \| history \| raw
-rw-r--r--	13279	sygus_sampler.h	blob \| history \| raw
-rw-r--r--	38443	term_database.cpp	blob \| history \| raw
-rw-r--r--	17283	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--	18890	term_util.cpp	blob \| history \| raw
-rw-r--r--	10683	term_util.h	blob \| history \| raw
-rw-r--r--	5434	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	3181	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	5704	theory_quantifiers_type_rules.h	blob \| history \| raw