deal with ATP time slices in a more flexible/robust fashion

--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 20 09:19:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -49,8 +49,8 @@
   val extract_known_failure :
     (failure * string) list -> string -> failure option
   val extract_tstplike_proof_and_outcome :
-    bool -> bool -> int -> (string * string) list -> (failure * string) list
-    -> string -> string * failure option
+    bool -> bool -> (string * string) list -> (failure * string) list -> string
+    -> string * failure option
   val is_same_atp_step : step_name -> step_name -> bool
   val scan_general_id : string list -> string * string list
   val parse_formula :
@@ -194,7 +194,7 @@
   |> find_first (fn (_, pattern) => String.isSubstring pattern output)
   |> Option.map fst
 
-fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
+fun extract_tstplike_proof_and_outcome verbose complete proof_delims
                                        known_failures output =
   case (extract_tstplike_proof proof_delims output,
         extract_known_failure known_failures output) of

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 09:19:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -15,14 +15,15 @@
     {exec : string * string,
      required_execs : (string * string) list,
      arguments :
-       Proof.context -> bool -> int -> Time.time
+       Proof.context -> bool -> string -> Time.time
        -> (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      formats : format list,
-     best_slices : Proof.context -> (real * (bool * (int * string list))) list}
+     best_slices :
+       Proof.context -> (real * (bool * (int * string list * string))) list}
 
   val e_weight_method : string Config.T
   val e_default_fun_weight : real Config.T
@@ -68,14 +69,15 @@
   {exec : string * string,
    required_execs : (string * string) list,
    arguments :
-     Proof.context -> bool -> int -> Time.time -> (unit -> (string * real) list)
-     -> string,
+     Proof.context -> bool -> string -> Time.time
+     -> (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
    formats : format list,
-   best_slices : Proof.context -> (real * (bool * (int * string list))) list}
+   best_slices :
+     Proof.context -> (real * (bool * (int * string list * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" components give the faction of the
@@ -119,6 +121,9 @@
 
 fun to_secs time = (Time.toMilliseconds time + 999) div 1000
 
+val sosN = "sos"
+val no_sosN = "no_sos"
+
 
 (* E *)
 
@@ -126,13 +131,13 @@
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
 
-val e_slicesN = "slices"
+val e_smartN = "smart"
 val e_autoN = "auto"
 val e_fun_weightN = "fun_weight"
 val e_sym_offset_weightN = "sym_offset_weight"
 
 val e_weight_method =
-  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN)
+  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
 (* FUDGE *)
 val e_default_fun_weight =
   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
@@ -184,26 +189,12 @@
 fun effective_e_weight_method ctxt =
   if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
 
-(* The order here must correspond to the order in "e_config" below. *)
-fun method_for_slice ctxt slice =
-  let val method = effective_e_weight_method ctxt in
-    if method = e_slicesN then
-      case slice of
-        0 => e_sym_offset_weightN
-      | 1 => e_autoN
-      | 2 => e_fun_weightN
-      | _ => raise Fail "no such slice"
-    else
-      method
-  end
-
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments =
-     fn ctxt => fn full_proof => fn slice => fn timeout => fn weights =>
-        "--tstp-in --tstp-out -l5 " ^
-        e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
+     fn ctxt => fn full_proof => fn method => fn timeout => fn weights =>
+        "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
         (if full_proof orelse is_old_e_version () then "" else " --trim"),
    proof_delims = tstp_proof_delims,
@@ -221,13 +212,15 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     if effective_e_weight_method ctxt = e_slicesN then
-       [(0.333, (true, (100, ["mangled_preds_heavy"]))) (* sym_offset_weight *),
-        (0.333, (true, (800, ["poly_preds?"]))) (* auto *),
-        (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
-                                                               (* fun_weight *)]
-     else
-       [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]}
+     let val method = effective_e_weight_method ctxt in
+       if method = e_smartN then
+         [(0.333, (true, (100, ["mangled_preds_heavy"], e_sym_offset_weightN))),
+          (0.333, (true, (800, ["poly_preds?"], e_autoN))),
+          (0.334, (true,
+             (200, ["mangled_tags!", "mangled_tags?"], e_fun_weightN)))]
+       else
+         [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"], method)))]
+     end}
 
 val e = (eN, e_config)
 
@@ -242,10 +235,10 @@
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
-     |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
+     |> sos = sosN ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
@@ -261,9 +254,9 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *),
-      (0.333, (false, (150, ["mangled_preds?"]))) (* SOS *),
-      (0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)]
+     [(0.333, (false, (150, ["mangled_preds_heavy"], sosN))),
+      (0.333, (false, (150, ["mangled_preds?"], sosN))),
+      (0.334, (true, (150, ["poly_preds"], no_sosN)))]
      |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -278,11 +271,10 @@
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
+   arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
      "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
-     |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
-        ? prefix "--sos on ",
+     |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
        "======= End of refutation ======="),
