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--	bounded_integers.cpp	15755	log plain
-rw-r--r--	bounded_integers.h	4463	log plain
-rw-r--r--	candidate_generator.cpp	7163	log plain
-rw-r--r--	candidate_generator.h	4365	log plain
-rw-r--r--	first_order_model.cpp	28812	log plain
-rw-r--r--	first_order_model.h	7831	log plain
-rw-r--r--	first_order_reasoning.cpp	5711	log plain
-rw-r--r--	first_order_reasoning.h	1222	log plain
-rw-r--r--	full_model_check.cpp	54424	log plain
-rw-r--r--	full_model_check.h	6037	log plain
-rw-r--r--	inst_gen.cpp	12486	log plain
-rw-r--r--	inst_gen.h	2089	log plain
-rw-r--r--	inst_match.cpp	7678	log plain
-rw-r--r--	inst_match.h	6761	log plain
-rw-r--r--	inst_match_generator.cpp	27861	log plain
-rw-r--r--	inst_match_generator.h	7876	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	13648	log plain
-rw-r--r--	inst_strategy_cbqi.h	3443	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	18006	log plain
-rw-r--r--	inst_strategy_e_matching.h	4608	log plain
-rw-r--r--	instantiation_engine.cpp	18279	log plain
-rw-r--r--	instantiation_engine.h	5138	log plain
-rw-r--r--	kinds	2527	log plain
-rw-r--r--	macros.cpp	14050	log plain
-rw-r--r--	macros.h	2032	log plain
-rw-r--r--	model_builder.cpp	47177	log plain
-rw-r--r--	model_builder.h	9851	log plain
-rw-r--r--	model_engine.cpp	13037	log plain
-rw-r--r--	model_engine.h	2103	log plain
-rw-r--r--	modes.cpp	2745	log plain
-rw-r--r--	modes.h	3448	log plain
-rw-r--r--	options	7934	log plain
-rw-r--r--	options_handlers.h	9950	log plain
-rwxr-xr-x	qinterval_builder.cpp	42608	log plain
-rwxr-xr-x	qinterval_builder.h	6181	log plain
-rwxr-xr-x	quant_conflict_find.cpp	85151	log plain
-rwxr-xr-x	quant_conflict_find.h	9381	log plain
-rw-r--r--	quant_util.cpp	7766	log plain
-rw-r--r--	quant_util.h	3760	log plain
-rw-r--r--	quantifiers_attributes.cpp	1493	log plain
-rw-r--r--	quantifiers_attributes.h	1610	log plain
-rw-r--r--	quantifiers_rewriter.cpp	42343	log plain
-rw-r--r--	quantifiers_rewriter.h	3733	log plain
-rw-r--r--	relevant_domain.cpp	8463	log plain
-rw-r--r--	relevant_domain.h	2059	log plain
-rw-r--r--	rewrite_engine.cpp	11804	log plain
-rw-r--r--	rewrite_engine.h	1904	log plain
-rw-r--r--	symmetry_breaking.cpp	12261	log plain
-rw-r--r--	symmetry_breaking.h	3698	log plain
-rw-r--r--	term_database.cpp	20793	log plain
-rw-r--r--	term_database.h	9311	log plain
-rw-r--r--	theory_quantifiers.cpp	6423	log plain
-rw-r--r--	theory_quantifiers.h	2692	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	7845	log plain
-rw-r--r--	trigger.cpp	17320	log plain
-rw-r--r--	trigger.h	5909	log plain