src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
changeset 59962 b622365f181c
parent 59936 b8ffc3dc9e24
child 60094 96a4765ba7d1
equal deleted inserted replaced
59961:a965060dcbb8 59962:b622365f181c
   179   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
   179   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
   180   else remotify_prover_if_supported_and_not_already_remote ctxt name
   180   else remotify_prover_if_supported_and_not_already_remote ctxt name
   181 
   181 
   182 (* The first ATP of the list is used by Auto Sledgehammer. *)
   182 (* The first ATP of the list is used by Auto Sledgehammer. *)
   183 fun default_provers_param_value mode ctxt =
   183 fun default_provers_param_value mode ctxt =
   184   [spassN, cvc4N, vampireN, eN, z3N, veritN, e_sineN]
   184   [cvc4N, vampireN, z3N, spassN, eN, veritN, e_sineN]
   185   |> map_filter (remotify_prover_if_not_installed ctxt)
   185   |> map_filter (remotify_prover_if_not_installed ctxt)
   186   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   186   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   187   |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
   187   |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
   188   |> implode_param
   188   |> implode_param
   189 
   189