1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -143,6 +143,12 @@
     1.4                              | _ => value)
     1.5      | NONE => (name, value)
     1.6  
     1.7 +(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
     1.8 +   correctly. *)
     1.9 +fun implode_param [s, "?"] = s ^ "?"
    1.10 +  | implode_param [s, "!"] = s ^ "!"
    1.11 +  | implode_param ss = space_implode " " ss
    1.12 +
    1.13  structure Data = Theory_Data
    1.14  (
    1.15    type T = raw_param list
    1.16 @@ -165,27 +171,33 @@
    1.17    else
    1.18      remotify_prover_if_supported_and_not_already_remote ctxt name
    1.19  
    1.20 -fun avoid_too_many_local_threads _ _ [] = []
    1.21 -  | avoid_too_many_local_threads ctxt 0 provers =
    1.22 -    map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
    1.23 -               provers
    1.24 -  | avoid_too_many_local_threads ctxt n (prover :: provers) =
    1.25 -    let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
    1.26 -      prover :: avoid_too_many_local_threads ctxt n provers
    1.27 -    end
    1.28 +fun avoid_too_many_threads _ _ [] = []
    1.29 +  | avoid_too_many_threads _ (0, 0) _ = []
    1.30 +  | avoid_too_many_threads ctxt (0, max_remote) provers =
    1.31 +    provers
    1.32 +    |> map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
    1.33 +    |> take max_remote
    1.34 +  | avoid_too_many_threads _ (max_local, 0) provers =
    1.35 +    provers
    1.36 +    |> filter_out (String.isPrefix remote_prefix)
    1.37 +    |> take max_local
    1.38 +  | avoid_too_many_threads ctxt max_local_and_remote (prover :: provers) =
    1.39 +    let
    1.40 +      val max_local_and_remote =
    1.41 +        max_local_and_remote
    1.42 +        |> (if String.isPrefix remote_prefix prover then apsnd else apfst)
    1.43 +              (Integer.add ~1)
    1.44 +    in prover :: avoid_too_many_threads ctxt max_local_and_remote provers end
    1.45  
    1.46 -(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
    1.47 -   correctly. *)
    1.48 -fun implode_param [s, "?"] = s ^ "?"
    1.49 -  | implode_param [s, "!"] = s ^ "!"
    1.50 -  | implode_param ss = space_implode " " ss
    1.51 +val max_default_remote_threads = 4
    1.52  
    1.53  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    1.54     timeout, it makes sense to put SPASS first. *)
    1.55  fun default_provers_param_value ctxt =
    1.56 -  [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
    1.57 +  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
    1.58    |> map_filter (remotify_prover_if_not_installed ctxt)
    1.59 -  |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
    1.60 +  |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    1.61 +                                  max_default_remote_threads)
    1.62    |> implode_param
    1.63  
    1.64  val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param