equal
deleted
inserted
replaced
26 open Sledgehammer_Fact |
26 open Sledgehammer_Fact |
27 open Sledgehammer_Provers |
27 open Sledgehammer_Provers |
28 open Sledgehammer_Minimize |
28 open Sledgehammer_Minimize |
29 open Sledgehammer_MaSh |
29 open Sledgehammer_MaSh |
30 open Sledgehammer_Run |
30 open Sledgehammer_Run |
|
31 |
|
32 val cvc3N = "cvc3" |
|
33 val yicesN = "yices" |
|
34 val z3N = "z3" |
31 |
35 |
32 val runN = "run" |
36 val runN = "run" |
33 val minN = "min" |
37 val minN = "min" |
34 val messagesN = "messages" |
38 val messagesN = "messages" |
35 val supported_proversN = "supported_provers" |
39 val supported_proversN = "supported_provers" |
218 in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end |
222 in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end |
219 |
223 |
220 val max_default_remote_threads = 4 |
224 val max_default_remote_threads = 4 |
221 |
225 |
222 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
226 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low |
223 timeout, it makes sense to put SPASS first. *) |
227 timeout, it makes sense to put E first. *) |
224 fun default_provers_param_value ctxt = |
228 fun default_provers_param_value ctxt = |
225 [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, |
229 [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N] |
226 waldmeisterN] |
|
227 |> map_filter (remotify_prover_if_not_installed ctxt) |
230 |> map_filter (remotify_prover_if_not_installed ctxt) |
228 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
231 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), |
229 max_default_remote_threads) |
232 max_default_remote_threads) |
230 |> implode_param |
233 |> implode_param |
231 |
234 |