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
d---------	arith	2813	log plain
d---------	arrays	590	log plain
-rw-r--r--	atom_requests.cpp	2534	log plain
-rw-r--r--	atom_requests.h	3103	log plain
d---------	booleans	414	log plain
d---------	builtin	331	log plain
d---------	bv	2192	log plain
d---------	datatypes	416	log plain
d---------	example	162	log plain
d---------	fp	261	log plain
d---------	idl	377	log plain
-rw-r--r--	interrupted.h	1560	log plain
-rw-r--r--	ite_utilities.cpp	47026	log plain
-rw-r--r--	ite_utilities.h	10382	log plain
-rw-r--r--	logic_info.cpp	16706	log plain
-rw-r--r--	logic_info.h	8127	log plain
-rw-r--r--	logic_info.i	593	log plain
-rwxr-xr-x	mkrewriter	6846	log plain
-rwxr-xr-x	mktheorytraits	10976	log plain
-rw-r--r--	output_channel.h	9150	log plain
d---------	quantifiers	3336	log plain
-rw-r--r--	quantifiers_engine.cpp	56125	log plain
-rw-r--r--	quantifiers_engine.h	15488	log plain
-rw-r--r--	rep_set.cpp	15795	log plain
-rw-r--r--	rep_set.h	4265	log plain
-rw-r--r--	rewriter.cpp	9522	log plain
-rw-r--r--	rewriter.h	3432	log plain
-rw-r--r--	rewriter_attributes.h	2575	log plain
-rw-r--r--	rewriter_tables_template.h	2562	log plain
d---------	sets	629	log plain
-rw-r--r--	shared_terms_database.cpp	8953	log plain
-rw-r--r--	shared_terms_database.h	7534	log plain
-rw-r--r--	sort_inference.cpp	30180	log plain
-rw-r--r--	sort_inference.h	3898	log plain
d---------	strings	537	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	12868	log plain
-rw-r--r--	term_registration_visitor.h	3999	log plain
-rw-r--r--	theory.cpp	9786	log plain
-rw-r--r--	theory.h	27732	log plain
-rw-r--r--	theory_engine.cpp	64996	log plain
-rw-r--r--	theory_engine.h	27146	log plain
-rw-r--r--	theory_model.cpp	39085	log plain
-rw-r--r--	theory_model.h	8720	log plain
-rw-r--r--	theory_registrar.h	1442	log plain
-rw-r--r--	theory_test_utils.h	4076	log plain
-rw-r--r--	theory_traits_template.h	1330	log plain
-rw-r--r--	type_enumerator.h	5241	log plain
-rw-r--r--	type_enumerator_template.cpp	1480	log plain
d---------	uf	648	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24720	log plain
-rw-r--r--	unconstrained_simplifier.h	1865	log plain
-rw-r--r--	valuation.cpp	2993	log plain
-rw-r--r--	valuation.h	4588	log plain