sygus « quantifiers « theory « src - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	ce_guided_conjecture.cpp	30444	log plain
-rw-r--r--	ce_guided_conjecture.h	11478	log plain
-rw-r--r--	ce_guided_instantiation.cpp	8515	log plain
-rw-r--r--	ce_guided_instantiation.h	3059	log plain
-rw-r--r--	ce_guided_single_inv.cpp	39532	log plain
-rw-r--r--	ce_guided_single_inv.h	9055	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	58251	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7880	log plain
-rw-r--r--	cegis.cpp	19080	log plain
-rw-r--r--	cegis.h	7803	log plain
-rw-r--r--	cegis_unif.cpp	21812	log plain
-rw-r--r--	cegis_unif.h	12460	log plain
-rw-r--r--	sygus_eval_unfold.cpp	6778	log plain
-rw-r--r--	sygus_eval_unfold.h	4473	log plain
-rw-r--r--	sygus_explain.cpp	10505	log plain
-rw-r--r--	sygus_explain.h	8832	log plain
-rw-r--r--	sygus_grammar_cons.cpp	33207	log plain
-rw-r--r--	sygus_grammar_cons.h	6805	log plain
-rw-r--r--	sygus_grammar_norm.cpp	20338	log plain
-rw-r--r--	sygus_grammar_norm.h	16376	log plain
-rw-r--r--	sygus_grammar_red.cpp	4371	log plain
-rw-r--r--	sygus_grammar_red.h	4099	log plain
-rw-r--r--	sygus_invariance.cpp	8217	log plain
-rw-r--r--	sygus_invariance.h	9036	log plain
-rw-r--r--	sygus_module.cpp	898	log plain
-rw-r--r--	sygus_module.h	5661	log plain
-rw-r--r--	sygus_pbe.cpp	16298	log plain
-rw-r--r--	sygus_pbe.h	13244	log plain
-rw-r--r--	sygus_process_conj.cpp	24647	log plain
-rw-r--r--	sygus_process_conj.h	12725	log plain
-rw-r--r--	sygus_repair_const.cpp	19152	log plain
-rw-r--r--	sygus_repair_const.h	8383	log plain
-rw-r--r--	sygus_unif.cpp	3708	log plain
-rw-r--r--	sygus_unif.h	7723	log plain
-rw-r--r--	sygus_unif_io.cpp	46573	log plain
-rw-r--r--	sygus_unif_io.h	17075	log plain
-rw-r--r--	sygus_unif_rl.cpp	31717	log plain
-rw-r--r--	sygus_unif_rl.h	13367	log plain
-rw-r--r--	sygus_unif_strat.cpp	35477	log plain
-rw-r--r--	sygus_unif_strat.h	15154	log plain
-rw-r--r--	term_database_sygus.cpp	60728	log plain
-rw-r--r--	term_database_sygus.h	20466	log plain