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--	ambqi_builder.cpp	36744	log plain
-rw-r--r--	ambqi_builder.h	4345	log plain
-rw-r--r--	bounded_integers.cpp	17851	log plain
-rw-r--r--	bounded_integers.h	4612	log plain
-rw-r--r--	candidate_generator.cpp	7514	log plain
-rw-r--r--	candidate_generator.h	4485	log plain
-rwxr-xr-x	conjecture_generator.cpp	88162	log plain
-rwxr-xr-x	conjecture_generator.h	16725	log plain
-rw-r--r--	first_order_model.cpp	34655	log plain
-rw-r--r--	first_order_model.h	9697	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	54773	log plain
-rw-r--r--	full_model_check.h	6356	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	8796	log plain
-rw-r--r--	inst_match.h	7165	log plain
-rw-r--r--	inst_match_generator.cpp	29951	log plain
-rw-r--r--	inst_match_generator.h	9497	log plain
-rw-r--r--	inst_strategy_cbqi.cpp	15253	log plain
-rw-r--r--	inst_strategy_cbqi.h	3457	log plain
-rw-r--r--	inst_strategy_e_matching.cpp	19101	log plain
-rw-r--r--	inst_strategy_e_matching.h	4759	log plain
-rw-r--r--	instantiation_engine.cpp	19019	log plain
-rw-r--r--	instantiation_engine.h	5438	log plain
-rw-r--r--	kinds	3133	log plain
-rw-r--r--	macros.cpp	10613	log plain
-rw-r--r--	macros.h	1894	log plain
-rw-r--r--	model_builder.cpp	47184	log plain
-rw-r--r--	model_builder.h	9851	log plain
-rw-r--r--	model_engine.cpp	13854	log plain
-rw-r--r--	model_engine.h	2254	log plain
-rw-r--r--	modes.cpp	2895	log plain
-rw-r--r--	modes.h	3728	log plain
-rw-r--r--	options	10639	log plain
-rw-r--r--	options_handlers.h	11013	log plain
-rw-r--r--	qinterval_builder.cpp	41506	log plain
-rw-r--r--	qinterval_builder.h	6036	log plain
-rwxr-xr-x	quant_conflict_find.cpp	84584	log plain
-rwxr-xr-x	quant_conflict_find.h	8682	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	2200	log plain
-rw-r--r--	quantifiers_attributes.h	1664	log plain
-rw-r--r--	quantifiers_rewriter.cpp	43413	log plain
-rw-r--r--	quantifiers_rewriter.h	3709	log plain
-rw-r--r--	relevant_domain.cpp	8497	log plain
-rw-r--r--	relevant_domain.h	2059	log plain
-rw-r--r--	rewrite_engine.cpp	11966	log plain
-rw-r--r--	rewrite_engine.h	2052	log plain
-rw-r--r--	symmetry_breaking.cpp	12270	log plain
-rw-r--r--	symmetry_breaking.h	3698	log plain
-rw-r--r--	term_database.cpp	33662	log plain
-rw-r--r--	term_database.h	11243	log plain
-rw-r--r--	theory_quantifiers.cpp	6305	log plain
-rw-r--r--	theory_quantifiers.h	2658	log plain
-rw-r--r--	theory_quantifiers_type_rules.h	8209	log plain
-rw-r--r--	trigger.cpp	19084	log plain
-rw-r--r--	trigger.h	6124	log plain