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	11177	log plain
-rw-r--r--	candidate_generator.h	8757	log plain
-rw-r--r--	ho_trigger.cpp	18736	log plain
-rw-r--r--	ho_trigger.h	10412	log plain
-rw-r--r--	im_generator.cpp	1152	log plain
-rw-r--r--	im_generator.h	4125	log plain
-rw-r--r--	inst_match_generator.cpp	20945	log plain
-rw-r--r--	inst_match_generator.h	13265	log plain
-rw-r--r--	inst_match_generator_multi.cpp	10471	log plain
-rw-r--r--	inst_match_generator_multi.h	4066	log plain
-rw-r--r--	inst_match_generator_multi_linear.cpp	5085	log plain
-rw-r--r--	inst_match_generator_multi_linear.h	3169	log plain
-rw-r--r--	inst_match_generator_simple.cpp	6164	log plain
-rw-r--r--	inst_match_generator_simple.h	3532	log plain
-rw-r--r--	inst_strategy.cpp	1746	log plain
-rw-r--r--	inst_strategy.h	2712	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	22208	log plain
-rw-r--r--	inst_strategy_e_matching.h	3885	log plain
-rw-r--r--	inst_strategy_e_matching_user.cpp	5162	log plain
-rw-r--r--	inst_strategy_e_matching_user.h	2381	log plain
-rw-r--r--	instantiation_engine.cpp	8271	log plain
-rw-r--r--	instantiation_engine.h	2973	log plain
-rw-r--r--	pattern_term_selector.cpp	20591	log plain
-rw-r--r--	pattern_term_selector.h	7944	log plain
-rw-r--r--	trigger.cpp	7822	log plain
-rw-r--r--	trigger.h	9211	log plain
-rw-r--r--	trigger_database.cpp	5311	log plain
-rw-r--r--	trigger_database.h	3726	log plain
-rw-r--r--	trigger_term_info.cpp	2965	log plain
-rw-r--r--	trigger_term_info.h	4747	log plain
-rw-r--r--	trigger_trie.cpp	1972	log plain
-rw-r--r--	trigger_trie.h	1915	log plain
-rw-r--r--	var_match_generator.cpp	2435	log plain
-rw-r--r--	var_match_generator.h	1717	log plain