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

drwxr-xr-x		..
-rw-r--r--	3449	alpha_equivalence.cpp	blob \| history \| raw
-rw-r--r--	3142	alpha_equivalence.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--	10148	candidate_rewrite_database.cpp	blob \| history \| raw
-rw-r--r--	5605	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--	87044	conjecture_generator.cpp	blob \| history \| raw
-rw-r--r--	16345	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--	6568	equality_query.cpp	blob \| history \| raw
-rw-r--r--	3649	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--	14576	first_order_model.cpp	blob \| history \| raw
-rw-r--r--	7770	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--	2393	inst_match.cpp	blob \| history \| raw
-rw-r--r--	2898	inst_match.h	blob \| history \| raw
-rw-r--r--	14951	inst_match_trie.cpp	blob \| history \| raw
-rw-r--r--	15778	inst_match_trie.h	blob \| history \| raw
-rw-r--r--	10733	inst_strategy_enumerative.cpp	blob \| history \| raw
-rw-r--r--	4270	inst_strategy_enumerative.h	blob \| history \| raw
-rw-r--r--	25975	instantiate.cpp	blob \| history \| raw
-rw-r--r--	13993	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--	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--	83958	quant_conflict_find.cpp	blob \| history \| raw
-rw-r--r--	10909	quant_conflict_find.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--	2467	quant_rep_bound_ext.cpp	blob \| history \| raw
-rw-r--r--	2203	quant_rep_bound_ext.h	blob \| history \| raw
-rw-r--r--	7021	quant_split.cpp	blob \| history \| raw
-rw-r--r--	2600	quant_split.h	blob \| history \| raw
-rw-r--r--	5844	quant_util.cpp	blob \| history \| raw
-rw-r--r--	8672	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--	1012	quantifiers_inference_manager.cpp	blob \| history \| raw
-rw-r--r--	1357	quantifiers_inference_manager.h	blob \| history \| raw
-rw-r--r--	3350	quantifiers_modules.cpp	blob \| history \| raw
-rw-r--r--	3243	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--	12201	relevant_domain.cpp	blob \| history \| raw
-rw-r--r--	5565	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--	12840	skolemize.cpp	blob \| history \| raw
-rw-r--r--	5818	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--	16911	sygus_inst.cpp	blob \| history \| raw
-rw-r--r--	4860	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--	37631	term_database.cpp	blob \| history \| raw
-rw-r--r--	17160	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--	18815	term_util.cpp	blob \| history \| raw
-rw-r--r--	10571	term_util.h	blob \| history \| raw
-rw-r--r--	5926	theory_quantifiers.cpp	blob \| history \| raw
-rw-r--r--	3529	theory_quantifiers.h	blob \| history \| raw
-rw-r--r--	5704	theory_quantifiers_type_rules.h	blob \| history \| raw