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	2867	log plain
-rw-r--r--	Makefile.subdirs	502	log plain
d---------	arith	1977	log plain
d---------	arrays	746	log plain
d---------	booleans	688	log plain
d---------	builtin	441	log plain
d---------	bv	1607	log plain
d---------	datatypes	387	log plain
d---------	example	237	log plain
-rw-r--r--	interrupted.h	1581	log plain
-rw-r--r--	ite_simplifier.cpp	13281	log plain
-rw-r--r--	ite_simplifier.h	4805	log plain
-rw-r--r--	logic_info.cpp	9612	log plain
-rw-r--r--	logic_info.h	12011	log plain
-rw-r--r--	logic_info.i	533	log plain
-rwxr-xr-x	mkrewriter	6129	log plain
-rwxr-xr-x	mktheorytraits	10191	log plain
-rw-r--r--	model.cpp	29987	log plain
-rw-r--r--	model.h	8037	log plain
-rw-r--r--	options	430	log plain
-rw-r--r--	options_handlers.h	1629	log plain
-rw-r--r--	output_channel.h	7787	log plain
d---------	quantifiers	1980	log plain
-rw-r--r--	quantifiers_engine.cpp	26992	log plain
-rw-r--r--	quantifiers_engine.h	11131	log plain
-rw-r--r--	rep_set.cpp	6522	log plain
-rw-r--r--	rep_set.h	3598	log plain
-rw-r--r--	rewriter.cpp	8742	log plain
-rw-r--r--	rewriter.h	3269	log plain
-rw-r--r--	rewriter_attributes.h	2596	log plain
-rw-r--r--	rewriter_tables_template.h	2007	log plain
d---------	rewriterules	1015	log plain
-rw-r--r--	shared_terms_database.cpp	8988	log plain
-rw-r--r--	shared_terms_database.h	7687	log plain
-rw-r--r--	substitutions.cpp	11714	log plain
-rw-r--r--	substitutions.h	6028	log plain
-rw-r--r--	term_registration_visitor.cpp	11202	log plain
-rw-r--r--	term_registration_visitor.h	4150	log plain
-rw-r--r--	theory.cpp	6672	log plain
-rw-r--r--	theory.h	23767	log plain
-rw-r--r--	theory_engine.cpp	49302	log plain
-rw-r--r--	theory_engine.h	24036	log plain
-rw-r--r--	theory_registrar.h	1504	log plain
-rw-r--r--	theory_test_utils.h	3567	log plain
-rw-r--r--	theory_traits_template.h	1097	log plain
-rw-r--r--	theoryof_mode.h	1075	log plain
-rw-r--r--	type_enumerator.h	3822	log plain
-rw-r--r--	type_enumerator_template.cpp	1458	log plain
d---------	uf	804	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24312	log plain
-rw-r--r--	unconstrained_simplifier.h	1856	log plain
-rw-r--r--	valuation.cpp	3154	log plain
-rw-r--r--	valuation.h	4240	log plain