# HG changeset patch
# User blanchet
# Date 1287756703 -7200
# Node ID 27f2a45b0aab731961f0b9218a8fb7b9e186e0d7
# Parent  658a37c80b5308b2d132d434d8a03cb90dc9122c
more robust handling of "remote_" vs. non-"remote_" provers

diff -r 658a37c80b53 -r 27f2a45b0aab src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 15:02:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 16:11:43 2010 +0200
@@ -51,6 +51,8 @@
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
   val smtN : string
+  val is_prover_available : theory -> string -> bool
+  val is_prover_installed : Proof.context -> string -> bool
   val default_max_relevant_for_prover : theory -> string -> int
   val irrelevant_consts_for_prover : string -> string list
   val relevance_fudge_for_prover : string -> relevance_fudge
@@ -92,7 +94,16 @@
 
 val is_smt_prover = member (op =) smt_prover_names
 
-val smt_default_max_relevant = 300 (* FUDGE *)
+fun is_prover_available thy name =
+  is_smt_prover name orelse member (op =) (available_atps thy) name
+
+fun is_prover_installed ctxt name =
+  let val thy = ProofContext.theory_of ctxt in
+    if is_smt_prover name then true (* FIXME *)
+    else is_atp_installed thy name
+  end
+
+val smt_default_max_relevant = 300 (* FUDGE (FIXME) *)
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
 fun default_max_relevant_for_prover thy name =
diff -r 658a37c80b53 -r 27f2a45b0aab src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 15:02:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 16:11:43 2010 +0200
@@ -133,21 +133,37 @@
 (* FIXME: dummy *)
 fun is_smt_solver_installed ctxt = true
 
-fun maybe_remote_atp thy name =
-  name |> not (is_atp_installed thy name) ? prefix remote_prefix
-fun maybe_remote_smt_solver ctxt =
-  smtN |> not (is_smt_solver_installed ctxt) ? prefix remote_prefix
+fun remotify_prover_if_available_and_not_already_remote thy 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
+    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
+
+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) =
+    let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
+      prover :: avoid_too_many_local_threads thy 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
-    (filter (is_atp_installed thy) [spassN] @
-     [maybe_remote_atp thy eN,
-      if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
-      else maybe_remote_atp thy vampireN,
-      remote_prefix ^ sine_eN (* FIXME: Introduce and document: ,
-      maybe_remote_smt_solver ctxt *)])
+    [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)]
+    |> map_filter (remotify_prover_if_not_installed ctxt)
+    |> avoid_too_many_local_threads thy (Thread.numProcessors ())
     |> space_implode " "
   end