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--	CMakeLists.txt	1173	log plain
d---------	arith	3022	log plain
d---------	arrays	704	log plain
-rw-r--r--	assertion.cpp	776	log plain
-rw-r--r--	assertion.h	1517	log plain
-rw-r--r--	atom_requests.cpp	2567	log plain
-rw-r--r--	atom_requests.h	3136	log plain
d---------	booleans	414	log plain
d---------	builtin	378	log plain
d---------	bv	1722	log plain
-rw-r--r--	care_graph.h	1603	log plain
d---------	datatypes	666	log plain
-rw-r--r--	decision_manager.cpp	3407	log plain
-rw-r--r--	decision_manager.h	5724	log plain
-rw-r--r--	decision_strategy.cpp	3900	log plain
-rw-r--r--	decision_strategy.h	4905	log plain
-rw-r--r--	evaluator.cpp	17389	log plain
-rw-r--r--	evaluator.h	3257	log plain
d---------	example	162	log plain
-rw-r--r--	ext_theory.cpp	15445	log plain
-rw-r--r--	ext_theory.h	9676	log plain
d---------	fp	392	log plain
d---------	idl	377	log plain
-rw-r--r--	interrupted.h	1596	log plain
-rw-r--r--	logic_info.cpp	20917	log plain
-rw-r--r--	logic_info.h	9243	log plain
-rw-r--r--	logic_info.i	593	log plain
-rwxr-xr-x	mkrewriter	6965	log plain
-rwxr-xr-x	mktheorytraits	10653	log plain
-rw-r--r--	output_channel.h	6956	log plain
d---------	quantifiers	4116	log plain
-rw-r--r--	quantifiers_engine.cpp	47799	log plain
-rw-r--r--	quantifiers_engine.h	14773	log plain
-rw-r--r--	rep_set.cpp	11833	log plain
-rw-r--r--	rep_set.h	11398	log plain
-rw-r--r--	rewriter.cpp	9670	log plain
-rw-r--r--	rewriter.h	3441	log plain
-rw-r--r--	rewriter_attributes.h	2609	log plain
-rw-r--r--	rewriter_tables_template.h	2611	log plain
d---------	sep	266	log plain
d---------	sets	975	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	31059	log plain
-rw-r--r--	sort_inference.h	5904	log plain
d---------	strings	1245	log plain
-rw-r--r--	subs_minimize.cpp	13237	log plain
-rw-r--r--	subs_minimize.h	3448	log plain
-rw-r--r--	substitutions.cpp	8832	log plain
-rw-r--r--	substitutions.h	5553	log plain
-rw-r--r--	term_registration_visitor.cpp	12090	log plain
-rw-r--r--	term_registration_visitor.h	4063	log plain
-rw-r--r--	theory.cpp	11769	log plain
-rw-r--r--	theory.h	28775	log plain
-rw-r--r--	theory_engine.cpp	83619	log plain
-rw-r--r--	theory_engine.h	29128	log plain
-rw-r--r--	theory_id.cpp	1783	log plain
-rw-r--r--	theory_id.h	912	log plain
-rw-r--r--	theory_id.i	67	log plain
-rw-r--r--	theory_model.cpp	22993	log plain
-rw-r--r--	theory_model.h	15551	log plain
-rw-r--r--	theory_model_builder.cpp	38394	log plain
-rw-r--r--	theory_model_builder.h	9436	log plain
-rw-r--r--	theory_registrar.h	1489	log plain
-rw-r--r--	theory_test_utils.h	3517	log plain
-rw-r--r--	theory_traits_template.h	1346	log plain
-rw-r--r--	type_enumerator.h	5431	log plain
-rw-r--r--	type_enumerator_template.cpp	1419	log plain
-rw-r--r--	type_set.cpp	2959	log plain
-rw-r--r--	type_set.h	2789	log plain
d---------	uf	730	log plain
-rw-r--r--	valuation.cpp	3736	log plain
-rw-r--r--	valuation.h	4766	log plain