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--	.gitignore	18	log plain
-rw-r--r--	Makefile	70	log plain
-rw-r--r--	Makefile.am	3615	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	1642	log plain
d---------	arrays	825	log plain
d---------	booleans	489	log plain
d---------	builtin	406	log plain
d---------	bv	1286	log plain
-rw-r--r--	candidate_generator.cpp	7627	log plain
-rw-r--r--	candidate_generator.h	4886	log plain
d---------	datatypes	472	log plain
d---------	example	237	log plain
-rw-r--r--	inst_match.cpp	34604	log plain
-rw-r--r--	inst_match.h	15665	log plain
-rw-r--r--	instantiator_default.cpp	1966	log plain
-rw-r--r--	instantiator_default.h	1495	log plain
-rw-r--r--	instantiator_tables_template.cpp	1155	log plain
-rw-r--r--	interrupted.h	1634	log plain
-rw-r--r--	ite_simplifier.cpp	13236	log plain
-rw-r--r--	ite_simplifier.h	4783	log plain
-rw-r--r--	logic_info.cpp	8602	log plain
-rw-r--r--	logic_info.h	7895	log plain
-rwxr-xr-x	mkinstantiator	5592	log plain
-rwxr-xr-x	mkrewriter	6102	log plain
-rwxr-xr-x	mktheorytraits	10197	log plain
-rw-r--r--	model.cpp	20445	log plain
-rw-r--r--	model.h	6355	log plain
-rw-r--r--	output_channel.h	8070	log plain
d---------	quantifiers	1137	log plain
-rw-r--r--	quantifiers_engine.cpp	29992	log plain
-rw-r--r--	quantifiers_engine.h	12550	log plain
-rw-r--r--	rewriter.cpp	8081	log plain
-rw-r--r--	rewriter.h	3214	log plain
-rw-r--r--	rewriter_attributes.h	2610	log plain
-rw-r--r--	rewriter_tables_template.h	2021	log plain
d---------	rewriterules	599	log plain
-rw-r--r--	rr_candidate_generator.cpp	4164	log plain
-rw-r--r--	rr_candidate_generator.h	6114	log plain
-rw-r--r--	rr_inst_match.cpp	50641	log plain
-rw-r--r--	rr_inst_match.h	8716	log plain
-rw-r--r--	rr_inst_match_impl.h	4185	log plain
-rw-r--r--	rr_trigger.cpp	16414	log plain
-rw-r--r--	rr_trigger.h	6419	log plain
-rw-r--r--	shared_terms_database.cpp	8942	log plain
-rw-r--r--	shared_terms_database.h	7610	log plain
-rw-r--r--	substitutions.cpp	10747	log plain
-rw-r--r--	substitutions.h	5275	log plain
-rw-r--r--	term_registration_visitor.cpp	9894	log plain
-rw-r--r--	term_registration_visitor.h	4157	log plain
-rw-r--r--	theory.cpp	8538	log plain
-rw-r--r--	theory.h	25694	log plain
-rw-r--r--	theory_engine.cpp	45488	log plain
-rw-r--r--	theory_engine.h	21740	log plain
-rw-r--r--	theory_registrar.h	1487	log plain
-rw-r--r--	theory_test_utils.h	3437	log plain
-rw-r--r--	theory_traits_template.h	1106	log plain
-rw-r--r--	theoryof_mode.h	1106	log plain
-rw-r--r--	trigger.cpp	17661	log plain
-rw-r--r--	trigger.h	6514	log plain
-rw-r--r--	type_enumerator.h	2703	log plain
-rw-r--r--	type_enumerator_template.cpp	1500	log plain
d---------	uf	917	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24343	log plain
-rw-r--r--	unconstrained_simplifier.h	1870	log plain
-rw-r--r--	valuation.cpp	2842	log plain
-rw-r--r--	valuation.h	3906	log plain