192 |> map (apsnd single) |
192 |> map (apsnd single) |
193 val extend = I |
193 val extend = I |
194 fun merge data : T = AList.merge (op =) (K true) data |
194 fun merge data : T = AList.merge (op =) (K true) data |
195 ) |
195 ) |
196 |
196 |
197 fun avoid_too_many_threads _ _ [] = [] |
|
198 | avoid_too_many_threads _ (0, 0) _ = [] |
|
199 | avoid_too_many_threads ctxt (0, max_remote) provers = |
|
200 provers |
|
201 |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt) |
|
202 |> take max_remote |
|
203 | avoid_too_many_threads _ (max_local, 0) provers = |
|
204 provers |
|
205 |> filter_out (String.isPrefix remote_prefix) |
|
206 |> take max_local |
|
207 | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) = |
|
208 let |
|
209 val max_local_and_remote = |
|
210 max_local_and_remote |
|
211 |> (if String.isPrefix remote_prefix prover then apsnd else apfst) |
|
212 (Integer.add ~1) |
|
213 in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end |
|
214 |
|
215 val max_default_remote_threads = 4 |
|
216 |
|
217 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
197 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
218 timeout, it makes sense to put E first. *) |
198 timeout, it makes sense to put E first. *) |
219 fun default_provers_param_value ctxt = |
199 fun default_provers_param_value ctxt = |
220 [eN, spassN, vampireN, z3N, e_sineN, yicesN] |
200 [eN, spassN, vampireN, z3N, e_sineN, yicesN] |
221 |> map_filter (remotify_prover_if_not_installed ctxt) |
201 |> map_filter (remotify_prover_if_not_installed ctxt) |
222 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
202 |> take (Multithreading.max_threads_value ()) |
223 max_default_remote_threads) |
|
224 |> implode_param |
203 |> implode_param |
225 |
204 |
226 fun set_default_raw_param param thy = |
205 fun set_default_raw_param param thy = |
227 let val ctxt = Proof_Context.init_global thy in |
206 let val ctxt = Proof_Context.init_global thy in |
228 thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) |
207 thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) |