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--	Makefile	85	log plain
-rw-r--r--	Makefile.am	991	log plain
-rw-r--r--	candidate_generator.cpp	7628	log plain
-rw-r--r--	candidate_generator.h	4946	log plain
-rw-r--r--	first_order_model.cpp	17488	log plain
-rw-r--r--	first_order_model.h	3952	log plain
-rw-r--r--	inst_match.cpp	34499	log plain
-rw-r--r--	inst_match.h	15740	log plain
-rw-r--r--	instantiation_engine.cpp	16108	log plain
-rw-r--r--	instantiation_engine.h	2654	log plain
-rw-r--r--	instantiator_default.cpp	1978	log plain
-rw-r--r--	instantiator_default.h	1558	log plain
-rw-r--r--	kinds	1949	log plain
-rw-r--r--	model_builder.cpp	20730	log plain
-rw-r--r--	model_builder.h	3921	log plain
-rw-r--r--	model_engine.cpp	17119	log plain
-rw-r--r--	model_engine.h	2763	log plain
-rw-r--r--	modes.cpp	2262	log plain
-rw-r--r--	modes.h	2170	log plain
-rw-r--r--	options	4761	log plain
-rw-r--r--	options_handlers.h	4975	log plain
-rw-r--r--	quantifiers_attributes.cpp	1447	log plain
-rw-r--r--	quantifiers_attributes.h	1559	log plain
-rw-r--r--	quantifiers_rewriter.cpp	24927	log plain
-rw-r--r--	quantifiers_rewriter.h	3144	log plain
-rw-r--r--	relevant_domain.cpp	7303	log plain
-rw-r--r--	relevant_domain.h	1875	log plain
-rw-r--r--	term_database.cpp	13134	log plain
-rw-r--r--	term_database.h	6094	log plain
-rw-r--r--	theory_quantifiers.cpp	5942	log plain
-rw-r--r--	theory_quantifiers.h	2390	log plain
-rw-r--r--	theory_quantifiers_instantiator.cpp	2828	log plain
-rw-r--r--	theory_quantifiers_instantiator.h	1861	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	4443	log plain
-rw-r--r--	trigger.cpp	17715	log plain
-rw-r--r--	trigger.h	6587	log plain