equal
deleted
inserted
replaced
199 val max_default_remote_threads = 4 |
199 val max_default_remote_threads = 4 |
200 |
200 |
201 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
201 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
202 timeout, it makes sense to put SPASS first. *) |
202 timeout, it makes sense to put SPASS first. *) |
203 fun default_provers_param_value ctxt = |
203 fun default_provers_param_value ctxt = |
204 [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN] |
204 [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, waldmeisterN] |
205 |> map_filter (remotify_prover_if_not_installed ctxt) |
205 |> map_filter (remotify_prover_if_not_installed ctxt) |
206 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
206 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
207 max_default_remote_threads) |
207 max_default_remote_threads) |
208 |> implode_param |
208 |> implode_param |
209 |
209 |