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	27129	log plain
-rw-r--r--	ce_guided_conjecture.h	10391	log plain
-rw-r--r--	ce_guided_instantiation.cpp	8631	log plain
-rw-r--r--	ce_guided_instantiation.h	3042	log plain
-rw-r--r--	ce_guided_single_inv.cpp	38665	log plain
-rw-r--r--	ce_guided_single_inv.h	9277	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	57908	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7497	log plain
-rw-r--r--	cegis.cpp	13083	log plain
-rw-r--r--	cegis.h	4853	log plain
-rw-r--r--	sygus_explain.cpp	8878	log plain
-rw-r--r--	sygus_explain.h	7711	log plain
-rw-r--r--	sygus_grammar_cons.cpp	28604	log plain
-rw-r--r--	sygus_grammar_cons.h	5646	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	7608	log plain
-rw-r--r--	sygus_invariance.h	8456	log plain
-rw-r--r--	sygus_module.cpp	863	log plain
-rw-r--r--	sygus_module.h	5091	log plain
-rw-r--r--	sygus_pbe.cpp	87519	log plain
-rw-r--r--	sygus_pbe.h	33632	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--	term_database_sygus.cpp	54168	log plain
-rw-r--r--	term_database_sygus.h	14170	log plain