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	23616	log plain
-rw-r--r--	ce_guided_single_inv.h	6956	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	37407	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7554	log plain
-rw-r--r--	cegis.cpp	24475	log plain
-rw-r--r--	cegis.h	10104	log plain
-rw-r--r--	cegis_core_connective.cpp	28666	log plain
-rw-r--r--	cegis_core_connective.h	15206	log plain
-rw-r--r--	cegis_unif.cpp	25934	log plain
-rw-r--r--	cegis_unif.h	14128	log plain
-rw-r--r--	enum_stream_substitution.cpp	19251	log plain
-rw-r--r--	enum_stream_substitution.h	11174	log plain
-rw-r--r--	example_eval_cache.cpp	3664	log plain
-rw-r--r--	example_eval_cache.h	6733	log plain
-rw-r--r--	example_infer.cpp	7550	log plain
-rw-r--r--	example_infer.h	6353	log plain
-rw-r--r--	example_min_eval.cpp	2587	log plain
-rw-r--r--	example_min_eval.h	3654	log plain
-rw-r--r--	sygus_abduct.cpp	7751	log plain
-rw-r--r--	sygus_abduct.h	3463	log plain
-rw-r--r--	sygus_enumerator.cpp	39542	log plain
-rw-r--r--	sygus_enumerator.h	21217	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1494	log plain
-rw-r--r--	sygus_enumerator_basic.h	2179	log plain
-rw-r--r--	sygus_eval_unfold.cpp	11038	log plain
-rw-r--r--	sygus_eval_unfold.h	6647	log plain
-rw-r--r--	sygus_explain.cpp	10735	log plain
-rw-r--r--	sygus_explain.h	8858	log plain
-rw-r--r--	sygus_grammar_cons.cpp	57538	log plain
-rw-r--r--	sygus_grammar_cons.h	10733	log plain
-rw-r--r--	sygus_grammar_norm.cpp	19674	log plain
-rw-r--r--	sygus_grammar_norm.h	15657	log plain
-rw-r--r--	sygus_grammar_red.cpp	5884	log plain
-rw-r--r--	sygus_grammar_red.h	4157	log plain
-rw-r--r--	sygus_interpol.cpp	13108	log plain
-rw-r--r--	sygus_interpol.h	8350	log plain
-rw-r--r--	sygus_invariance.cpp	8475	log plain
-rw-r--r--	sygus_invariance.h	9464	log plain
-rw-r--r--	sygus_module.cpp	940	log plain
-rw-r--r--	sygus_module.h	6551	log plain
-rw-r--r--	sygus_pbe.cpp	9239	log plain
-rw-r--r--	sygus_pbe.h	7284	log plain
-rw-r--r--	sygus_process_conj.cpp	24756	log plain
-rw-r--r--	sygus_process_conj.h	12784	log plain
-rw-r--r--	sygus_repair_const.cpp	19852	log plain
-rw-r--r--	sygus_repair_const.h	9171	log plain
-rw-r--r--	sygus_stats.cpp	2635	log plain
-rw-r--r--	sygus_stats.h	1793	log plain
-rw-r--r--	sygus_unif.cpp	3552	log plain
-rw-r--r--	sygus_unif.h	8009	log plain
-rw-r--r--	sygus_unif_io.cpp	54925	log plain
-rw-r--r--	sygus_unif_io.h	17762	log plain
-rw-r--r--	sygus_unif_rl.cpp	43590	log plain
-rw-r--r--	sygus_unif_rl.h	18440	log plain
-rw-r--r--	sygus_unif_strat.cpp	34972	log plain
-rw-r--r--	sygus_unif_strat.h	15153	log plain
-rw-r--r--	synth_conjecture.cpp	44880	log plain
-rw-r--r--	synth_conjecture.h	18084	log plain
-rw-r--r--	synth_engine.cpp	13385	log plain
-rw-r--r--	synth_engine.h	4292	log plain
-rw-r--r--	term_database_sygus.cpp	32713	log plain
-rw-r--r--	term_database_sygus.h	20091	log plain
-rw-r--r--	transition_inference.cpp	16587	log plain
-rw-r--r--	transition_inference.h	13164	log plain
-rw-r--r--	type_info.cpp	13547	log plain
-rw-r--r--	type_info.h	9417	log plain
-rw-r--r--	type_node_id_trie.cpp	1374	log plain
-rw-r--r--	type_node_id_trie.h	1599	log plain