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--	CMakeLists.txt	342	log plain
d---------	arith	2939	log plain
d---------	arrays	746	log plain
-rw-r--r--	assertion.cpp	776	log plain
-rw-r--r--	assertion.h	1506	log plain
-rw-r--r--	atom_requests.cpp	2582	log plain
-rw-r--r--	atom_requests.h	3151	log plain
d---------	booleans	456	log plain
d---------	builtin	420	log plain
d---------	bv	1764	log plain
-rw-r--r--	care_graph.h	1577	log plain
d---------	datatypes	602	log plain
-rw-r--r--	decision_manager.cpp	2376	log plain
-rw-r--r--	decision_manager.h	4477	log plain
-rw-r--r--	decision_strategy.cpp	3900	log plain
-rw-r--r--	decision_strategy.h	4911	log plain
-rw-r--r--	evaluator.cpp	16131	log plain
-rw-r--r--	evaluator.h	3263	log plain
d---------	example	204	log plain
-rw-r--r--	ext_theory.cpp	15127	log plain
-rw-r--r--	ext_theory.h	9672	log plain
d---------	fp	434	log plain
d---------	idl	419	log plain
-rw-r--r--	interrupted.h	1612	log plain
-rw-r--r--	logic_info.cpp	20190	log plain
-rw-r--r--	logic_info.h	8876	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	6992	log plain
d---------	quantifiers	3770	log plain
-rw-r--r--	quantifiers_engine.cpp	46919	log plain
-rw-r--r--	quantifiers_engine.h	16247	log plain
-rw-r--r--	rep_set.cpp	11830	log plain
-rw-r--r--	rep_set.h	11053	log plain
-rw-r--r--	rewriter.cpp	9547	log plain
-rw-r--r--	rewriter.h	3447	log plain
-rw-r--r--	rewriter_attributes.h	2609	log plain
-rw-r--r--	rewriter_tables_template.h	2610	log plain
d---------	sep	308	log plain
d---------	sets	683	log plain
-rw-r--r--	shared_terms_database.cpp	9110	log plain
-rw-r--r--	shared_terms_database.h	7780	log plain
-rw-r--r--	sort_inference.cpp	31067	log plain
-rw-r--r--	sort_inference.h	5918	log plain
d---------	strings	749	log plain
-rw-r--r--	subs_minimize.cpp	9609	log plain
-rw-r--r--	subs_minimize.h	1811	log plain
-rw-r--r--	substitutions.cpp	8887	log plain
-rw-r--r--	substitutions.h	5559	log plain
-rw-r--r--	term_registration_visitor.cpp	12376	log plain
-rw-r--r--	term_registration_visitor.h	4063	log plain
-rw-r--r--	theory.cpp	11659	log plain
-rw-r--r--	theory.h	29181	log plain
-rw-r--r--	theory_engine.cpp	81991	log plain
-rw-r--r--	theory_engine.h	27270	log plain
-rw-r--r--	theory_model.cpp	21793	log plain
-rw-r--r--	theory_model.h	15441	log plain
-rw-r--r--	theory_model_builder.cpp	37527	log plain
-rw-r--r--	theory_model_builder.h	9434	log plain
-rw-r--r--	theory_registrar.h	1493	log plain
-rw-r--r--	theory_test_utils.h	3552	log plain
-rw-r--r--	theory_traits_template.h	1388	log plain
-rw-r--r--	type_enumerator.h	5440	log plain
-rw-r--r--	type_enumerator_template.cpp	1515	log plain
-rw-r--r--	type_set.cpp	3033	log plain
-rw-r--r--	type_set.h	2795	log plain
d---------	uf	690	log plain
-rw-r--r--	valuation.cpp	3736	log plain
-rw-r--r--	valuation.h	4772	log plain