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	3049	log plain
d---------	arrays	704	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	1722	log plain
-rw-r--r--	care_graph.h	1665	log plain
d---------	datatypes	768	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	3598	log plain
-rw-r--r--	eager_proof_generator.h	6772	log plain
-rw-r--r--	engine_output_channel.cpp	11511	log plain
-rw-r--r--	engine_output_channel.h	3961	log plain
-rw-r--r--	evaluator.cpp	28600	log plain
-rw-r--r--	evaluator.h	5417	log plain
d---------	example	162	log plain
-rw-r--r--	ext_theory.cpp	15445	log plain
-rw-r--r--	ext_theory.h	9693	log plain
d---------	fp	392	log plain
-rw-r--r--	interrupted.h	1613	log plain
-rw-r--r--	logic_info.cpp	20917	log plain
-rw-r--r--	logic_info.h	9243	log plain
-rwxr-xr-x	mkrewriter	6483	log plain
-rwxr-xr-x	mktheorytraits	10487	log plain
-rw-r--r--	output_channel.h	8163	log plain
d---------	quantifiers	4010	log plain
-rw-r--r--	quantifiers_engine.cpp	46506	log plain
-rw-r--r--	quantifiers_engine.h	15506	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	12147	log plain
-rw-r--r--	rewriter.h	5501	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	1034	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--	smt_engine_subsolver.cpp	3485	log plain
-rw-r--r--	smt_engine_subsolver.h	3227	log plain
-rw-r--r--	sort_inference.cpp	31162	log plain
-rw-r--r--	sort_inference.h	6024	log plain
d---------	strings	2460	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	12009	log plain
-rw-r--r--	term_registration_visitor.h	4063	log plain
-rw-r--r--	theory.cpp	12937	log plain
-rw-r--r--	theory.h	30872	log plain
-rw-r--r--	theory_engine.cpp	73967	log plain
-rw-r--r--	theory_engine.h	25680	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	2350	log plain
-rw-r--r--	theory_engine_proof_generator.h	2731	log plain
-rw-r--r--	theory_id.cpp	2505	log plain
-rw-r--r--	theory_id.h	1576	log plain
-rw-r--r--	theory_model.cpp	25210	log plain
-rw-r--r--	theory_model.h	19294	log plain
-rw-r--r--	theory_model_builder.cpp	48053	log plain
-rw-r--r--	theory_model_builder.h	13192	log plain
-rw-r--r--	theory_preprocessor.cpp	7274	log plain
-rw-r--r--	theory_preprocessor.h	2498	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	2854	log plain
-rw-r--r--	theory_proof_step_buffer.h	3254	log plain
-rw-r--r--	theory_registrar.h	1489	log plain
-rw-r--r--	theory_rewriter.h	2650	log plain
-rw-r--r--	theory_test_utils.h	3564	log plain
-rw-r--r--	theory_traits_template.h	1363	log plain
-rw-r--r--	trust_node.cpp	3552	log plain
-rw-r--r--	trust_node.h	5434	log plain
-rw-r--r--	type_enumerator.h	5431	log plain
-rw-r--r--	type_enumerator_template.cpp	1420	log plain
-rw-r--r--	type_set.cpp	2959	log plain
-rw-r--r--	type_set.h	2806	log plain
d---------	uf	818	log plain
-rw-r--r--	valuation.cpp	3791	log plain
-rw-r--r--	valuation.h	4793	log plain