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	23495	log plain
-rw-r--r--	ce_guided_single_inv.h	6992	log plain
-rw-r--r--	ce_guided_single_inv_sol.cpp	37895	log plain
-rw-r--r--	ce_guided_single_inv_sol.h	7401	log plain
-rw-r--r--	cegis.cpp	22387	log plain
-rw-r--r--	cegis.h	9776	log plain
-rw-r--r--	cegis_unif.cpp	26114	log plain
-rw-r--r--	cegis_unif.h	13758	log plain
-rw-r--r--	enum_stream_substitution.cpp	19742	log plain
-rw-r--r--	enum_stream_substitution.h	11157	log plain
-rw-r--r--	sygus_abduct.cpp	12825	log plain
-rw-r--r--	sygus_abduct.h	3463	log plain
-rw-r--r--	sygus_enumerator.cpp	34350	log plain
-rw-r--r--	sygus_enumerator.h	19087	log plain
-rw-r--r--	sygus_enumerator_basic.cpp	1520	log plain
-rw-r--r--	sygus_enumerator_basic.h	2179	log plain
-rw-r--r--	sygus_eval_unfold.cpp	7005	log plain
-rw-r--r--	sygus_eval_unfold.h	4467	log plain
-rw-r--r--	sygus_explain.cpp	10505	log plain
-rw-r--r--	sygus_explain.h	8840	log plain
-rw-r--r--	sygus_grammar_cons.cpp	44611	log plain
-rw-r--r--	sygus_grammar_cons.h	8806	log plain
-rw-r--r--	sygus_grammar_norm.cpp	23934	log plain
-rw-r--r--	sygus_grammar_norm.h	16660	log plain
-rw-r--r--	sygus_grammar_red.cpp	4372	log plain
-rw-r--r--	sygus_grammar_red.h	4170	log plain
-rw-r--r--	sygus_invariance.cpp	8329	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	6534	log plain
-rw-r--r--	sygus_pbe.cpp	17202	log plain
-rw-r--r--	sygus_pbe.h	12858	log plain
-rw-r--r--	sygus_process_conj.cpp	24841	log plain
-rw-r--r--	sygus_process_conj.h	12767	log plain
-rw-r--r--	sygus_repair_const.cpp	21740	log plain
-rw-r--r--	sygus_repair_const.h	10057	log plain
-rw-r--r--	sygus_unif.cpp	3607	log plain
-rw-r--r--	sygus_unif.h	7997	log plain
-rw-r--r--	sygus_unif_io.cpp	53826	log plain
-rw-r--r--	sygus_unif_io.h	18630	log plain
-rw-r--r--	sygus_unif_rl.cpp	40220	log plain
-rw-r--r--	sygus_unif_rl.h	17949	log plain
-rw-r--r--	sygus_unif_strat.cpp	35478	log plain
-rw-r--r--	sygus_unif_strat.h	15152	log plain
-rw-r--r--	synth_conjecture.cpp	41986	log plain
-rw-r--r--	synth_conjecture.h	16639	log plain
-rw-r--r--	synth_engine.cpp	13925	log plain
-rw-r--r--	synth_engine.h	4169	log plain
-rw-r--r--	term_database_sygus.cpp	37354	log plain
-rw-r--r--	term_database_sygus.h	20317	log plain
-rw-r--r--	transition_inference.cpp	16531	log plain
-rw-r--r--	transition_inference.h	12937	log plain
-rw-r--r--	type_info.cpp	12775	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