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	19111	log plain
-rw-r--r--	ce_guided_single_inv.h	6810	log plain
-rw-r--r--	cegis.cpp	24451	log plain
-rw-r--r--	cegis.h	10130	log plain
-rw-r--r--	cegis_core_connective.cpp	28825	log plain
-rw-r--r--	cegis_core_connective.h	15344	log plain
-rw-r--r--	cegis_unif.cpp	26213	log plain
-rw-r--r--	cegis_unif.h	14446	log plain
-rw-r--r--	enum_stream_substitution.cpp	19309	log plain
-rw-r--r--	enum_stream_substitution.h	11178	log plain
-rw-r--r--	example_eval_cache.cpp	3753	log plain
-rw-r--r--	example_eval_cache.h	6812	log plain
-rw-r--r--	example_infer.cpp	7557	log plain
-rw-r--r--	example_infer.h	6283	log plain
-rw-r--r--	example_min_eval.cpp	2594	log plain
-rw-r--r--	example_min_eval.h	3663	log plain
-rw-r--r--	rcons_obligation_info.cpp	3190	log plain
-rw-r--r--	rcons_obligation_info.h	5660	log plain
-rw-r--r--	rcons_type_info.cpp	2260	log plain
-rw-r--r--	rcons_type_info.h	3407	log plain
-rw-r--r--	sygus_abduct.cpp	7633	log plain
-rw-r--r--	sygus_abduct.h	3483	log plain
-rw-r--r--	sygus_enumerator.cpp	39877	log plain
-rw-r--r--	sygus_enumerator.h	21229	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1511	log plain
-rw-r--r--	sygus_enumerator_basic.h	2186	log plain
-rw-r--r--	sygus_eval_unfold.cpp	11283	log plain
-rw-r--r--	sygus_eval_unfold.h	6658	log plain
-rw-r--r--	sygus_explain.cpp	10854	log plain
-rw-r--r--	sygus_explain.h	8840	log plain
-rw-r--r--	sygus_grammar_cons.cpp	62041	log plain
-rw-r--r--	sygus_grammar_cons.h	10286	log plain
-rw-r--r--	sygus_grammar_norm.cpp	19638	log plain
-rw-r--r--	sygus_grammar_norm.h	15508	log plain
-rw-r--r--	sygus_grammar_red.cpp	5803	log plain
-rw-r--r--	sygus_grammar_red.h	4110	log plain
-rw-r--r--	sygus_interpol.cpp	13295	log plain
-rw-r--r--	sygus_interpol.h	8310	log plain
-rw-r--r--	sygus_invariance.cpp	8502	log plain
-rw-r--r--	sygus_invariance.h	9451	log plain
-rw-r--r--	sygus_module.cpp	947	log plain
-rw-r--r--	sygus_module.h	6605	log plain
-rw-r--r--	sygus_pbe.cpp	9397	log plain
-rw-r--r--	sygus_pbe.h	7280	log plain
-rw-r--r--	sygus_process_conj.cpp	24720	log plain
-rw-r--r--	sygus_process_conj.h	12716	log plain
-rw-r--r--	sygus_qe_preproc.cpp	5165	log plain
-rw-r--r--	sygus_qe_preproc.h	1584	log plain
-rw-r--r--	sygus_reconstruct.cpp	18041	log plain
-rw-r--r--	sygus_reconstruct.h	11954	log plain
-rw-r--r--	sygus_repair_const.cpp	20066	log plain
-rw-r--r--	sygus_repair_const.h	9022	log plain
-rw-r--r--	sygus_stats.cpp	1837	log plain
-rw-r--r--	sygus_stats.h	1783	log plain
-rw-r--r--	sygus_unif.cpp	3444	log plain
-rw-r--r--	sygus_unif.h	7896	log plain
-rw-r--r--	sygus_unif_io.cpp	54897	log plain
-rw-r--r--	sygus_unif_io.h	17746	log plain
-rw-r--r--	sygus_unif_rl.cpp	43728	log plain
-rw-r--r--	sygus_unif_rl.h	18450	log plain
-rw-r--r--	sygus_unif_strat.cpp	35049	log plain
-rw-r--r--	sygus_unif_strat.h	15127	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	44746	log plain
-rw-r--r--	synth_conjecture.h	18053	log plain
-rw-r--r--	synth_engine.cpp	8450	log plain
-rw-r--r--	synth_engine.h	4552	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	32889	log plain
-rw-r--r--	term_database_sygus.h	20251	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	14043	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