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	39467	log plain
-rw-r--r--	ce_guided_single_inv.h	12317	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	58512	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7831	log plain
-rw-r--r--	cegis.cpp	21084	log plain
-rw-r--r--	cegis.h	9376	log plain
-rw-r--r--	cegis_unif.cpp	25803	log plain
-rw-r--r--	cegis_unif.h	13726	log plain
-rw-r--r--	enum_stream_substitution.cpp	19690	log plain
-rw-r--r--	enum_stream_substitution.h	11200	log plain
-rw-r--r--	sygus_enumerator.cpp	34350	log plain
-rw-r--r--	sygus_enumerator.h	19093	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	8846	log plain
-rw-r--r--	sygus_grammar_cons.cpp	39659	log plain
-rw-r--r--	sygus_grammar_cons.h	7181	log plain
-rw-r--r--	sygus_grammar_norm.cpp	23780	log plain
-rw-r--r--	sygus_grammar_norm.h	16745	log plain
-rw-r--r--	sygus_grammar_red.cpp	4387	log plain
-rw-r--r--	sygus_grammar_red.h	4099	log plain
-rw-r--r--	sygus_invariance.cpp	8329	log plain
-rw-r--r--	sygus_invariance.h	9470	log plain
-rw-r--r--	sygus_module.cpp	900	log plain
-rw-r--r--	sygus_module.h	6197	log plain
-rw-r--r--	sygus_pbe.cpp	17165	log plain
-rw-r--r--	sygus_pbe.h	12833	log plain
-rw-r--r--	sygus_process_conj.cpp	24841	log plain
-rw-r--r--	sygus_process_conj.h	12783	log plain
-rw-r--r--	sygus_repair_const.cpp	21036	log plain
-rw-r--r--	sygus_repair_const.h	9302	log plain
-rw-r--r--	sygus_unif.cpp	3568	log plain
-rw-r--r--	sygus_unif.h	7995	log plain
-rw-r--r--	sygus_unif_io.cpp	53826	log plain
-rw-r--r--	sygus_unif_io.h	18636	log plain
-rw-r--r--	sygus_unif_rl.cpp	40220	log plain
-rw-r--r--	sygus_unif_rl.h	17994	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	41958	log plain
-rw-r--r--	synth_conjecture.h	15903	log plain
-rw-r--r--	synth_engine.cpp	14770	log plain
-rw-r--r--	synth_engine.h	4189	log plain
-rw-r--r--	term_database_sygus.cpp	53446	log plain
-rw-r--r--	term_database_sygus.h	25943	log plain