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

drwxr-xr-x		..
-rwxr-xr-x	4132	alpha_equivalence.cpp	blob \| history \| raw
-rwxr-xr-x	1776	alpha_equivalence.h	blob \| history \| raw
-rwxr-xr-x	36829	ambqi_builder.cpp	blob \| history \| raw
-rwxr-xr-x	4432	ambqi_builder.h	blob \| history \| raw
-rwxr-xr-x	10791	anti_skolem.cpp	blob \| history \| raw
-rwxr-xr-x	2366	anti_skolem.h	blob \| history \| raw
-rwxr-xr-x	25047	bounded_integers.cpp	blob \| history \| raw
-rwxr-xr-x	6066	bounded_integers.h	blob \| history \| raw
-rwxr-xr-x	10033	candidate_generator.cpp	blob \| history \| raw
-rwxr-xr-x	5075	candidate_generator.h	blob \| history \| raw
-rwxr-xr-x	37012	ce_guided_instantiation.cpp	blob \| history \| raw
-rwxr-xr-x	6352	ce_guided_instantiation.h	blob \| history \| raw
-rwxr-xr-x	52239	ce_guided_single_inv.cpp	blob \| history \| raw
-rwxr-xr-x	8438	ce_guided_single_inv.h	blob \| history \| raw
-rwxr-xr-x	1527	ce_guided_single_inv_ei.cpp	blob \| history \| raw
-rwxr-xr-x	1172	ce_guided_single_inv_ei.h	blob \| history \| raw
-rwxr-xr-x	47992	ce_guided_single_inv_sol.cpp	blob \| history \| raw
-rwxr-xr-x	3691	ce_guided_single_inv_sol.h	blob \| history \| raw
-rwxr-xr-x	75743	ceg_instantiator.cpp	blob \| history \| raw
-rwxr-xr-x	5676	ceg_instantiator.h	blob \| history \| raw
-rwxr-xr-x	85013	conjecture_generator.cpp	blob \| history \| raw
-rwxr-xr-x	15658	conjecture_generator.h	blob \| history \| raw
-rwxr-xr-x	16757	equality_infer.cpp	blob \| history \| raw
-rwxr-xr-x	3582	equality_infer.h	blob \| history \| raw
-rwxr-xr-x	32092	first_order_model.cpp	blob \| history \| raw
-rwxr-xr-x	8217	first_order_model.h	blob \| history \| raw
-rwxr-xr-x	55337	full_model_check.cpp	blob \| history \| raw
-rwxr-xr-x	6512	full_model_check.h	blob \| history \| raw
-rwxr-xr-x	1554	fun_def_engine.cpp	blob \| history \| raw
-rwxr-xr-x	1696	fun_def_engine.h	blob \| history \| raw
-rwxr-xr-x	9450	fun_def_process.cpp	blob \| history \| raw
-rwxr-xr-x	1594	fun_def_process.h	blob \| history \| raw
-rwxr-xr-x	14454	inst_match.cpp	blob \| history \| raw
-rwxr-xr-x	9781	inst_match.h	blob \| history \| raw
-rwxr-xr-x	34200	inst_match_generator.cpp	blob \| history \| raw
-rwxr-xr-x	10299	inst_match_generator.h	blob \| history \| raw
-rwxr-xr-x	30587	inst_propagator.cpp	blob \| history \| raw
-rwxr-xr-x	6573	inst_propagator.h	blob \| history \| raw
-rwxr-xr-x	28016	inst_strategy_cbqi.cpp	blob \| history \| raw
-rwxr-xr-x	5538	inst_strategy_cbqi.h	blob \| history \| raw
-rwxr-xr-x	31324	inst_strategy_e_matching.cpp	blob \| history \| raw
-rwxr-xr-x	4724	inst_strategy_e_matching.h	blob \| history \| raw
-rwxr-xr-x	7635	instantiation_engine.cpp	blob \| history \| raw
-rwxr-xr-x	3233	instantiation_engine.h	blob \| history \| raw
-rwxr-xr-x	3426	kinds	blob \| history \| raw
-rwxr-xr-x	9376	local_theory_ext.cpp	blob \| history \| raw
-rwxr-xr-x	2750	local_theory_ext.h	blob \| history \| raw
-rwxr-xr-x	20155	macros.cpp	blob \| history \| raw
-rwxr-xr-x	2612	macros.h	blob \| history \| raw
-rwxr-xr-x	32948	model_builder.cpp	blob \| history \| raw
-rwxr-xr-x	6821	model_builder.h	blob \| history \| raw
-rwxr-xr-x	12777	model_engine.cpp	blob \| history \| raw
-rwxr-xr-x	2358	model_engine.h	blob \| history \| raw
-rwxr-xr-x	85560	quant_conflict_find.cpp	blob \| history \| raw
-rwxr-xr-x	9748	quant_conflict_find.h	blob \| history \| raw
-rwxr-xr-x	7078	quant_equality_engine.cpp	blob \| history \| raw
-rwxr-xr-x	3778	quant_equality_engine.h	blob \| history \| raw
-rwxr-xr-x	5245	quant_split.cpp	blob \| history \| raw
-rwxr-xr-x	1730	quant_split.h	blob \| history \| raw
-rwxr-xr-x	13246	quant_util.cpp	blob \| history \| raw
-rwxr-xr-x	6573	quant_util.h	blob \| history \| raw
-rwxr-xr-x	2942	quantifiers_attributes.cpp	blob \| history \| raw
-rwxr-xr-x	1408	quantifiers_attributes.h	blob \| history \| raw
-rwxr-xr-x	64992	quantifiers_rewriter.cpp	blob \| history \| raw
-rwxr-xr-x	4834	quantifiers_rewriter.h	blob \| history \| raw
-rwxr-xr-x	10991	relevant_domain.cpp	blob \| history \| raw
-rwxr-xr-x	2526	relevant_domain.h	blob \| history \| raw
-rwxr-xr-x	12049	rewrite_engine.cpp	blob \| history \| raw
-rwxr-xr-x	2125	rewrite_engine.h	blob \| history \| raw
-rwxr-xr-x	12331	symmetry_breaking.cpp	blob \| history \| raw
-rwxr-xr-x	3618	symmetry_breaking.h	blob \| history \| raw
-rwxr-xr-x	113964	term_database.cpp	blob \| history \| raw
-rwxr-xr-x	26893	term_database.h	blob \| history \| raw
-rwxr-xr-x	6206	theory_quantifiers.cpp	blob \| history \| raw
-rwxr-xr-x	2558	theory_quantifiers.h	blob \| history \| raw
-rwxr-xr-x	9316	theory_quantifiers_type_rules.h	blob \| history \| raw
-rwxr-xr-x	26647	trigger.cpp	blob \| history \| raw
-rwxr-xr-x	7016	trigger.h	blob \| history \| raw