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	10235	log plain
-rw-r--r--	candidate_generator.h	7690	log plain
-rw-r--r--	ho_trigger.cpp	18517	log plain
-rw-r--r--	ho_trigger.h	10281	log plain
-rw-r--r--	inst_match_generator.cpp	21230	log plain
-rw-r--r--	inst_match_generator.h	16620	log plain
-rw-r--r--	inst_match_generator_multi.cpp	11324	log plain
-rw-r--r--	inst_match_generator_multi.h	4354	log plain
-rw-r--r--	inst_match_generator_multi_linear.cpp	5093	log plain
-rw-r--r--	inst_match_generator_multi_linear.h	3267	log plain
-rw-r--r--	inst_match_generator_simple.cpp	6224	log plain
-rw-r--r--	inst_match_generator_simple.h	3921	log plain
-rw-r--r--	inst_strategy.cpp	1499	log plain
-rw-r--r--	inst_strategy.h	2352	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	21808	log plain
-rw-r--r--	inst_strategy_e_matching.h	3738	log plain
-rw-r--r--	inst_strategy_e_matching_user.cpp	5190	log plain
-rw-r--r--	inst_strategy_e_matching_user.h	2249	log plain
-rw-r--r--	instantiation_engine.cpp	8376	log plain
-rw-r--r--	instantiation_engine.h	2825	log plain
-rw-r--r--	pattern_term_selector.cpp	20535	log plain
-rw-r--r--	pattern_term_selector.h	7898	log plain
-rw-r--r--	trigger.cpp	11066	log plain
-rw-r--r--	trigger.h	10913	log plain
-rw-r--r--	trigger_term_info.cpp	2907	log plain
-rw-r--r--	trigger_term_info.h	4699	log plain
-rw-r--r--	trigger_trie.cpp	1911	log plain
-rw-r--r--	trigger_trie.h	1868	log plain
-rw-r--r--	var_match_generator.cpp	2351	log plain
-rw-r--r--	var_match_generator.h	1800	log plain