git.libre-soc.org Git - cvc5.git/tree

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