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	3532	log plain
d---------	arrays	816	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	3158	log plain
d---------	bags	1299	log plain
d---------	booleans	666	log plain
d---------	builtin	523	log plain
d---------	bv	2224	log plain
-rw-r--r--	care_graph.h	1634	log plain
-rw-r--r--	combination_care_graph.cpp	3229	log plain
-rw-r--r--	combination_care_graph.h	1453	log plain
-rw-r--r--	combination_engine.cpp	3709	log plain
-rw-r--r--	combination_engine.h	4599	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	4012	log plain
-rw-r--r--	decision_strategy.h	4917	log plain
-rw-r--r--	eager_proof_generator.cpp	4763	log plain
-rw-r--r--	eager_proof_generator.h	7477	log plain
-rw-r--r--	ee_manager.cpp	1509	log plain
-rw-r--r--	ee_manager.h	3148	log plain
-rw-r--r--	ee_manager_distributed.cpp	3772	log plain
-rw-r--r--	ee_manager_distributed.h	3563	log plain
-rw-r--r--	ee_setup_info.h	1803	log plain
-rw-r--r--	engine_output_channel.cpp	6358	log plain
-rw-r--r--	engine_output_channel.h	3597	log plain
-rw-r--r--	evaluator.cpp	29211	log plain
-rw-r--r--	evaluator.h	5592	log plain
-rw-r--r--	ext_theory.cpp	15487	log plain
-rw-r--r--	ext_theory.h	12846	log plain
d---------	fp	534	log plain
-rw-r--r--	incomplete_id.cpp	1969	log plain
-rw-r--r--	incomplete_id.h	2472	log plain
-rw-r--r--	inference_id.cpp	21306	log plain
-rw-r--r--	inference_id.h	30266	log plain
-rw-r--r--	inference_manager_buffered.cpp	5542	log plain
-rw-r--r--	inference_manager_buffered.h	6733	log plain
-rw-r--r--	interrupted.h	1626	log plain
-rw-r--r--	lazy_tree_proof_generator.cpp	4039	log plain
-rw-r--r--	lazy_tree_proof_generator.h	7782	log plain
-rw-r--r--	logic_info.cpp	21035	log plain
-rw-r--r--	logic_info.h	9173	log plain
-rwxr-xr-x	mkrewriter	6462	log plain
-rwxr-xr-x	mktheorytraits	10358	log plain
-rw-r--r--	model_manager.cpp	7075	log plain
-rw-r--r--	model_manager.h	5836	log plain
-rw-r--r--	model_manager_distributed.cpp	3805	log plain
-rw-r--r--	model_manager_distributed.h	2123	log plain
-rw-r--r--	output_channel.cpp	2465	log plain
-rw-r--r--	output_channel.h	7051	log plain
d---------	quantifiers	5089	log plain
-rw-r--r--	quantifiers_engine.cpp	23034	log plain
-rw-r--r--	quantifiers_engine.h	7675	log plain
-rw-r--r--	relevance_manager.cpp	8540	log plain
-rw-r--r--	relevance_manager.h	6927	log plain
-rw-r--r--	rep_set.cpp	12474	log plain
-rw-r--r--	rep_set.h	11668	log plain
-rw-r--r--	rewriter.cpp	17807	log plain
-rw-r--r--	rewriter.h	7292	log plain
-rw-r--r--	rewriter_attributes.h	2582	log plain
-rw-r--r--	rewriter_tables_template.h	2990	log plain
d---------	sep	319	log plain
d---------	sets	1262	log plain
-rw-r--r--	shared_solver.cpp	4672	log plain
-rw-r--r--	shared_solver.h	4936	log plain
-rw-r--r--	shared_solver_distributed.cpp	2943	log plain
-rw-r--r--	shared_solver_distributed.h	2297	log plain
-rw-r--r--	shared_terms_database.cpp	10254	log plain
-rw-r--r--	shared_terms_database.h	8917	log plain
-rw-r--r--	skolem_lemma.cpp	1211	log plain
-rw-r--r--	skolem_lemma.h	1899	log plain
-rw-r--r--	smt_engine_subsolver.cpp	3331	log plain
-rw-r--r--	smt_engine_subsolver.h	3496	log plain
-rw-r--r--	sort_inference.cpp	31206	log plain
-rw-r--r--	sort_inference.h	6063	log plain
d---------	strings	2785	log plain
-rw-r--r--	subs_minimize.cpp	13305	log plain
-rw-r--r--	subs_minimize.h	3480	log plain
-rw-r--r--	substitutions.cpp	7251	log plain
-rw-r--r--	substitutions.h	4649	log plain
-rw-r--r--	term_registration_visitor.cpp	10417	log plain
-rw-r--r--	term_registration_visitor.h	6129	log plain
-rw-r--r--	theory.cpp	16962	log plain
-rw-r--r--	theory.h	31557	log plain
-rw-r--r--	theory_engine.cpp	68547	log plain
-rw-r--r--	theory_engine.h	23806	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	3755	log plain
-rw-r--r--	theory_engine_proof_generator.h	2788	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	16722	log plain
-rw-r--r--	theory_inference_manager.h	19694	log plain
-rw-r--r--	theory_model.cpp	26255	log plain
-rw-r--r--	theory_model.h	19169	log plain
-rw-r--r--	theory_model_builder.cpp	48282	log plain
-rw-r--r--	theory_model_builder.h	12008	log plain
-rw-r--r--	theory_preprocessor.cpp	18482	log plain
-rw-r--r--	theory_preprocessor.h	8330	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	7457	log plain
-rw-r--r--	theory_proof_step_buffer.h	4974	log plain
-rw-r--r--	theory_rewriter.cpp	2176	log plain
-rw-r--r--	theory_rewriter.h	5461	log plain
-rw-r--r--	theory_state.cpp	4013	log plain
-rw-r--r--	theory_state.h	4571	log plain
-rw-r--r--	theory_traits_template.h	1476	log plain
-rw-r--r--	trust_node.cpp	4160	log plain
-rw-r--r--	trust_node.h	5994	log plain
-rw-r--r--	trust_substitutions.cpp	9833	log plain
-rw-r--r--	trust_substitutions.h	5381	log plain
-rw-r--r--	type_enumerator.h	5492	log plain
-rw-r--r--	type_enumerator_template.cpp	1484	log plain
-rw-r--r--	type_set.cpp	2982	log plain
-rw-r--r--	type_set.h	2817	log plain
d---------	uf	1264	log plain
-rw-r--r--	valuation.cpp	5992	log plain
-rw-r--r--	valuation.h	7654	log plain