replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -316,11 +316,10 @@
 
 fun get_prover ctxt args =
   let
-    val thy = ProofContext.theory_of ctxt
     fun default_prover_name () =
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
       handle Empty => error "No ATP available."
-    fun get_prover name = (name, Sledgehammer.get_prover thy false name)
+    fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
@@ -356,10 +355,11 @@
           [("verbose", "true"),
            ("timeout", Int.toString timeout)]
     val default_max_relevant =
-      Sledgehammer.default_max_relevant_for_prover thy prover_name
+      Sledgehammer.default_max_relevant_for_prover ctxt prover_name
     val is_built_in_const =
       Sledgehammer.is_built_in_const_for_prover ctxt prover_name
-    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
+    val relevance_fudge =
+      Sledgehammer.relevance_fudge_for_prover ctxt prover_name
     val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     val facts =

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -106,16 +106,15 @@
        SOME proofs =>
        let
          val {context = ctxt, facts, goal} = Proof.goal pre
-         val thy = ProofContext.theory_of ctxt
          val prover = AList.lookup (op =) args "prover"
                       |> the_default default_prover
          val default_max_relevant =
-           Sledgehammer.default_max_relevant_for_prover thy prover
+           Sledgehammer.default_max_relevant_for_prover ctxt prover
         val is_built_in_const =
           Sledgehammer.is_built_in_const_for_prover ctxt default_prover
          val relevance_fudge =
            extract_relevance_fudge args
-               (Sledgehammer.relevance_fudge_for_prover prover)
+               (Sledgehammer.relevance_fudge_for_prover ctxt prover)
          val relevance_override = {add = [], del = [], only = false}
          val {relevance_thresholds, full_types, max_relevant, ...} =
            Sledgehammer_Isar.default_params ctxt args

--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -16,19 +16,18 @@
   
 fun run_atp force_full_types timeout i n ctxt goal name =
   let
-    val thy = ProofContext.theory_of ctxt
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {full_types, relevance_thresholds, max_relevant, ...} =
       ((if force_full_types then [("full_types", "true")] else [])
        @ [("timeout", Int.toString (Time.toSeconds timeout))])
        @ [("overlord", "true")]
       |> Sledgehammer_Isar.default_params ctxt
-    val prover = Sledgehammer.get_prover thy false name
+    val prover = Sledgehammer.get_prover ctxt false name
     val default_max_relevant =
-      Sledgehammer.default_max_relevant_for_prover thy name
+      Sledgehammer.default_max_relevant_for_prover ctxt name
     val is_built_in_const =
       Sledgehammer.is_built_in_const_for_prover ctxt name
-    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover name
+    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover ctxt name
     val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     val facts =
@@ -75,7 +74,6 @@
 
 fun sledgehammer_with_metis_tac ctxt i th =
   let
-    val thy = ProofContext.theory_of ctxt
     val timeout = Time.fromSeconds 30
   in
     case run_atp false timeout i i ctxt th atp of

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -50,21 +50,20 @@
 
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
-  val smtN : string
-  val is_prover_available : theory -> string -> bool
+  val is_prover_available : Proof.context -> string -> bool
   val is_prover_installed : Proof.context -> string -> bool
-  val default_max_relevant_for_prover : theory -> string -> int
+  val default_max_relevant_for_prover : Proof.context -> string -> int
   val is_built_in_const_for_prover :
     Proof.context -> string -> string * typ -> bool
-  val relevance_fudge_for_prover : string -> relevance_fudge
+  val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
-  val available_provers : theory -> unit
+  val available_provers : Proof.context -> unit
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val get_prover : theory -> bool -> string -> prover
+  val get_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
@@ -90,27 +89,43 @@
    "Async_Manager". *)
 val das_Tool = "Sledgehammer"
 
-val smtN = "smt"
-val smt_prover_names = [smtN, remote_prefix ^ smtN]
+fun is_smt_prover ctxt name =
+  let val smts = SMT_Solver.available_solvers_of ctxt in
+    case try (unprefix remote_prefix) name of
+      SOME suffix => member (op =) smts suffix andalso
+                     SMT_Solver.is_remotely_available ctxt suffix
+    | NONE => member (op =) smts name
+  end
 
