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	18831	log plain
-rw-r--r--	ce_guided_single_inv.h	6719	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	36615	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7423	log plain
-rw-r--r--	cegis.cpp	24440	log plain
-rw-r--r--	cegis.h	10103	log plain
-rw-r--r--	cegis_core_connective.cpp	28724	log plain
-rw-r--r--	cegis_core_connective.h	15205	log plain
-rw-r--r--	cegis_unif.cpp	25988	log plain
-rw-r--r--	cegis_unif.h	14235	log plain
-rw-r--r--	enum_stream_substitution.cpp	19262	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	6732	log plain
-rw-r--r--	example_infer.cpp	7549	log plain
-rw-r--r--	example_infer.h	6352	log plain
-rw-r--r--	example_min_eval.cpp	2586	log plain
-rw-r--r--	example_min_eval.h	3653	log plain
-rw-r--r--	sygus_abduct.cpp	7446	log plain
-rw-r--r--	sygus_abduct.h	3467	log plain
-rw-r--r--	sygus_enumerator.cpp	39541	log plain
-rw-r--r--	sygus_enumerator.h	21216	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1493	log plain
-rw-r--r--	sygus_enumerator_basic.h	2178	log plain
-rw-r--r--	sygus_eval_unfold.cpp	11200	log plain
-rw-r--r--	sygus_eval_unfold.h	6646	log plain
-rw-r--r--	sygus_explain.cpp	10734	log plain
-rw-r--r--	sygus_explain.h	8857	log plain
-rw-r--r--	sygus_grammar_cons.cpp	61693	log plain
-rw-r--r--	sygus_grammar_cons.h	10302	log plain
-rw-r--r--	sygus_grammar_norm.cpp	19590	log plain
-rw-r--r--	sygus_grammar_norm.h	15519	log plain
-rw-r--r--	sygus_grammar_red.cpp	5791	log plain
-rw-r--r--	sygus_grammar_red.h	4124	log plain
-rw-r--r--	sygus_interpol.cpp	13231	log plain
-rw-r--r--	sygus_interpol.h	8296	log plain
-rw-r--r--	sygus_invariance.cpp	8474	log plain
-rw-r--r--	sygus_invariance.h	9463	log plain
-rw-r--r--	sygus_module.cpp	939	log plain
-rw-r--r--	sygus_module.h	6550	log plain
-rw-r--r--	sygus_pbe.cpp	9238	log plain
-rw-r--r--	sygus_pbe.h	7283	log plain
-rw-r--r--	sygus_process_conj.cpp	24755	log plain
-rw-r--r--	sygus_process_conj.h	12783	log plain
-rw-r--r--	sygus_qe_preproc.cpp	5085	log plain
-rw-r--r--	sygus_qe_preproc.h	1768	log plain
-rw-r--r--	sygus_repair_const.cpp	20023	log plain
-rw-r--r--	sygus_repair_const.h	9154	log plain
-rw-r--r--	sygus_stats.cpp	2634	log plain
-rw-r--r--	sygus_stats.h	1792	log plain
-rw-r--r--	sygus_unif.cpp	3551	log plain
-rw-r--r--	sygus_unif.h	8008	log plain
-rw-r--r--	sygus_unif_io.cpp	54924	log plain
-rw-r--r--	sygus_unif_io.h	17761	log plain
-rw-r--r--	sygus_unif_rl.cpp	43589	log plain
-rw-r--r--	sygus_unif_rl.h	18439	log plain
-rw-r--r--	sygus_unif_strat.cpp	34971	log plain
-rw-r--r--	sygus_unif_strat.h	15152	log plain
-rw-r--r--	sygus_utils.cpp	5394	log plain
-rw-r--r--	sygus_utils.h	4204	log plain
-rw-r--r--	synth_conjecture.cpp	44119	log plain
-rw-r--r--	synth_conjecture.h	18026	log plain
-rw-r--r--	synth_engine.cpp	8561	log plain
-rw-r--r--	synth_engine.h	4602	log plain
-rw-r--r--	template_infer.cpp	6358	log plain
-rw-r--r--	template_infer.h	2335	log plain
-rw-r--r--	term_database_sygus.cpp	32802	log plain
-rw-r--r--	term_database_sygus.h	20308	log plain
-rw-r--r--	transition_inference.cpp	16586	log plain
-rw-r--r--	transition_inference.h	13163	log plain
-rw-r--r--	type_info.cpp	13546	log plain
-rw-r--r--	type_info.h	9416	log plain
-rw-r--r--	type_node_id_trie.cpp	1373	log plain
-rw-r--r--	type_node_id_trie.h	1598	log plain