@@ -303,9 +295,9 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *),
-      (0.333, (false, (300, ["mangled_tags?"]))) (* SOS *),
-      (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
+     [(0.333, (false, (200, ["mangled_preds_heavy"], sosN))),
+      (0.333, (false, (300, ["mangled_tags?"], sosN))),
+      (0.334, (true, (400, ["poly_preds"], no_sosN)))]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -331,7 +323,7 @@
    formats = [FOF],
    best_slices =
      (* FUDGE (FIXME) *)
-     K [(1.0, (false, (250, [])))]}
+     K [(1.0, (false, (250, [], "")))]}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
@@ -390,14 +382,19 @@
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    formats = formats,
-   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
+   best_slices = fn ctxt =>
+     let val (max_relevant, type_syss) = best_slice ctxt in
+       [(1.0, (false, (max_relevant, type_syss, "")))]
+     end}
 
 fun remotify_config system_name system_versions
         ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
           best_slices, ...} : atp_config) : atp_config =
   remote_config system_name system_versions proof_delims known_failures
                 conj_sym_kind prem_kind formats
-                (best_slices #> List.last #> snd #> snd)
+                (best_slices #> List.last #> snd #> snd
+                 #> (fn (max_relevant, type_syss, _) =>
+                        (max_relevant, type_syss)))
 
 fun remote_atp name system_name system_versions proof_delims known_failures
         conj_sym_kind prem_kind formats best_slice =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 20 09:19:31 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -178,7 +178,7 @@
     if is_metis_prover name then
       metis_default_max_relevant
     else if is_atp thy name then
-      fold (Integer.max o fst o snd o snd o snd)
+      fold (Integer.max o #1 o snd o snd o snd)
            (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
     else (* is_smt_prover ctxt name *)
       SMT_Solver.default_max_relevant ctxt name
@@ -511,14 +511,14 @@
    them each time. *)
 val atp_important_message_keep_quotient = 10
 
-val fallback_best_type_systems =
+val fallback_best_type_syss =
   [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)]
 
 fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     choose_format formats type_sys
-  | choose_format_and_type_sys best_type_systems formats
+  | choose_format_and_type_sys best_type_syss formats
                                (Smart_Type_Sys full_types) =
-    map type_sys_from_string best_type_systems @ fallback_best_type_systems
+    map type_sys_from_string best_type_syss @ fallback_best_type_syss
     |> find_first (if full_types then is_type_sys_virtually_sound else K true)
     |> the |> choose_format formats
 
@@ -610,14 +610,14 @@
                 |> maps (fn (name, rths) => map (pair name o snd) rths)
               end
             fun run_slice blacklist (slice, (time_frac, (complete,
-                                       (best_max_relevant, best_type_systems))))
+                                   (best_max_relevant, best_type_syss, extra))))
                           time_left =
               let
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
                 val (format, type_sys) =
-                  choose_format_and_type_sys best_type_systems formats type_sys
+                  choose_format_and_type_sys best_type_syss formats type_sys
                 val fairly_sound = is_type_sys_fairly_sound type_sys
                 val facts =
                   facts |> map untranslated_fact
@@ -655,7 +655,7 @@
                 val full_proof = debug orelse isar_proof
                 val core =
                   File.shell_path command ^ " " ^
-                  arguments ctxt full_proof slice slice_timeout weights ^ " " ^
+                  arguments ctxt full_proof extra slice_timeout weights ^ " " ^
                   File.shell_path prob_file
                 val command =
                   (if measure_run_time then
@@ -671,7 +671,7 @@
                   conjecture_offset + 1
                     upto conjecture_offset + length hyp_ts + 1
                   |> map single
-                val ((output, msecs), res_code) =
+                val ((output, msecs), _) =
                   bash_output command
                   |>> (if overlord then
                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
@@ -679,7 +679,7 @@
                          I)
                   |>> (if measure_run_time then split_time else rpair NONE)
                 val (atp_proof, outcome) =
-                  extract_tstplike_proof_and_outcome verbose complete res_code
+                  extract_tstplike_proof_and_outcome verbose complete
                       proof_delims known_failures output
                   |>> atp_proof_from_tstplike_proof atp_problem
                   handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)