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	3341	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	2049	log plain
d---------	arrays	860	log plain
d---------	booleans	524	log plain
d---------	builtin	441	log plain
d---------	bv	1321	log plain
d---------	datatypes	507	log plain
d---------	example	237	log plain
-rw-r--r--	instantiator_tables_template.cpp	1146	log plain
-rw-r--r--	interrupted.h	1634	log plain
-rw-r--r--	ite_simplifier.cpp	13304	log plain
-rw-r--r--	ite_simplifier.h	4819	log plain
-rw-r--r--	logic_info.cpp	9194	log plain
-rw-r--r--	logic_info.h	12008	log plain
-rwxr-xr-x	mkinstantiator	5709	log plain
-rwxr-xr-x	mkrewriter	6219	log plain
-rwxr-xr-x	mktheorytraits	10491	log plain
-rw-r--r--	model.cpp	23306	log plain
-rw-r--r--	model.h	7929	log plain
-rw-r--r--	options	558	log plain
-rw-r--r--	options_handlers.h	1688	log plain
-rw-r--r--	output_channel.h	7476	log plain
d---------	quantifiers	1662	log plain
-rw-r--r--	quantifiers_engine.cpp	30138	log plain
-rw-r--r--	quantifiers_engine.h	12876	log plain
-rw-r--r--	rep_set.cpp	6624	log plain
-rw-r--r--	rep_set.h	3544	log plain
-rw-r--r--	rewriter.cpp	8272	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	2012	log plain
d---------	rewriterules	958	log plain
-rw-r--r--	shared_terms_database.cpp	9059	log plain
-rw-r--r--	shared_terms_database.h	7728	log plain
-rw-r--r--	substitutions.cpp	11360	log plain
-rw-r--r--	substitutions.h	5275	log plain
-rw-r--r--	term_registration_visitor.cpp	11752	log plain
-rw-r--r--	term_registration_visitor.h	4157	log plain
-rw-r--r--	theory.cpp	8423	log plain
-rw-r--r--	theory.h	26155	log plain
-rw-r--r--	theory_engine.cpp	47195	log plain
-rw-r--r--	theory_engine.h	21066	log plain
-rw-r--r--	theory_registrar.h	1487	log plain
-rw-r--r--	theory_test_utils.h	3511	log plain
-rw-r--r--	theory_traits_template.h	1102	log plain
-rw-r--r--	theoryof_mode.h	1106	log plain
-rw-r--r--	type_enumerator.h	3105	log plain
-rw-r--r--	type_enumerator_template.cpp	1495	log plain
d---------	uf	998	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24335	log plain
-rw-r--r--	unconstrained_simplifier.h	1870	log plain
-rw-r--r--	valuation.cpp	2949	log plain
-rw-r--r--	valuation.h	4005	log plain