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	30908	log plain
-rw-r--r--	ce_guided_conjecture.h	11060	log plain
-rw-r--r--	ce_guided_instantiation.cpp	14067	log plain
-rw-r--r--	ce_guided_instantiation.h	3624	log plain
-rw-r--r--	ce_guided_single_inv.cpp	40552	log plain
-rw-r--r--	ce_guided_single_inv.h	10390	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	58195	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7880	log plain
-rw-r--r--	cegis.cpp	19299	log plain
-rw-r--r--	cegis.h	7804	log plain
-rw-r--r--	cegis_unif.cpp	23830	log plain
-rw-r--r--	cegis_unif.h	13199	log plain
-rw-r--r--	sygus_eval_unfold.cpp	6613	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	8833	log plain
-rw-r--r--	sygus_grammar_cons.cpp	35275	log plain
-rw-r--r--	sygus_grammar_cons.h	6731	log plain
-rw-r--r--	sygus_grammar_norm.cpp	21434	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	9072	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	16260	log plain
-rw-r--r--	sygus_pbe.h	13244	log plain
-rw-r--r--	sygus_process_conj.cpp	24876	log plain
-rw-r--r--	sygus_process_conj.h	12725	log plain
-rw-r--r--	sygus_repair_const.cpp	20988	log plain
-rw-r--r--	sygus_repair_const.h	9286	log plain
-rw-r--r--	sygus_unif.cpp	3119	log plain
-rw-r--r--	sygus_unif.h	7727	log plain
-rw-r--r--	sygus_unif_io.cpp	46602	log plain
-rw-r--r--	sygus_unif_io.h	17003	log plain
-rw-r--r--	sygus_unif_rl.cpp	34164	log plain
-rw-r--r--	sygus_unif_rl.h	14584	log plain
-rw-r--r--	sygus_unif_strat.cpp	35439	log plain
-rw-r--r--	sygus_unif_strat.h	15170	log plain
-rw-r--r--	term_database_sygus.cpp	44271	log plain
-rw-r--r--	term_database_sygus.h	19874	log plain