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	27233	log plain
-rw-r--r--	ce_guided_conjecture.h	11047	log plain
-rw-r--r--	ce_guided_instantiation.cpp	8515	log plain
-rw-r--r--	ce_guided_instantiation.h	3042	log plain
-rw-r--r--	ce_guided_single_inv.cpp	39506	log plain
-rw-r--r--	ce_guided_single_inv.h	9277	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	57803	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7497	log plain
-rw-r--r--	cegis.cpp	17441	log plain
-rw-r--r--	cegis.h	7270	log plain
-rw-r--r--	cegis_unif.cpp	21812	log plain
-rw-r--r--	cegis_unif.h	12435	log plain
-rw-r--r--	sygus_eval_unfold.cpp	6741	log plain
-rw-r--r--	sygus_eval_unfold.h	4473	log plain
-rw-r--r--	sygus_explain.cpp	9589	log plain
-rw-r--r--	sygus_explain.h	8530	log plain
-rw-r--r--	sygus_grammar_cons.cpp	33489	log plain
-rw-r--r--	sygus_grammar_cons.h	6895	log plain
-rw-r--r--	sygus_grammar_norm.cpp	18488	log plain
-rw-r--r--	sygus_grammar_norm.h	16349	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	7489	log plain
-rw-r--r--	sygus_invariance.h	8390	log plain
-rw-r--r--	sygus_module.cpp	898	log plain
-rw-r--r--	sygus_module.h	5364	log plain
-rw-r--r--	sygus_pbe.cpp	15550	log plain
-rw-r--r--	sygus_pbe.h	13232	log plain
-rw-r--r--	sygus_process_conj.cpp	24588	log plain
-rw-r--r--	sygus_process_conj.h	12715	log plain
-rw-r--r--	sygus_repair_const.cpp	17475	log plain
-rw-r--r--	sygus_repair_const.h	7288	log plain
-rw-r--r--	sygus_unif.cpp	3692	log plain
-rw-r--r--	sygus_unif.h	7707	log plain
-rw-r--r--	sygus_unif_io.cpp	44071	log plain
-rw-r--r--	sygus_unif_io.h	15928	log plain
-rw-r--r--	sygus_unif_rl.cpp	31288	log plain
-rw-r--r--	sygus_unif_rl.h	13081	log plain
-rw-r--r--	sygus_unif_strat.cpp	35003	log plain
-rw-r--r--	sygus_unif_strat.h	14754	log plain
-rw-r--r--	term_database_sygus.cpp	50896	log plain
-rw-r--r--	term_database_sygus.h	15503	log plain