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	3647	log plain
d---------	arrays	760	log plain
-rw-r--r--	assertion.cpp	794	log plain
-rw-r--r--	assertion.h	1550	log plain
-rw-r--r--	atom_requests.cpp	2597	log plain
-rw-r--r--	atom_requests.h	3127	log plain
d---------	bags	981	log plain
d---------	booleans	612	log plain
d---------	builtin	523	log plain
d---------	bv	1945	log plain
-rw-r--r--	care_graph.h	1664	log plain
-rw-r--r--	combination_care_graph.cpp	3153	log plain
-rw-r--r--	combination_care_graph.h	1446	log plain
-rw-r--r--	combination_engine.cpp	3825	log plain
-rw-r--r--	combination_engine.h	4782	log plain
d---------	datatypes	1126	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	4921	log plain
-rw-r--r--	eager_proof_generator.cpp	4453	log plain
-rw-r--r--	eager_proof_generator.h	7045	log plain
-rw-r--r--	ee_manager.cpp	1492	log plain
-rw-r--r--	ee_manager.h	3197	log plain
-rw-r--r--	ee_manager_distributed.cpp	3847	log plain
-rw-r--r--	ee_manager_distributed.h	3581	log plain
-rw-r--r--	ee_setup_info.h	1590	log plain
-rw-r--r--	engine_output_channel.cpp	6642	log plain
-rw-r--r--	engine_output_channel.h	3684	log plain
-rw-r--r--	evaluator.cpp	29374	log plain
-rw-r--r--	evaluator.h	5574	log plain
-rw-r--r--	ext_theory.cpp	16021	log plain
-rw-r--r--	ext_theory.h	11892	log plain
d---------	fp	392	log plain
-rw-r--r--	inference_manager_buffered.cpp	4100	log plain
-rw-r--r--	inference_manager_buffered.h	5427	log plain
-rw-r--r--	interrupted.h	1612	log plain
-rw-r--r--	logic_info.cpp	21130	log plain
-rw-r--r--	logic_info.h	9242	log plain
-rwxr-xr-x	mkrewriter	6208	log plain
-rwxr-xr-x	mktheorytraits	10102	log plain
-rw-r--r--	model_manager.cpp	6596	log plain
-rw-r--r--	model_manager.h	5827	log plain
-rw-r--r--	model_manager_distributed.cpp	3762	log plain
-rw-r--r--	model_manager_distributed.h	2138	log plain
-rw-r--r--	output_channel.cpp	2927	log plain
-rw-r--r--	output_channel.h	8240	log plain
d---------	quantifiers	4114	log plain
-rw-r--r--	quantifiers_engine.cpp	41304	log plain
-rw-r--r--	quantifiers_engine.h	15857	log plain
-rw-r--r--	relevance_manager.cpp	8246	log plain
-rw-r--r--	relevance_manager.h	6249	log plain
-rw-r--r--	rep_set.cpp	12463	log plain
-rw-r--r--	rep_set.h	11653	log plain
-rw-r--r--	rewriter.cpp	17651	log plain
-rw-r--r--	rewriter.h	7389	log plain
-rw-r--r--	rewriter_attributes.h	2608	log plain
-rw-r--r--	rewriter_tables_template.h	2474	log plain
d---------	sep	266	log plain
d---------	sets	1208	log plain
-rw-r--r--	shared_solver.cpp	3611	log plain
-rw-r--r--	shared_solver.h	4800	log plain
-rw-r--r--	shared_solver_distributed.cpp	2941	log plain
-rw-r--r--	shared_solver_distributed.h	2294	log plain
-rw-r--r--	shared_terms_database.cpp	10372	log plain
-rw-r--r--	shared_terms_database.h	8913	log plain
-rw-r--r--	smt_engine_subsolver.cpp	3350	log plain
-rw-r--r--	smt_engine_subsolver.h	3506	log plain
-rw-r--r--	sort_inference.cpp	31128	log plain
-rw-r--r--	sort_inference.h	6023	log plain
d---------	strings	2642	log plain
-rw-r--r--	subs_minimize.cpp	13289	log plain
-rw-r--r--	subs_minimize.h	3464	log plain
-rw-r--r--	substitutions.cpp	7179	log plain
-rw-r--r--	substitutions.h	4907	log plain
-rw-r--r--	term_registration_visitor.cpp	12463	log plain
-rw-r--r--	term_registration_visitor.h	4085	log plain
-rw-r--r--	theory.cpp	16135	log plain
-rw-r--r--	theory.h	32749	log plain
-rw-r--r--	theory_engine.cpp	74697	log plain
-rw-r--r--	theory_engine.h	24187	log plain
-rw-r--r--	theory_engine_proof_generator.cpp	3692	log plain
-rw-r--r--	theory_engine_proof_generator.h	2787	log plain
-rw-r--r--	theory_eq_notify.h	2244	log plain
-rw-r--r--	theory_id.cpp	4273	log plain
-rw-r--r--	theory_id.h	3047	log plain
-rw-r--r--	theory_inference.cpp	1933	log plain
-rw-r--r--	theory_inference.h	4478	log plain
-rw-r--r--	theory_inference_manager.cpp	14386	log plain
-rw-r--r--	theory_inference_manager.h	18163	log plain
-rw-r--r--	theory_model.cpp	24935	log plain
-rw-r--r--	theory_model.h	19009	log plain
-rw-r--r--	theory_model_builder.cpp	47556	log plain
-rw-r--r--	theory_model_builder.h	13458	log plain
-rw-r--r--	theory_preprocessor.cpp	15474	log plain
-rw-r--r--	theory_preprocessor.h	4940	log plain
-rw-r--r--	theory_proof_step_buffer.cpp	7174	log plain
-rw-r--r--	theory_proof_step_buffer.h	4700	log plain
-rw-r--r--	theory_registrar.h	1488	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	3065	log plain
-rw-r--r--	theory_state.h	3426	log plain
-rw-r--r--	theory_test_utils.h	3639	log plain
-rw-r--r--	theory_traits_template.h	1338	log plain
-rw-r--r--	trust_node.cpp	4104	log plain
-rw-r--r--	trust_node.h	5971	log plain
-rw-r--r--	trust_substitutions.cpp	8313	log plain
-rw-r--r--	trust_substitutions.h	4998	log plain
-rw-r--r--	type_enumerator.h	5430	log plain
-rw-r--r--	type_enumerator_template.cpp	1373	log plain
-rw-r--r--	type_set.cpp	2958	log plain
-rw-r--r--	type_set.h	2805	log plain
d---------	uf	1162	log plain
-rw-r--r--	valuation.cpp	4849	log plain
-rw-r--r--	valuation.h	5574	log plain