-val is_smt_prover = member (op =) smt_prover_names
-
-fun is_prover_available thy name =
-  is_smt_prover name orelse member (op =) (available_atps thy) name
+fun is_prover_available ctxt name =
+  let val thy = ProofContext.theory_of ctxt in
+    is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
+  end
 
 fun is_prover_installed ctxt name =
   let val thy = ProofContext.theory_of ctxt in
-    if is_smt_prover name then SMT_Solver.is_locally_installed ctxt
-    else is_atp_installed thy name
+    if is_smt_prover ctxt name then
+      String.isPrefix remote_prefix name orelse
+      SMT_Solver.is_locally_installed ctxt name
+    else
+      is_atp_installed thy name
+  end
+
+fun available_smt_solvers ctxt =
+  let val smts = SMT_Solver.available_solvers_of ctxt in
+    smts @ map (prefix remote_prefix)
+               (filter (SMT_Solver.is_remotely_available ctxt) smts)
   end
 
 (* FUDGE *)
 val smt_default_max_relevant = 225
 val auto_max_relevant_divisor = 2
 
-fun default_max_relevant_for_prover thy name =
-  if is_smt_prover name then smt_default_max_relevant
-  else #default_max_relevant (get_atp thy name)
+fun default_max_relevant_for_prover ctxt name =
+  let val thy = ProofContext.theory_of ctxt in
+    if is_smt_prover ctxt name then smt_default_max_relevant
+    else #default_max_relevant (get_atp thy name)
+  end
 
 (* These are typically simplified away by "Meson.presimplify". Equality is
    handled specially via "fequal". *)
@@ -119,7 +134,7 @@
    @{const_name HOL.eq}]
 
 fun is_built_in_const_for_prover ctxt name (s, T) =
-  if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T)
+  if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
   else member (op =) atp_irrelevant_consts s
 
 (* FUDGE *)
@@ -162,13 +177,15 @@
    threshold_divisor = #threshold_divisor atp_relevance_fudge,
    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
 
-fun relevance_fudge_for_prover name =
-  if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
+fun relevance_fudge_for_prover ctxt name =
+  if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
 
-fun available_provers thy =
+fun available_provers ctxt =
   let
+    val thy = ProofContext.theory_of ctxt
     val (remote_provers, local_provers) =
