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	18772	log plain
-rw-r--r--	ce_guided_single_inv.h	6796	log plain
-rw-r--r--	cegis.cpp	24428	log plain
-rw-r--r--	cegis.h	10106	log plain
-rw-r--r--	cegis_core_connective.cpp	28819	log plain
-rw-r--r--	cegis_core_connective.h	15322	log plain
-rw-r--r--	cegis_unif.cpp	26049	log plain
-rw-r--r--	cegis_unif.h	14426	log plain
-rw-r--r--	enum_stream_substitution.cpp	19306	log plain
-rw-r--r--	enum_stream_substitution.h	11173	log plain
-rw-r--r--	example_eval_cache.cpp	3663	log plain
-rw-r--r--	example_eval_cache.h	6729	log plain
-rw-r--r--	example_infer.cpp	7549	log plain
-rw-r--r--	example_infer.h	6267	log plain
-rw-r--r--	example_min_eval.cpp	2583	log plain
-rw-r--r--	example_min_eval.h	3650	log plain
-rw-r--r--	rcons_obligation_info.cpp	2803	log plain
-rw-r--r--	rcons_obligation_info.h	5280	log plain
-rw-r--r--	rcons_type_info.cpp	2147	log plain
-rw-r--r--	rcons_type_info.h	3393	log plain
-rw-r--r--	sygus_abduct.cpp	7466	log plain
-rw-r--r--	sygus_abduct.h	3467	log plain
-rw-r--r--	sygus_enumerator.cpp	39688	log plain
-rw-r--r--	sygus_enumerator.h	21216	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1490	log plain
-rw-r--r--	sygus_enumerator_basic.h	2178	log plain
-rw-r--r--	sygus_eval_unfold.cpp	11258	log plain
-rw-r--r--	sygus_eval_unfold.h	6646	log plain
-rw-r--r--	sygus_explain.cpp	10825	log plain
-rw-r--r--	sygus_explain.h	8823	log plain
-rw-r--r--	sygus_grammar_cons.cpp	61554	log plain
-rw-r--r--	sygus_grammar_cons.h	10275	log plain
-rw-r--r--	sygus_grammar_norm.cpp	19630	log plain
-rw-r--r--	sygus_grammar_norm.h	15501	log plain
-rw-r--r--	sygus_grammar_red.cpp	5794	log plain
-rw-r--r--	sygus_grammar_red.h	4098	log plain
-rw-r--r--	sygus_interpol.cpp	13251	log plain
-rw-r--r--	sygus_interpol.h	8296	log plain
-rw-r--r--	sygus_invariance.cpp	8477	log plain
-rw-r--r--	sygus_invariance.h	9437	log plain
-rw-r--r--	sygus_module.cpp	931	log plain
-rw-r--r--	sygus_module.h	6588	log plain
-rw-r--r--	sygus_pbe.cpp	9383	log plain
-rw-r--r--	sygus_pbe.h	7243	log plain
-rw-r--r--	sygus_process_conj.cpp	24697	log plain
-rw-r--r--	sygus_process_conj.h	12708	log plain
-rw-r--r--	sygus_qe_preproc.cpp	5064	log plain
-rw-r--r--	sygus_qe_preproc.h	1570	log plain
-rw-r--r--	sygus_reconstruct.cpp	16265	log plain
-rw-r--r--	sygus_reconstruct.h	11459	log plain
-rw-r--r--	sygus_repair_const.cpp	19954	log plain
-rw-r--r--	sygus_repair_const.h	8996	log plain
-rw-r--r--	sygus_stats.cpp	2631	log plain
-rw-r--r--	sygus_stats.h	1789	log plain
-rw-r--r--	sygus_unif.cpp	3426	log plain
-rw-r--r--	sygus_unif.h	7877	log plain
-rw-r--r--	sygus_unif_io.cpp	54884	log plain
-rw-r--r--	sygus_unif_io.h	17730	log plain
-rw-r--r--	sygus_unif_rl.cpp	43614	log plain
-rw-r--r--	sygus_unif_rl.h	18434	log plain
-rw-r--r--	sygus_unif_strat.cpp	34938	log plain
-rw-r--r--	sygus_unif_strat.h	15114	log plain
-rw-r--r--	sygus_utils.cpp	5414	log plain
-rw-r--r--	sygus_utils.h	4204	log plain
-rw-r--r--	synth_conjecture.cpp	44416	log plain
-rw-r--r--	synth_conjecture.h	18036	log plain
-rw-r--r--	synth_engine.cpp	8439	log plain
-rw-r--r--	synth_engine.h	4535	log plain
-rw-r--r--	template_infer.cpp	6358	log plain
-rw-r--r--	template_infer.h	2332	log plain
-rw-r--r--	term_database_sygus.cpp	32774	log plain
-rw-r--r--	term_database_sygus.h	20240	log plain
-rw-r--r--	transition_inference.cpp	16615	log plain
-rw-r--r--	transition_inference.h	13160	log plain
-rw-r--r--	type_info.cpp	13631	log plain
-rw-r--r--	type_info.h	9335	log plain
-rw-r--r--	type_node_id_trie.cpp	1373	log plain
-rw-r--r--	type_node_id_trie.h	1578	log plain