141 | ["true"] => ["false"] |
141 | ["true"] => ["false"] |
142 | [] => ["false"] |
142 | [] => ["false"] |
143 | _ => value) |
143 | _ => value) |
144 | NONE => (name, value) |
144 | NONE => (name, value) |
145 |
145 |
|
146 (* Ensure that type systems such as "simple!" and "mangled_preds?" are handled |
|
147 correctly. *) |
|
148 fun implode_param [s, "?"] = s ^ "?" |
|
149 | implode_param [s, "!"] = s ^ "!" |
|
150 | implode_param ss = space_implode " " ss |
|
151 |
146 structure Data = Theory_Data |
152 structure Data = Theory_Data |
147 ( |
153 ( |
148 type T = raw_param list |
154 type T = raw_param list |
149 val empty = default_default_params |> map (apsnd single) |
155 val empty = default_default_params |> map (apsnd single) |
150 val extend = I |
156 val extend = I |
163 if is_prover_supported ctxt name andalso is_prover_installed ctxt name then |
169 if is_prover_supported ctxt name andalso is_prover_installed ctxt name then |
164 SOME name |
170 SOME name |
165 else |
171 else |
166 remotify_prover_if_supported_and_not_already_remote ctxt name |
172 remotify_prover_if_supported_and_not_already_remote ctxt name |
167 |
173 |
168 fun avoid_too_many_local_threads _ _ [] = [] |
174 fun avoid_too_many_threads _ _ [] = [] |
169 | avoid_too_many_local_threads ctxt 0 provers = |
175 | avoid_too_many_threads _ (0, 0) _ = [] |
170 map_filter (remotify_prover_if_supported_and_not_already_remote ctxt) |
176 | avoid_too_many_threads ctxt (0, max_remote) provers = |
171 provers |
177 provers |
172 | avoid_too_many_local_threads ctxt n (prover :: provers) = |
178 |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt) |
173 let val n = if String.isPrefix remote_prefix prover then n else n - 1 in |
179 |> take max_remote |
174 prover :: avoid_too_many_local_threads ctxt n provers |
180 | avoid_too_many_threads _ (max_local, 0) provers = |
175 end |
181 provers |
176 |
182 |> filter_out (String.isPrefix remote_prefix) |
177 (* Ensure that type systems such as "simple!" and "mangled_preds?" are handled |
183 |> take max_local |
178 correctly. *) |
184 | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) = |
179 fun implode_param [s, "?"] = s ^ "?" |
185 let |
180 | implode_param [s, "!"] = s ^ "!" |
186 val max_local_and_remote = |
181 | implode_param ss = space_implode " " ss |
187 max_local_and_remote |
|
188 |> (if String.isPrefix remote_prefix prover then apsnd else apfst) |
|
189 (Integer.add ~1) |
|
190 in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end |
|
191 |
|
192 val max_default_remote_threads = 4 |
182 |
193 |
183 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
194 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
184 timeout, it makes sense to put SPASS first. *) |
195 timeout, it makes sense to put SPASS first. *) |
185 fun default_provers_param_value ctxt = |
196 fun default_provers_param_value ctxt = |
186 [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt] |
197 [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN] |
187 |> map_filter (remotify_prover_if_not_installed ctxt) |
198 |> map_filter (remotify_prover_if_not_installed ctxt) |
188 |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ()) |
199 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
|
200 max_default_remote_threads) |
189 |> implode_param |
201 |> implode_param |
190 |
202 |
191 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param |
203 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param |
192 fun default_raw_params ctxt = |
204 fun default_raw_params ctxt = |
193 let val thy = Proof_Context.theory_of ctxt in |
205 let val thy = Proof_Context.theory_of ctxt in |