-      sort_strings (available_atps thy) @ smt_prover_names
+      sort_strings (available_atps thy) @
+      sort_strings (available_smt_solvers ctxt)
       |> List.partition (String.isPrefix remote_prefix)
   in
     Output.urgent_message ("Available provers: " ^
@@ -523,11 +540,16 @@
             (Config.put Metis_Tactics.verbose debug
              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
-fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
+fun run_smt_solver auto name (params as {debug, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
+    val (remote, suffix) =
+      case try (unprefix remote_prefix) name of
+        SOME suffix => (true, suffix)
+      | NONE => (false, name)
     val repair_context =
-      Config.put SMT_Config.verbose debug
+      Context.proof_map (SMT_Config.select_solver suffix)
+      #> Config.put SMT_Config.verbose debug
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
     val thy = Proof.theory_of state
@@ -558,30 +580,34 @@
      run_time_in_msecs = run_time_in_msecs, message = message}
   end
 
-fun get_prover thy auto name =
-  if is_smt_prover name then
-    run_smt_solver auto (String.isPrefix remote_prefix name)
-  else
-    run_atp auto name (get_atp thy name)
+fun get_prover ctxt auto name =
+  let val thy = ProofContext.theory_of ctxt in
+    if is_smt_prover ctxt name then
+      run_smt_solver auto name
+    else if member (op =) (available_atps thy) name then
+      run_atp auto name (get_atp thy name)
+    else
+      error ("No such prover: " ^ name ^ ".")
+  end
 
 fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
                auto minimize_command
                (problem as {state, goal, subgoal, subgoal_count, facts, ...})
                name =
   let
-    val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val max_relevant =
-      the_default (default_max_relevant_for_prover thy name) max_relevant
+      the_default (default_max_relevant_for_prover ctxt name) max_relevant
     val num_facts = Int.min (length facts, max_relevant)
     val desc =
       prover_description ctxt params name num_facts subgoal subgoal_count goal
+    val prover = get_prover ctxt auto name
     fun go () =
       let
         fun really_go () =
-          get_prover thy auto name params (minimize_command name) problem
+          prover params (minimize_command name) problem
           |> (fn {outcome, message, ...} =>
                  (if is_some outcome then "none" else "some", message))
         val (outcome_code, message) =
@@ -629,13 +655,15 @@
   | n =>
     let
       val _ = Proof.assert_backward state
-      val thy = Proof.theory_of state
       val ctxt = Proof.context_of state
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val _ = () |> not blocking ? kill_provers
+      val _ = case find_first (not o is_prover_available ctxt) provers of
+                SOME name => error ("No such prover: " ^ name ^ ".")
+              | NONE => ()
       val _ = if auto then () else Output.urgent_message "Sledgehammering..."
-      val (smts, atps) = provers |> List.partition is_smt_prover
+      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
       fun run_provers label full_types relevance_fudge maybe_translate provers
                       (res as (success, state)) =
         if success orelse null provers then
@@ -646,7 +674,7 @@
               case max_relevant of
                 SOME n => n
               | NONE =>
-                0 |> fold (Integer.max o default_max_relevant_for_prover thy)
+                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
                           provers
                   |> auto ? (fn n => n div auto_max_relevant_divisor)
             val is_built_in_const =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -130,39 +130,36 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-fun remotify_prover_if_available_and_not_already_remote thy name =
+fun remotify_prover_if_available_and_not_already_remote ctxt name =
   if String.isPrefix remote_prefix name then
     SOME name
   else
     let val remote_name = remote_prefix ^ name in
-      if is_prover_available thy remote_name then SOME remote_name else NONE
+      if is_prover_available ctxt remote_name then SOME remote_name else NONE
     end
 
 fun remotify_prover_if_not_installed ctxt name =
-  let val thy = ProofContext.theory_of ctxt in
-    if is_prover_available thy name andalso is_prover_installed ctxt name then
-      SOME name
-    else
-      remotify_prover_if_available_and_not_already_remote thy name
-  end
+  if is_prover_available ctxt name andalso is_prover_installed ctxt name then
+    SOME name
+  else
+    remotify_prover_if_available_and_not_already_remote ctxt name
 
 fun avoid_too_many_local_threads _ _ [] = []
-  | avoid_too_many_local_threads thy 0 provers =
-    map_filter (remotify_prover_if_available_and_not_already_remote thy) provers
-  | avoid_too_many_local_threads thy n (prover :: provers) =
+  | avoid_too_many_local_threads ctxt 0 provers =
+    map_filter (remotify_prover_if_available_and_not_already_remote ctxt)
+               provers
+  | avoid_too_many_local_threads ctxt n (prover :: provers) =
     let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
-      prover :: avoid_too_many_local_threads thy n provers
+      prover :: avoid_too_many_local_threads ctxt n provers
     end
 
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value ctxt =
-  let val thy = ProofContext.theory_of ctxt in
-    [spassN, eN, vampireN, sine_eN, smtN]
-    |> map_filter (remotify_prover_if_not_installed ctxt)
-    |> avoid_too_many_local_threads thy (Multithreading.max_threads_value ())
-    |> space_implode " "
-  end
+  [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
+  |> map_filter (remotify_prover_if_not_installed ctxt)
+  |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
+  |> space_implode " "
 
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params ctxt =
@@ -270,7 +267,6 @@
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val ctxt = Proof.context_of state
-    val thy = Proof.theory_of state
     val _ = app check_raw_param override_params
   in
     if subcommand = runN then
@@ -286,7 +282,7 @@
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_proversN then
-      available_provers thy
+      available_provers ctxt
     else if subcommand = running_proversN then
       running_provers ()
     else if subcommand = kill_proversN then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 03 18:27:21 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 03 18:29:14 2010 +0100
@@ -92,7 +92,8 @@
                    state facts =
   let
     val thy = Proof.theory_of state
-    val prover = get_prover thy false prover_name
+    val ctxt = Proof.context_of state
+    val prover = get_prover ctxt false prover_name
     val msecs = Time.toMilliseconds timeout
     val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
     val {goal, ...} = Proof.goal state