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	879	log plain
-rw-r--r--	first_order_model.cpp	6033	log plain
-rw-r--r--	first_order_model.h	2735	log plain
-rw-r--r--	inst_when_mode.cpp	1317	log plain
-rw-r--r--	inst_when_mode.h	1539	log plain
-rw-r--r--	instantiation_engine.cpp	15590	log plain
-rw-r--r--	instantiation_engine.h	2401	log plain
-rw-r--r--	kinds	1675	log plain
-rw-r--r--	literal_match_mode.cpp	1252	log plain
-rw-r--r--	literal_match_mode.h	1436	log plain
-rw-r--r--	model_builder.cpp	16581	log plain
-rw-r--r--	model_builder.h	2742	log plain
-rw-r--r--	model_engine.cpp	14561	log plain
-rw-r--r--	model_engine.h	2432	log plain
-rw-r--r--	options	4513	log plain
-rw-r--r--	options_handlers.h	3850	log plain
-rw-r--r--	quantifiers_rewriter.cpp	24916	log plain
-rw-r--r--	quantifiers_rewriter.h	3144	log plain
-rw-r--r--	relevant_domain.cpp	6414	log plain
-rw-r--r--	relevant_domain.h	1565	log plain
-rw-r--r--	rep_set_iterator.cpp	18017	log plain
-rw-r--r--	rep_set_iterator.h	3727	log plain
-rw-r--r--	term_database.cpp	13030	log plain
-rw-r--r--	term_database.h	5936	log plain
-rw-r--r--	theory_quantifiers.cpp	5657	log plain
-rw-r--r--	theory_quantifiers.h	2326	log plain
-rw-r--r--	theory_quantifiers_instantiator.cpp	2828	log plain
-rw-r--r--	theory_quantifiers_instantiator.h	1641	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	4431	log plain