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	3441	log plain
d---------	arrays	664	log plain
-rw-r--r--	assertion.cpp	795	log plain
-rw-r--r--	assertion.h	1551	log plain
-rw-r--r--	atom_requests.cpp	2598	log plain
-rw-r--r--	atom_requests.h	3128	log plain
d---------	booleans	502	log plain
d---------	builtin	466	log plain
d---------	bv	1851	log plain
-rw-r--r--	care_graph.h	1665	log plain
-rw-r--r--	combination_care_graph.cpp	3137	log plain
-rw-r--r--	combination_care_graph.h	1447	log plain
-rw-r--r--	combination_engine.cpp	3504	log plain
-rw-r--r--	combination_engine.h	4304	log plain
d---------	datatypes	864	log plain
-rw-r--r--	decision_manager.cpp	3407	log plain
-rw-r--r--	decision_manager.h	5741	log plain
-rw-r--r--	decision_strategy.cpp	3990	log plain
-rw-r--r--	decision_strategy.h	4922	log plain
-rw-r--r--	eager_proof_generator.cpp	4286	log plain
-rw-r--r--	eager_proof_generator.h	7046	log plain
-rw-r--r--	ee_manager.cpp	1448	log plain
-rw-r--r--	ee_manager.h	2910	log plain
-rw-r--r--	ee_manager_distributed.cpp	3348	log plain
-rw-r--r--	ee_manager_distributed.h	3429	log plain
-rw-r--r--	ee_setup_info.h	1591	log plain
-rw-r--r--	engine_output_channel.cpp	6638	log plain
-rw-r--r--	engine_output_channel.h	3686	log plain
-rw-r--r--	evaluator.cpp	29375	log plain
-rw-r--r--	evaluator.h	5575	log plain
-rw-r--r--	ext_theory.cpp	16022	log plain
-rw-r--r--	ext_theory.h	11893	log plain
d---------	fp	392	log plain
-rw-r--r--	inference_manager_buffered.cpp	3682	log plain
-rw-r--r--	inference_manager_buffered.h	5102	log plain
-rw-r--r--	interrupted.h	1613	log plain
-rw-r--r--	logic_info.cpp	21044	log plain
-rw-r--r--	logic_info.h	9243	log plain
-rwxr-xr-x	mkrewriter	6208	log plain
-rwxr-xr-x	mktheorytraits	10102	log plain
-rw-r--r--	model_manager.cpp	6597	log plain
-rw-r--r--	model_manager.h	5828	log plain
-rw-r--r--	model_manager_distributed.cpp	3578	log plain
-rw-r--r--	model_manager_distributed.h	2139	log plain
-rw-r--r--	output_channel.cpp	2926	log plain
-rw-r--r--	output_channel.h	8240	log plain
d---------	quantifiers	4206	log plain
-rw-r--r--	quantifiers_engine.cpp	41464	log plain
-rw-r--r--	quantifiers_engine.h	16435	log plain
-rw-r--r--	relevance_manager.cpp	8247	log plain
-rw-r--r--	relevance_manager.h	6250	log plain
-rw-r--r--	rep_set.cpp	12466	log plain
-rw-r--r--	rep_set.h	11656	log plain
-rw-r--r--	rewriter.cpp	15936	log plain
-rw-r--r--	rewriter.h	7590	log plain
-rw-r--r--	rewriter_attributes.h	2609	log plain
-rw-r--r--	rewriter_tables_template.h	2458	log plain
d---------	sep	266	log plain
d---------	sets	1122	log plain
-rw-r--r--	shared_solver.cpp	3560	log plain
-rw-r--r--	shared_solver.h	4740	log plain
-rw-r--r--	shared_solver_distributed.cpp	2859	log plain
-rw-r--r--	shared_solver_distributed.h	2271	log plain
-rw-r--r--	shared_terms_database.cpp	9716	log plain
-rw-r--r--	shared_terms_database.h	8167	log plain
-rw-r--r--	smt_engine_subsolver.cpp	3391	log plain
-rw-r--r--	smt_engine_subsolver.h	3126	log plain
-rw-r--r--	sort_inference.cpp	31129	log plain
-rw-r--r--	sort_inference.h	6024	log plain
d---------	strings	2548	log plain
-rw-r--r--	subs_minimize.cpp	13290	log plain
-rw-r--r--	subs_minimize.h	3465	log plain
-rw-r--r--	substitutions.cpp	8861	log plain
-rw-r--r--	substitutions.h	5553	log plain
-rw-r--r--	term_registration_visitor.cpp	12464	log plain
-rw-r--r--	term_registration_visitor.h	4079	log plain
-rw-r--r--	theory.cpp	17281	log plain
-rw-r--r--	theory.h	33030	log plain
-rw-r--r--	theory_engine.cpp	67662	log plain
-rw-r--r--	theory_engine.h	24066	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	3693	log plain
-rw-r--r--	theory_engine_proof_generator.h	2771	log plain
-rw-r--r--	theory_eq_notify.h	2244	log plain
-rw-r--r--	theory_id.cpp	4171	log plain
-rw-r--r--	theory_id.h	3033	log plain
-rw-r--r--	theory_inference.cpp	1934	log plain
-rw-r--r--	theory_inference.h	4479	log plain
-rw-r--r--	theory_inference_manager.cpp	14355	log plain
-rw-r--r--	theory_inference_manager.h	18133	log plain
-rw-r--r--	theory_model.cpp	25548	log plain
-rw-r--r--	theory_model.h	19198	log plain
-rw-r--r--	theory_model_builder.cpp	47444	log plain
-rw-r--r--	theory_model_builder.h	13453	log plain
-rw-r--r--	theory_preprocessor.cpp	13269	log plain
-rw-r--r--	theory_preprocessor.h	3941	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	6419	log plain
-rw-r--r--	theory_proof_step_buffer.h	4164	log plain
-rw-r--r--	theory_registrar.h	1489	log plain
-rw-r--r--	theory_rewriter.cpp	2089	log plain
-rw-r--r--	theory_rewriter.h	4182	log plain
-rw-r--r--	theory_state.cpp	2942	log plain
-rw-r--r--	theory_state.h	3258	log plain
-rw-r--r--	theory_test_utils.h	3415	log plain
-rw-r--r--	theory_traits_template.h	1339	log plain
-rw-r--r--	trust_node.cpp	4061	log plain
-rw-r--r--	trust_node.h	5966	log plain
-rw-r--r--	type_enumerator.h	5431	log plain
-rw-r--r--	type_enumerator_template.cpp	1374	log plain
-rw-r--r--	type_set.cpp	2959	log plain
-rw-r--r--	type_set.h	2806	log plain
d---------	uf	1162	log plain
-rw-r--r--	valuation.cpp	4850	log plain
-rw-r--r--	valuation.h	5575	log plain