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

drwxr-xr-x		..
-rw-r--r--	1743	CMakeLists.txt	blob \| history \| raw
drwxr-xr-x	-	arith	tree \| history
drwxr-xr-x	-	arrays	tree \| history
-rw-r--r--	777	assertion.cpp	blob \| history \| raw
-rw-r--r--	1498	assertion.h	blob \| history \| raw
-rw-r--r--	2622	atom_requests.cpp	blob \| history \| raw
-rw-r--r--	3158	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--	1634	care_graph.h	blob \| history \| raw
-rw-r--r--	3229	combination_care_graph.cpp	blob \| history \| raw
-rw-r--r--	1453	combination_care_graph.h	blob \| history \| raw
-rw-r--r--	3709	combination_engine.cpp	blob \| history \| raw
-rw-r--r--	4599	combination_engine.h	blob \| history \| raw
drwxr-xr-x	-	datatypes	tree \| history
-rw-r--r--	3430	decision_manager.cpp	blob \| history \| raw
-rw-r--r--	5713	decision_manager.h	blob \| history \| raw
-rw-r--r--	4012	decision_strategy.cpp	blob \| history \| raw
-rw-r--r--	4917	decision_strategy.h	blob \| history \| raw
-rw-r--r--	4763	eager_proof_generator.cpp	blob \| history \| raw
-rw-r--r--	7477	eager_proof_generator.h	blob \| history \| raw
-rw-r--r--	1509	ee_manager.cpp	blob \| history \| raw
-rw-r--r--	3148	ee_manager.h	blob \| history \| raw
-rw-r--r--	3772	ee_manager_distributed.cpp	blob \| history \| raw
-rw-r--r--	3563	ee_manager_distributed.h	blob \| history \| raw
-rw-r--r--	1803	ee_setup_info.h	blob \| history \| raw
-rw-r--r--	6679	engine_output_channel.cpp	blob \| history \| raw
-rw-r--r--	3653	engine_output_channel.h	blob \| history \| raw
-rw-r--r--	29211	evaluator.cpp	blob \| history \| raw
-rw-r--r--	5592	evaluator.h	blob \| history \| raw
-rw-r--r--	15487	ext_theory.cpp	blob \| history \| raw
-rw-r--r--	12846	ext_theory.h	blob \| history \| raw
drwxr-xr-x	-	fp	tree \| history
-rw-r--r--	1969	incomplete_id.cpp	blob \| history \| raw
-rw-r--r--	2472	incomplete_id.h	blob \| history \| raw
-rw-r--r--	21229	inference_id.cpp	blob \| history \| raw
-rw-r--r--	30197	inference_id.h	blob \| history \| raw
-rw-r--r--	5532	inference_manager_buffered.cpp	blob \| history \| raw
-rw-r--r--	6728	inference_manager_buffered.h	blob \| history \| raw
-rw-r--r--	1626	interrupted.h	blob \| history \| raw
-rw-r--r--	4039	lazy_tree_proof_generator.cpp	blob \| history \| raw
-rw-r--r--	7782	lazy_tree_proof_generator.h	blob \| history \| raw
-rw-r--r--	21035	logic_info.cpp	blob \| history \| raw
-rw-r--r--	9173	logic_info.h	blob \| history \| raw
-rwxr-xr-x	6462	mkrewriter	blob \| history \| raw
-rwxr-xr-x	10358	mktheorytraits	blob \| history \| raw
-rw-r--r--	7075	model_manager.cpp	blob \| history \| raw
-rw-r--r--	5836	model_manager.h	blob \| history \| raw
-rw-r--r--	3805	model_manager_distributed.cpp	blob \| history \| raw
-rw-r--r--	2123	model_manager_distributed.h	blob \| history \| raw
-rw-r--r--	2465	output_channel.cpp	blob \| history \| raw
-rw-r--r--	7085	output_channel.h	blob \| history \| raw
drwxr-xr-x	-	quantifiers	tree \| history
-rw-r--r--	22875	quantifiers_engine.cpp	blob \| history \| raw
-rw-r--r--	7592	quantifiers_engine.h	blob \| history \| raw
-rw-r--r--	8290	relevance_manager.cpp	blob \| history \| raw
-rw-r--r--	6261	relevance_manager.h	blob \| history \| raw
-rw-r--r--	12474	rep_set.cpp	blob \| history \| raw
-rw-r--r--	11668	rep_set.h	blob \| history \| raw
-rw-r--r--	17824	rewriter.cpp	blob \| history \| raw
-rw-r--r--	7292	rewriter.h	blob \| history \| raw
-rw-r--r--	2582	rewriter_attributes.h	blob \| history \| raw
-rw-r--r--	2469	rewriter_tables_template.h	blob \| history \| raw
drwxr-xr-x	-	sep	tree \| history
drwxr-xr-x	-	sets	tree \| history
-rw-r--r--	4672	shared_solver.cpp	blob \| history \| raw
-rw-r--r--	4936	shared_solver.h	blob \| history \| raw
-rw-r--r--	2943	shared_solver_distributed.cpp	blob \| history \| raw
-rw-r--r--	2297	shared_solver_distributed.h	blob \| history \| raw
-rw-r--r--	10382	shared_terms_database.cpp	blob \| history \| raw
-rw-r--r--	8946	shared_terms_database.h	blob \| history \| raw
-rw-r--r--	1211	skolem_lemma.cpp	blob \| history \| raw
-rw-r--r--	1899	skolem_lemma.h	blob \| history \| raw
-rw-r--r--	3331	smt_engine_subsolver.cpp	blob \| history \| raw
-rw-r--r--	3496	smt_engine_subsolver.h	blob \| history \| raw
-rw-r--r--	31206	sort_inference.cpp	blob \| history \| raw
-rw-r--r--	6063	sort_inference.h	blob \| history \| raw
drwxr-xr-x	-	strings	tree \| history
-rw-r--r--	13305	subs_minimize.cpp	blob \| history \| raw
-rw-r--r--	3480	subs_minimize.h	blob \| history \| raw
-rw-r--r--	7210	substitutions.cpp	blob \| history \| raw
-rw-r--r--	4917	substitutions.h	blob \| history \| raw
-rw-r--r--	10321	term_registration_visitor.cpp	blob \| history \| raw
-rw-r--r--	6129	term_registration_visitor.h	blob \| history \| raw
-rw-r--r--	16888	theory.cpp	blob \| history \| raw
-rw-r--r--	33270	theory.h	blob \| history \| raw
-rw-r--r--	68117	theory_engine.cpp	blob \| history \| raw
-rw-r--r--	21932	theory_engine.h	blob \| history \| raw
-rw-r--r--	3755	theory_engine_proof_generator.cpp	blob \| history \| raw
-rw-r--r--	2788	theory_engine_proof_generator.h	blob \| history \| raw
-rw-r--r--	2283	theory_eq_notify.h	blob \| history \| raw
-rw-r--r--	4316	theory_id.cpp	blob \| history \| raw
-rw-r--r--	3038	theory_id.h	blob \| history \| raw
-rw-r--r--	1743	theory_inference.cpp	blob \| history \| raw
-rw-r--r--	4030	theory_inference.h	blob \| history \| raw
-rw-r--r--	16708	theory_inference_manager.cpp	blob \| history \| raw
-rw-r--r--	19779	theory_inference_manager.h	blob \| history \| raw
-rw-r--r--	25448	theory_model.cpp	blob \| history \| raw
-rw-r--r--	19169	theory_model.h	blob \| history \| raw
-rw-r--r--	48129	theory_model_builder.cpp	blob \| history \| raw
-rw-r--r--	11839	theory_model_builder.h	blob \| history \| raw
-rw-r--r--	18482	theory_preprocessor.cpp	blob \| history \| raw
-rw-r--r--	8330	theory_preprocessor.h	blob \| history \| raw
-rw-r--r--	7208	theory_proof_step_buffer.cpp	blob \| history \| raw
-rw-r--r--	4721	theory_proof_step_buffer.h	blob \| history \| raw
-rw-r--r--	2071	theory_rewriter.cpp	blob \| history \| raw
-rw-r--r--	4166	theory_rewriter.h	blob \| history \| raw
-rw-r--r--	3919	theory_state.cpp	blob \| history \| raw
-rw-r--r--	4373	theory_state.h	blob \| history \| raw
-rw-r--r--	1333	theory_traits_template.h	blob \| history \| raw
-rw-r--r--	4160	trust_node.cpp	blob \| history \| raw
-rw-r--r--	5994	trust_node.h	blob \| history \| raw
-rw-r--r--	8384	trust_substitutions.cpp	blob \| history \| raw
-rw-r--r--	5026	trust_substitutions.h	blob \| history \| raw
-rw-r--r--	5492	type_enumerator.h	blob \| history \| raw
-rw-r--r--	1338	type_enumerator_template.cpp	blob \| history \| raw
-rw-r--r--	2982	type_set.cpp	blob \| history \| raw
-rw-r--r--	2817	type_set.h	blob \| history \| raw
drwxr-xr-x	-	uf	tree \| history
-rw-r--r--	5902	valuation.cpp	blob \| history \| raw
-rw-r--r--	7456	valuation.h	blob \| history \| raw