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	10298	log plain
-rw-r--r--	candidate_generator.h	7690	log plain
-rw-r--r--	ho_trigger.cpp	18682	log plain
-rw-r--r--	ho_trigger.h	10396	log plain
-rw-r--r--	inst_match_generator.cpp	21758	log plain
-rw-r--r--	inst_match_generator.h	17325	log plain
-rw-r--r--	inst_match_generator_multi.cpp	11392	log plain
-rw-r--r--	inst_match_generator_multi.h	4536	log plain
-rw-r--r--	inst_match_generator_multi_linear.cpp	5318	log plain
-rw-r--r--	inst_match_generator_multi_linear.h	3358	log plain
-rw-r--r--	inst_match_generator_simple.cpp	6471	log plain
-rw-r--r--	inst_match_generator_simple.h	4086	log plain
-rw-r--r--	inst_strategy.cpp	1580	log plain
-rw-r--r--	inst_strategy.h	2484	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	22145	log plain
-rw-r--r--	inst_strategy_e_matching.h	3795	log plain
-rw-r--r--	inst_strategy_e_matching_user.cpp	5778	log plain
-rw-r--r--	inst_strategy_e_matching_user.h	2294	log plain
-rw-r--r--	instantiation_engine.cpp	8331	log plain
-rw-r--r--	instantiation_engine.h	2827	log plain
-rw-r--r--	pattern_term_selector.cpp	20564	log plain
-rw-r--r--	pattern_term_selector.h	7883	log plain
-rw-r--r--	trigger.cpp	11664	log plain
-rw-r--r--	trigger.h	11473	log plain
-rw-r--r--	trigger_term_info.cpp	2902	log plain
-rw-r--r--	trigger_term_info.h	4682	log plain
-rw-r--r--	trigger_trie.cpp	1904	log plain
-rw-r--r--	trigger_trie.h	1846	log plain
-rw-r--r--	var_match_generator.cpp	2528	log plain
-rw-r--r--	var_match_generator.h	1941	log plain