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.subdirs	598	log plain
d---------	arith	3220	log plain
d---------	arrays	625	log plain
-rw-r--r--	atom_requests.cpp	2534	log plain
-rw-r--r--	atom_requests.h	3103	log plain
d---------	booleans	613	log plain
d---------	builtin	366	log plain
d---------	bv	2361	log plain
d---------	datatypes	312	log plain
-rw-r--r--	decision_attributes.h	1062	log plain
d---------	example	162	log plain
d---------	idl	412	log plain
-rw-r--r--	interrupted.h	1560	log plain
-rw-r--r--	ite_utilities.cpp	46886	log plain
-rw-r--r--	ite_utilities.h	10381	log plain
-rw-r--r--	logic_info.cpp	10762	log plain
-rw-r--r--	logic_info.h	12682	log plain
-rw-r--r--	logic_info.i	593	log plain
-rwxr-xr-x	mkrewriter	6846	log plain
-rwxr-xr-x	mktheorytraits	10965	log plain
-rw-r--r--	options	745	log plain
-rw-r--r--	options_handlers.h	2106	log plain
-rw-r--r--	output_channel.h	7949	log plain
d---------	quantifiers	2769	log plain
-rw-r--r--	quantifiers_engine.cpp	38487	log plain
-rw-r--r--	quantifiers_engine.h	12202	log plain
-rw-r--r--	rep_set.cpp	13667	log plain
-rw-r--r--	rep_set.h	3959	log plain
-rw-r--r--	rewriter.cpp	8743	log plain
-rw-r--r--	rewriter.h	3312	log plain
-rw-r--r--	rewriter_attributes.h	2575	log plain
-rw-r--r--	rewriter_tables_template.h	2557	log plain
d---------	sets	669	log plain
-rw-r--r--	shared_terms_database.cpp	8896	log plain
-rw-r--r--	shared_terms_database.h	7534	log plain
d---------	strings	572	log plain
-rw-r--r--	substitutions.cpp	8777	log plain
-rw-r--r--	substitutions.h	5480	log plain
-rw-r--r--	term_registration_visitor.cpp	10808	log plain
-rw-r--r--	term_registration_visitor.h	3999	log plain
-rw-r--r--	theory.cpp	8597	log plain
-rw-r--r--	theory.h	27581	log plain
-rw-r--r--	theory_engine.cpp	60543	log plain
-rw-r--r--	theory_engine.h	26220	log plain
-rw-r--r--	theory_model.cpp	30968	log plain
-rw-r--r--	theory_model.h	8206	log plain
-rw-r--r--	theory_registrar.h	1442	log plain
-rw-r--r--	theory_test_utils.h	3665	log plain
-rw-r--r--	theory_traits_template.h	1322	log plain
-rw-r--r--	theoryof_mode.h	1413	log plain
-rw-r--r--	type_enumerator.h	4591	log plain
-rw-r--r--	type_enumerator_template.cpp	1437	log plain
d---------	uf	729	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24376	log plain
-rw-r--r--	unconstrained_simplifier.h	1865	log plain
-rw-r--r--	valuation.cpp	3265	log plain
-rw-r--r--	valuation.h	4536	log plain