ematching « 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--	candidate_generator.cpp	10924	log plain
-rw-r--r--	candidate_generator.h	7958	log plain
-rw-r--r--	ho_trigger.cpp	18748	log plain
-rw-r--r--	ho_trigger.h	10393	log plain
-rw-r--r--	im_generator.cpp	1147	log plain
-rw-r--r--	im_generator.h	4127	log plain
-rw-r--r--	inst_match_generator.cpp	20740	log plain
-rw-r--r--	inst_match_generator.h	13181	log plain
-rw-r--r--	inst_match_generator_multi.cpp	10469	log plain
-rw-r--r--	inst_match_generator_multi.h	4062	log plain
-rw-r--r--	inst_match_generator_multi_linear.cpp	5076	log plain
-rw-r--r--	inst_match_generator_multi_linear.h	3172	log plain
-rw-r--r--	inst_match_generator_simple.cpp	6165	log plain
-rw-r--r--	inst_match_generator_simple.h	3529	log plain
-rw-r--r--	inst_strategy.cpp	1632	log plain
-rw-r--r--	inst_strategy.h	2625	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	21505	log plain
-rw-r--r--	inst_strategy_e_matching.h	3839	log plain
-rw-r--r--	inst_strategy_e_matching_user.cpp	5000	log plain
-rw-r--r--	inst_strategy_e_matching_user.h	2343	log plain
-rw-r--r--	instantiation_engine.cpp	8264	log plain
-rw-r--r--	instantiation_engine.h	2931	log plain
-rw-r--r--	pattern_term_selector.cpp	20616	log plain
-rw-r--r--	pattern_term_selector.h	7935	log plain
-rw-r--r--	trigger.cpp	7129	log plain
-rw-r--r--	trigger.h	9029	log plain
-rw-r--r--	trigger_database.cpp	5215	log plain
-rw-r--r--	trigger_database.h	3620	log plain
-rw-r--r--	trigger_term_info.cpp	2954	log plain
-rw-r--r--	trigger_term_info.h	4734	log plain
-rw-r--r--	trigger_trie.cpp	1956	log plain
-rw-r--r--	trigger_trie.h	1897	log plain
-rw-r--r--	var_match_generator.cpp	2412	log plain
-rw-r--r--	var_match_generator.h	1709	log plain