src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
changeset 74369 3301c0d8b560
parent 74352 fb8ce6090437
child 74370 d8dc8fdc46fc
equal deleted inserted replaced
74368:ac90d6c6c149 74369:3301c0d8b560
   175   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
   175   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
   176   else remotify_prover_if_supported_and_not_already_remote ctxt name
   176   else remotify_prover_if_supported_and_not_already_remote ctxt name
   177 
   177 
   178 (* The first ATP of the list is used by Auto Sledgehammer. *)
   178 (* The first ATP of the list is used by Auto Sledgehammer. *)
   179 fun default_provers_param_value mode ctxt =
   179 fun default_provers_param_value mode ctxt =
   180   [cvc4N, vampireN, z3N, eN, spassN, veritN]
   180   [cvc4N, vampireN, z3N, eN, spassN, veritN, zipperpositionN]
   181   |> map_filter (remotify_prover_if_not_installed ctxt)
   181   |> map_filter (remotify_prover_if_not_installed ctxt)
   182   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   182   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   183   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
   183   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
   184   |> implode_param
   184   |> implode_param
   185 
   185