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_single_inv.cpp	40511	log plain
-rw-r--r--	ce_guided_single_inv.h	10364	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	58496	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7831	log plain
-rw-r--r--	cegis.cpp	21063	log plain
-rw-r--r--	cegis.h	8104	log plain
-rw-r--r--	cegis_unif.cpp	23436	log plain
-rw-r--r--	cegis_unif.h	12376	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	35294	log plain
-rw-r--r--	sygus_grammar_cons.h	6737	log plain
-rw-r--r--	sygus_grammar_norm.cpp	21375	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	8215	log plain
-rw-r--r--	sygus_invariance.h	9078	log plain
-rw-r--r--	sygus_module.cpp	900	log plain
-rw-r--r--	sygus_module.h	5957	log plain
-rw-r--r--	sygus_pbe.cpp	16587	log plain
-rw-r--r--	sygus_pbe.h	13395	log plain
-rw-r--r--	sygus_process_conj.cpp	24851	log plain
-rw-r--r--	sygus_process_conj.h	12793	log plain
-rw-r--r--	sygus_repair_const.cpp	20963	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	46826	log plain
-rw-r--r--	sygus_unif_io.h	17003	log plain
-rw-r--r--	sygus_unif_rl.cpp	39684	log plain
-rw-r--r--	sygus_unif_rl.h	17960	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--	synth_conjecture.cpp	31219	log plain
-rw-r--r--	synth_conjecture.h	11889	log plain
-rw-r--r--	synth_engine.cpp	13676	log plain
-rw-r--r--	synth_engine.h	3557	log plain
-rw-r--r--	term_database_sygus.cpp	49072	log plain
-rw-r--r--	term_database_sygus.h	23800	log plain