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	1055	log plain
-rw-r--r--	candidate_generator.cpp	5872	log plain
-rw-r--r--	candidate_generator.h	4327	log plain
-rw-r--r--	first_order_model.cpp	15917	log plain
-rw-r--r--	first_order_model.h	3928	log plain
-rwxr-xr-x	inst_gen.cpp	7690	log plain
-rwxr-xr-x	inst_gen.h	1960	log plain
-rw-r--r--	inst_match.cpp	34698	log plain
-rw-r--r--	inst_match.h	16224	log plain
-rw-r--r--	instantiation_engine.cpp	14118	log plain
-rw-r--r--	instantiation_engine.h	2489	log plain
-rw-r--r--	instantiator_default.cpp	1910	log plain
-rw-r--r--	instantiator_default.h	1483	log plain
-rw-r--r--	kinds	1949	log plain
-rw-r--r--	model_builder.cpp	35755	log plain
-rw-r--r--	model_builder.h	7407	log plain
-rw-r--r--	model_engine.cpp	14764	log plain
-rw-r--r--	model_engine.h	2480	log plain
-rw-r--r--	modes.cpp	2182	log plain
-rw-r--r--	modes.h	2090	log plain
-rw-r--r--	options	4900	log plain
-rw-r--r--	options_handlers.h	4914	log plain
-rwxr-xr-x	quant_util.cpp	4785	log plain
-rwxr-xr-x	quant_util.h	2472	log plain
-rw-r--r--	quantifiers_attributes.cpp	1363	log plain
-rw-r--r--	quantifiers_attributes.h	1468	log plain
-rw-r--r--	quantifiers_rewriter.cpp	24891	log plain
-rw-r--r--	quantifiers_rewriter.h	3066	log plain
-rw-r--r--	relevant_domain.cpp	7224	log plain
-rw-r--r--	relevant_domain.h	1800	log plain
-rw-r--r--	term_database.cpp	17057	log plain
-rw-r--r--	term_database.h	8510	log plain
-rw-r--r--	theory_quantifiers.cpp	5879	log plain
-rw-r--r--	theory_quantifiers.h	2336	log plain
-rw-r--r--	theory_quantifiers_instantiator.cpp	2709	log plain
-rw-r--r--	theory_quantifiers_instantiator.h	1807	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	4368	log plain
-rw-r--r--	trigger.cpp	15561	log plain
-rw-r--r--	trigger.h	5106	log plain