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	2995	log plain
d---------	arrays	704	log plain
-rw-r--r--	assertion.cpp	776	log plain
-rw-r--r--	assertion.h	1506	log plain
-rw-r--r--	atom_requests.cpp	2593	log plain
-rw-r--r--	atom_requests.h	3162	log plain
d---------	booleans	414	log plain
d---------	builtin	378	log plain
d---------	bv	2268	log plain
-rw-r--r--	care_graph.h	1577	log plain
d---------	datatypes	466	log plain
d---------	example	162	log plain
d---------	fp	392	log plain
d---------	idl	377	log plain
-rw-r--r--	interrupted.h	1623	log plain
-rw-r--r--	ite_utilities.cpp	48107	log plain
-rw-r--r--	ite_utilities.h	10665	log plain
-rw-r--r--	logic_info.cpp	18457	log plain
-rw-r--r--	logic_info.h	8631	log plain
-rw-r--r--	logic_info.i	593	log plain
-rwxr-xr-x	mkrewriter	6965	log plain
-rwxr-xr-x	mktheorytraits	11123	log plain
-rw-r--r--	output_channel.h	8280	log plain
d---------	quantifiers	5880	log plain
-rw-r--r--	quantifiers_engine.cpp	44809	log plain
-rw-r--r--	quantifiers_engine.h	16823	log plain
-rw-r--r--	rep_set.cpp	11650	log plain
-rw-r--r--	rep_set.h	10950	log plain
-rw-r--r--	rewriter.cpp	9552	log plain
-rw-r--r--	rewriter.h	3454	log plain
-rw-r--r--	rewriter_attributes.h	2610	log plain
-rw-r--r--	rewriter_tables_template.h	2610	log plain
d---------	sep	266	log plain
d---------	sets	641	log plain
-rw-r--r--	shared_terms_database.cpp	9115	log plain
-rw-r--r--	shared_terms_database.h	7583	log plain
-rw-r--r--	sort_inference.cpp	31510	log plain
-rw-r--r--	sort_inference.h	4175	log plain
d---------	strings	537	log plain
-rw-r--r--	substitutions.cpp	8825	log plain
-rw-r--r--	substitutions.h	5560	log plain
-rw-r--r--	term_registration_visitor.cpp	12232	log plain
-rw-r--r--	term_registration_visitor.h	4064	log plain
-rw-r--r--	theory.cpp	24388	log plain
-rw-r--r--	theory.h	32721	log plain
-rw-r--r--	theory_engine.cpp	85552	log plain
-rw-r--r--	theory_engine.h	27772	log plain
-rw-r--r--	theory_model.cpp	22164	log plain
-rw-r--r--	theory_model.h	11219	log plain
-rw-r--r--	theory_model_builder.cpp	36613	log plain
-rw-r--r--	theory_model_builder.h	9189	log plain
-rw-r--r--	theory_registrar.h	1485	log plain
-rw-r--r--	theory_test_utils.h	3600	log plain
-rw-r--r--	theory_traits_template.h	1389	log plain
-rw-r--r--	type_enumerator.h	5423	log plain
-rw-r--r--	type_enumerator_template.cpp	1510	log plain
-rw-r--r--	type_set.cpp	3063	log plain
-rw-r--r--	type_set.h	2825	log plain
d---------	uf	648	log plain
-rw-r--r--	unconstrained_simplifier.cpp	24447	log plain
-rw-r--r--	unconstrained_simplifier.h	1989	log plain
-rw-r--r--	valuation.cpp	3093	log plain
-rw-r--r--	valuation.h	4709	log plain