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	1589	log plain
d---------	arith	3477	log plain
d---------	arrays	760	log plain
-rw-r--r--	assertion.cpp	786	log plain
-rw-r--r--	assertion.h	1541	log plain
-rw-r--r--	atom_requests.cpp	2597	log plain
-rw-r--r--	atom_requests.h	3145	log plain
d---------	bags	1299	log plain
d---------	booleans	612	log plain
d---------	builtin	523	log plain
d---------	bv	2172	log plain
-rw-r--r--	care_graph.h	1653	log plain
-rw-r--r--	combination_care_graph.cpp	3224	log plain
-rw-r--r--	combination_care_graph.h	1446	log plain
-rw-r--r--	combination_engine.cpp	3700	log plain
-rw-r--r--	combination_engine.h	4573	log plain
d---------	datatypes	1220	log plain
-rw-r--r--	decision_manager.cpp	3406	log plain
-rw-r--r--	decision_manager.h	5701	log plain
-rw-r--r--	decision_strategy.cpp	3989	log plain
-rw-r--r--	decision_strategy.h	4906	log plain
-rw-r--r--	eager_proof_generator.cpp	4756	log plain
-rw-r--r--	eager_proof_generator.h	7453	log plain
-rw-r--r--	ee_manager.cpp	1492	log plain
-rw-r--r--	ee_manager.h	3129	log plain
-rw-r--r--	ee_manager_distributed.cpp	3767	log plain
-rw-r--r--	ee_manager_distributed.h	3542	log plain
-rw-r--r--	ee_setup_info.h	1787	log plain
-rw-r--r--	engine_output_channel.cpp	6564	log plain
-rw-r--r--	engine_output_channel.h	3630	log plain
-rw-r--r--	evaluator.cpp	29221	log plain
-rw-r--r--	evaluator.h	5574	log plain
-rw-r--r--	ext_theory.cpp	15615	log plain
-rw-r--r--	ext_theory.h	11803	log plain
d---------	fp	444	log plain
-rw-r--r--	inference_id.cpp	20163	log plain
-rw-r--r--	inference_id.h	30180	log plain
-rw-r--r--	inference_manager_buffered.cpp	5516	log plain
-rw-r--r--	inference_manager_buffered.h	6724	log plain
-rw-r--r--	interrupted.h	1605	log plain
-rw-r--r--	lazy_tree_proof_generator.cpp	4035	log plain
-rw-r--r--	lazy_tree_proof_generator.h	7777	log plain
-rw-r--r--	logic_info.cpp	21129	log plain
-rw-r--r--	logic_info.h	9263	log plain
-rwxr-xr-x	mkrewriter	6208	log plain
-rwxr-xr-x	mktheorytraits	10096	log plain
-rw-r--r--	model_manager.cpp	7061	log plain
-rw-r--r--	model_manager.h	5805	log plain
-rw-r--r--	model_manager_distributed.cpp	3803	log plain
-rw-r--r--	model_manager_distributed.h	2119	log plain
-rw-r--r--	output_channel.cpp	2451	log plain
-rw-r--r--	output_channel.h	7065	log plain
d---------	quantifiers	4750	log plain
-rw-r--r--	quantifiers_engine.cpp	22753	log plain
-rw-r--r--	quantifiers_engine.h	7580	log plain
-rw-r--r--	relevance_manager.cpp	8266	log plain
-rw-r--r--	relevance_manager.h	6249	log plain
-rw-r--r--	rep_set.cpp	12453	log plain
-rw-r--r--	rep_set.h	11645	log plain
-rw-r--r--	rewriter.cpp	17901	log plain
-rw-r--r--	rewriter.h	7298	log plain
-rw-r--r--	rewriter_attributes.h	2600	log plain
-rw-r--r--	rewriter_tables_template.h	2466	log plain
d---------	sep	266	log plain
d---------	sets	1208	log plain
-rw-r--r--	shared_solver.cpp	4657	log plain
-rw-r--r--	shared_solver.h	4904	log plain
-rw-r--r--	shared_solver_distributed.cpp	2940	log plain
-rw-r--r--	shared_solver_distributed.h	2293	log plain
-rw-r--r--	shared_terms_database.cpp	10370	log plain
-rw-r--r--	shared_terms_database.h	8932	log plain
-rw-r--r--	skolem_lemma.cpp	1195	log plain
-rw-r--r--	skolem_lemma.h	1881	log plain
-rw-r--r--	smt_engine_subsolver.cpp	3325	log plain
-rw-r--r--	smt_engine_subsolver.h	3491	log plain
-rw-r--r--	sort_inference.cpp	31196	log plain
-rw-r--r--	sort_inference.h	6047	log plain
d---------	strings	2728	log plain
-rw-r--r--	subs_minimize.cpp	13275	log plain
-rw-r--r--	subs_minimize.h	3464	log plain
-rw-r--r--	substitutions.cpp	7253	log plain
-rw-r--r--	substitutions.h	4958	log plain
-rw-r--r--	term_registration_visitor.cpp	10313	log plain
-rw-r--r--	term_registration_visitor.h	6134	log plain
-rw-r--r--	theory.cpp	16362	log plain
-rw-r--r--	theory.h	33133	log plain
-rw-r--r--	theory_engine.cpp	67089	log plain
-rw-r--r--	theory_engine.h	21628	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	3742	log plain
-rw-r--r--	theory_engine_proof_generator.h	2787	log plain
-rw-r--r--	theory_eq_notify.h	2270	log plain
-rw-r--r--	theory_id.cpp	4301	log plain
-rw-r--r--	theory_id.h	3021	log plain
-rw-r--r--	theory_inference.cpp	1717	log plain
-rw-r--r--	theory_inference.h	4016	log plain
-rw-r--r--	theory_inference_manager.cpp	16685	log plain
-rw-r--r--	theory_inference_manager.h	19758	log plain
-rw-r--r--	theory_model.cpp	25432	log plain
-rw-r--r--	theory_model.h	19151	log plain
-rw-r--r--	theory_model_builder.cpp	48121	log plain
-rw-r--r--	theory_model_builder.h	11829	log plain
-rw-r--r--	theory_preprocessor.cpp	18473	log plain
-rw-r--r--	theory_preprocessor.h	8320	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	7190	log plain
-rw-r--r--	theory_proof_step_buffer.h	4716	log plain
-rw-r--r--	theory_rewriter.cpp	2088	log plain
-rw-r--r--	theory_rewriter.h	4181	log plain
-rw-r--r--	theory_state.cpp	3903	log plain
-rw-r--r--	theory_state.h	4355	log plain
-rw-r--r--	theory_traits_template.h	1331	log plain
-rw-r--r--	trust_node.cpp	4142	log plain
-rw-r--r--	trust_node.h	5974	log plain
-rw-r--r--	trust_substitutions.cpp	8375	log plain
-rw-r--r--	trust_substitutions.h	5015	log plain
-rw-r--r--	type_enumerator.h	5507	log plain
-rw-r--r--	type_enumerator_template.cpp	1365	log plain
-rw-r--r--	type_set.cpp	2948	log plain
-rw-r--r--	type_set.h	2795	log plain
d---------	uf	1162	log plain
-rw-r--r--	valuation.cpp	5926	log plain
-rw-r--r--	valuation.h	7440	log plain