equal
deleted
inserted
replaced
208 val max_default_remote_threads = 4 |
208 val max_default_remote_threads = 4 |
209 |
209 |
210 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
210 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
211 timeout, it makes sense to put SPASS first. *) |
211 timeout, it makes sense to put SPASS first. *) |
212 fun default_provers_param_value ctxt = |
212 fun default_provers_param_value ctxt = |
213 [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN] |
213 [spassN, spass_newN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, |
|
214 waldmeisterN] |
214 |> map_filter (remotify_prover_if_not_installed ctxt) |
215 |> map_filter (remotify_prover_if_not_installed ctxt) |
215 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
216 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
216 max_default_remote_threads) |
217 max_default_remote_threads) |
217 |> implode_param |
218 |> implode_param |
218 |
219 |