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	18926	log plain
-rw-r--r--	ce_guided_single_inv.h	6810	log plain
-rw-r--r--	cegis.cpp	23822	log plain
-rw-r--r--	cegis.h	9656	log plain
-rw-r--r--	cegis_core_connective.cpp	28840	log plain
-rw-r--r--	cegis_core_connective.h	15178	log plain
-rw-r--r--	cegis_unif.cpp	26378	log plain
-rw-r--r--	cegis_unif.h	14219	log plain
-rw-r--r--	enum_stream_substitution.cpp	19297	log plain
-rw-r--r--	enum_stream_substitution.h	11081	log plain
-rw-r--r--	enum_val_generator.h	2161	log plain
-rw-r--r--	enum_value_manager.cpp	8262	log plain
-rw-r--r--	enum_value_manager.h	4779	log plain
-rw-r--r--	example_eval_cache.cpp	3454	log plain
-rw-r--r--	example_eval_cache.h	6911	log plain
-rw-r--r--	example_infer.cpp	7507	log plain
-rw-r--r--	example_infer.h	6250	log plain
-rw-r--r--	example_min_eval.cpp	2576	log plain
-rw-r--r--	example_min_eval.h	3663	log plain
-rw-r--r--	rcons_obligation.cpp	3394	log plain
-rw-r--r--	rcons_obligation.h	5590	log plain
-rw-r--r--	rcons_type_info.cpp	2453	log plain
-rw-r--r--	rcons_type_info.h	3635	log plain
-rw-r--r--	sygus_abduct.cpp	7615	log plain
-rw-r--r--	sygus_abduct.h	3483	log plain
-rw-r--r--	sygus_enumerator.cpp	39008	log plain
-rw-r--r--	sygus_enumerator.h	21920	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1529	log plain
-rw-r--r--	sygus_enumerator_basic.h	2170	log plain
-rw-r--r--	sygus_enumerator_callback.cpp	3302	log plain
-rw-r--r--	sygus_enumerator_callback.h	3665	log plain
-rw-r--r--	sygus_eval_unfold.cpp	11108	log plain
-rw-r--r--	sygus_eval_unfold.h	6484	log plain
-rw-r--r--	sygus_explain.cpp	10916	log plain
-rw-r--r--	sygus_explain.h	8840	log plain
-rw-r--r--	sygus_grammar_cons.cpp	61664	log plain
-rw-r--r--	sygus_grammar_cons.h	9975	log plain
-rw-r--r--	sygus_grammar_norm.cpp	19576	log plain
-rw-r--r--	sygus_grammar_norm.h	15508	log plain
-rw-r--r--	sygus_grammar_red.cpp	5823	log plain
-rw-r--r--	sygus_grammar_red.h	4110	log plain
-rw-r--r--	sygus_interpol.cpp	13020	log plain
-rw-r--r--	sygus_interpol.h	8352	log plain
-rw-r--r--	sygus_invariance.cpp	8310	log plain
-rw-r--r--	sygus_invariance.h	9207	log plain
-rw-r--r--	sygus_module.cpp	1080	log plain
-rw-r--r--	sygus_module.h	6675	log plain
-rw-r--r--	sygus_pbe.cpp	9633	log plain
-rw-r--r--	sygus_pbe.h	7245	log plain
-rw-r--r--	sygus_process_conj.cpp	23786	log plain
-rw-r--r--	sygus_process_conj.h	12286	log plain
-rw-r--r--	sygus_qe_preproc.cpp	5155	log plain
-rw-r--r--	sygus_qe_preproc.h	1649	log plain
-rw-r--r--	sygus_reconstruct.cpp	18006	log plain
-rw-r--r--	sygus_reconstruct.h	11693	log plain
-rw-r--r--	sygus_repair_const.cpp	19864	log plain
-rw-r--r--	sygus_repair_const.h	9082	log plain
-rw-r--r--	sygus_stats.cpp	1516	log plain
-rw-r--r--	sygus_stats.h	1570	log plain
-rw-r--r--	sygus_unif.cpp	3587	log plain
-rw-r--r--	sygus_unif.h	7923	log plain
-rw-r--r--	sygus_unif_io.cpp	54973	log plain
-rw-r--r--	sygus_unif_io.h	17721	log plain
-rw-r--r--	sygus_unif_rl.cpp	43763	log plain
-rw-r--r--	sygus_unif_rl.h	18410	log plain
-rw-r--r--	sygus_unif_strat.cpp	34998	log plain
-rw-r--r--	sygus_unif_strat.h	15193	log plain
-rw-r--r--	sygus_utils.cpp	5580	log plain
-rw-r--r--	sygus_utils.h	4223	log plain
-rw-r--r--	synth_conjecture.cpp	37966	log plain
-rw-r--r--	synth_conjecture.h	15165	log plain
-rw-r--r--	synth_engine.cpp	7931	log plain
-rw-r--r--	synth_engine.h	4462	log plain
-rw-r--r--	synth_verify.cpp	5014	log plain
-rw-r--r--	synth_verify.h	2010	log plain
-rw-r--r--	template_infer.cpp	6466	log plain
-rw-r--r--	template_infer.h	2349	log plain
-rw-r--r--	term_database_sygus.cpp	30922	log plain
-rw-r--r--	term_database_sygus.h	19335	log plain
-rw-r--r--	transition_inference.cpp	16783	log plain
-rw-r--r--	transition_inference.h	13169	log plain
-rw-r--r--	type_info.cpp	14374	log plain
-rw-r--r--	type_info.h	9646	log plain
-rw-r--r--	type_node_id_trie.cpp	1398	log plain
-rw-r--r--	type_node_id_trie.h	1591	log plain