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	1743	log plain
d---------	arith	3856	log plain
d---------	arrays	863	log plain
-rw-r--r--	assertion.cpp	777	log plain
-rw-r--r--	assertion.h	1498	log plain
-rw-r--r--	atom_requests.cpp	2622	log plain
-rw-r--r--	atom_requests.h	3140	log plain
d---------	bags	1299	log plain
d---------	booleans	666	log plain
d---------	builtin	523	log plain
d---------	bv	1303	log plain
-rw-r--r--	care_graph.h	1634	log plain
-rw-r--r--	combination_care_graph.cpp	3299	log plain
-rw-r--r--	combination_care_graph.h	1440	log plain
-rw-r--r--	combination_engine.cpp	4220	log plain
-rw-r--r--	combination_engine.h	4509	log plain
d---------	datatypes	1279	log plain
-rw-r--r--	decision_manager.cpp	3430	log plain
-rw-r--r--	decision_manager.h	5713	log plain
-rw-r--r--	decision_strategy.cpp	4083	log plain
-rw-r--r--	decision_strategy.h	4943	log plain
-rw-r--r--	difficulty_manager.cpp	3023	log plain
-rw-r--r--	difficulty_manager.h	2748	log plain
-rw-r--r--	ee_manager.cpp	1553	log plain
-rw-r--r--	ee_manager.h	3202	log plain
-rw-r--r--	ee_manager_central.cpp	10422	log plain
-rw-r--r--	ee_manager_central.h	5213	log plain
-rw-r--r--	ee_manager_distributed.cpp	3517	log plain
-rw-r--r--	ee_manager_distributed.h	2653	log plain
-rw-r--r--	ee_setup_info.h	2719	log plain
-rw-r--r--	engine_output_channel.cpp	5244	log plain
-rw-r--r--	engine_output_channel.h	3456	log plain
-rw-r--r--	evaluator.cpp	28946	log plain
-rw-r--r--	evaluator.h	5863	log plain
-rw-r--r--	ext_theory.cpp	15541	log plain
-rw-r--r--	ext_theory.h	12828	log plain
d---------	fp	540	log plain
-rw-r--r--	incomplete_id.cpp	2167	log plain
-rw-r--r--	incomplete_id.h	2906	log plain
-rw-r--r--	inference_id.cpp	26406	log plain
-rw-r--r--	inference_id.h	35503	log plain
-rw-r--r--	inference_manager_buffered.cpp	5702	log plain
-rw-r--r--	inference_manager_buffered.h	7055	log plain
-rw-r--r--	interrupted.h	1626	log plain
-rw-r--r--	logic_info.cpp	20765	log plain
-rw-r--r--	logic_info.h	9447	log plain
-rwxr-xr-x	mkrewriter	6462	log plain
-rwxr-xr-x	mktheorytraits	10358	log plain
-rw-r--r--	model_manager.cpp	5144	log plain
-rw-r--r--	model_manager.h	5081	log plain
-rw-r--r--	model_manager_distributed.cpp	4216	log plain
-rw-r--r--	model_manager_distributed.h	2111	log plain
-rw-r--r--	output_channel.cpp	2390	log plain
-rw-r--r--	output_channel.h	6787	log plain
d---------	quantifiers	5581	log plain
-rw-r--r--	quantifiers_engine.cpp	24536	log plain
-rw-r--r--	quantifiers_engine.h	7698	log plain
-rw-r--r--	relevance_manager.cpp	9559	log plain
-rw-r--r--	relevance_manager.h	8075	log plain
-rw-r--r--	rep_set.cpp	12621	log plain
-rw-r--r--	rep_set.h	11668	log plain
-rw-r--r--	rewriter.cpp	16506	log plain
-rw-r--r--	rewriter.h	6167	log plain
-rw-r--r--	rewriter_attributes.h	2582	log plain
-rw-r--r--	rewriter_tables_template.h	2758	log plain
d---------	sep	319	log plain
d---------	sets	1262	log plain
-rw-r--r--	shared_solver.cpp	5374	log plain
-rw-r--r--	shared_solver.h	5335	log plain
-rw-r--r--	shared_solver_distributed.cpp	2755	log plain
-rw-r--r--	shared_solver_distributed.h	2206	log plain
-rw-r--r--	shared_terms_database.cpp	10327	log plain
-rw-r--r--	shared_terms_database.h	8734	log plain
-rw-r--r--	skolem_lemma.cpp	1280	log plain
-rw-r--r--	skolem_lemma.h	1959	log plain
-rw-r--r--	smt_engine_subsolver.cpp	5056	log plain
-rw-r--r--	smt_engine_subsolver.h	5552	log plain
-rw-r--r--	sort_inference.cpp	31201	log plain
-rw-r--r--	sort_inference.h	6142	log plain
d---------	strings	2967	log plain
-rw-r--r--	subs_minimize.cpp	13168	log plain
-rw-r--r--	subs_minimize.h	3420	log plain
-rw-r--r--	substitutions.cpp	7173	log plain
-rw-r--r--	substitutions.h	4588	log plain
-rw-r--r--	term_registration_visitor.cpp	10507	log plain
-rw-r--r--	term_registration_visitor.h	6007	log plain
-rw-r--r--	theory.cpp	20542	log plain
-rw-r--r--	theory.h	30950	log plain
-rw-r--r--	theory_engine.cpp	67287	log plain
-rw-r--r--	theory_engine.h	21033	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	3720	log plain
-rw-r--r--	theory_engine_proof_generator.h	2733	log plain
-rw-r--r--	theory_eq_notify.h	2283	log plain
-rw-r--r--	theory_id.cpp	4344	log plain
-rw-r--r--	theory_id.h	3038	log plain
-rw-r--r--	theory_inference.cpp	1743	log plain
-rw-r--r--	theory_inference.h	4030	log plain
-rw-r--r--	theory_inference_manager.cpp	18223	log plain
-rw-r--r--	theory_inference_manager.h	19994	log plain
-rw-r--r--	theory_model.cpp	25996	log plain
-rw-r--r--	theory_model.h	19064	log plain
-rw-r--r--	theory_model_builder.cpp	49095	log plain
-rw-r--r--	theory_model_builder.h	12160	log plain
-rw-r--r--	theory_preprocessor.cpp	18011	log plain
-rw-r--r--	theory_preprocessor.h	7467	log plain
-rw-r--r--	theory_rewriter.cpp	2176	log plain
-rw-r--r--	theory_rewriter.h	5460	log plain
-rw-r--r--	theory_state.cpp	3643	log plain
-rw-r--r--	theory_state.h	4072	log plain
-rw-r--r--	theory_traits_template.h	1476	log plain
-rw-r--r--	trust_substitutions.cpp	9915	log plain
-rw-r--r--	trust_substitutions.h	5444	log plain
-rw-r--r--	type_enumerator.h	5862	log plain
-rw-r--r--	type_enumerator_template.cpp	1484	log plain
-rw-r--r--	type_set.cpp	2944	log plain
-rw-r--r--	type_set.h	2742	log plain
d---------	uf	1530	log plain
-rw-r--r--	valuation.cpp	6190	log plain
-rw-r--r--	valuation.h	7974	log plain