killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 28 20:25:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 28 20:45:28 2012 +0200
@@ -2759,8 +2759,7 @@
       0 upto length helpers - 1 ~~ helpers
       |> map (formula_line_for_fact ctxt polym_constrs helper_prefix I false
                                     true mono type_enc (K default_rank))
-    (* Reordering these might confuse the proof reconstruction code or the SPASS
-       FLOTTER hack. *)
+    (* Reordering these might confuse the proof reconstruction code. *)
     val problem =
       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
        (uncurried_alias_eqsN, uncurried_alias_eq_lines),

--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 28 20:25:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 28 20:45:28 2012 +0200
@@ -452,30 +452,20 @@
      -- Scan.repeat parse_decorated_atom
    >> (mk_horn o apfst (op @))) x
 
-fun resolve_spass_num (SOME names) _ _ = names
-  | resolve_spass_num NONE spass_names num =
-    case Int.fromString num of
-      SOME j => if j > 0 andalso j <= Vector.length spass_names then
-                  Vector.sub (spass_names, j - 1)
-                else
-                  []
-    | NONE => []
-
 val parse_spass_debug =
   Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
                --| $$ ")")
 
 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
            derived from formulae <ident>* *)
-fun parse_spass_line spass_names =
-  parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
-    -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
-    -- parse_horn_clause --| $$ "."
-    -- Scan.option (Scan.this_string "derived from formulae "
-                    |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
-  >> (fn ((((num, rule), deps), u), names) =>
-         Inference_Step ((num, resolve_spass_num names spass_names num), u,
-             rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
+fun parse_spass_line x =
+  (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
+     -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
+     -- parse_horn_clause --| $$ "."
+     -- Scan.option (Scan.this_string "derived from formulae "
+                     |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
+   >> (fn ((((num, rule), deps), u), names) =>
+          Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x
 
 val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
 
@@ -485,62 +475,20 @@
    >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
       x
 
-fun parse_line problem spass_names =
-  parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
-fun parse_proof problem spass_names tstp =
+fun parse_line problem =
+  parse_tstp_line problem || parse_spass_line || parse_satallax_line
+fun parse_proof problem tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode
        |> Scan.finite Symbol.stopper
               (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-                              (Scan.repeat1 (parse_line problem spass_names))))
+                              (Scan.repeat1 (parse_line problem))))
        |> fst
 
-(** SPASS's FLOTTER hack **)
-
-(* This is a hack required for keeping track of facts after they have been
-   clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is
-   also part of this hack. *)
-
-val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
-
-fun extract_clause_sequence output =
-  let
-    val tokens_of = String.tokens (not o Char.isAlphaNum)
-    fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
-      | extract_num _ = NONE
-  in output |> split_lines |> map_filter (extract_num o tokens_of) end
-
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
-val parse_clause_formula_pair =
-  $$ "(" |-- scan_integer --| $$ ","
-  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
-  --| Scan.option ($$ ",")
-val parse_clause_formula_relation =
-  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
-  |-- Scan.repeat parse_clause_formula_pair
-val extract_clause_formula_relation =
-  Substring.full #> Substring.position set_ClauseFormulaRelationN
-  #> snd #> Substring.position "." #> fst #> Substring.string
-  #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
-  #> fst
-
-fun extract_spass_name_vector output =
-  (if String.isSubstring set_ClauseFormulaRelationN output then
-     let
-       val num_seq = extract_clause_sequence output
-       val name_map = extract_clause_formula_relation output
-       val name_seq = num_seq |> map (these o AList.lookup (op =) name_map)
-     in name_seq end
-   else
-     [])
-  |> Vector.fromList
-
 fun atp_proof_from_tstplike_proof _ _ "" = []
   | atp_proof_from_tstplike_proof problem output tstp =
     tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
-    |> parse_proof problem (extract_spass_name_vector output)
+    |> parse_proof problem
     |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
 
 fun clean_up_dependencies _ [] = []

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 28 20:25:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 28 20:45:28 2012 +0200
@@ -379,23 +379,22 @@
 
 (* SPASS *)
 
-fun is_new_spass_version () =
-  string_ord (getenv "SPASS_VERSION", "3.7") = GREATER orelse
-  getenv "SPASS_NEW_HOME" <> ""
+val spass_H1SOS = "-Heuristic=1 -SOS"
+val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
+val spass_H2SOS = "-Heuristic=2 -SOS"
+val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
+val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
 
-(* TODO: Legacy: Remove after planned Isabelle2012 release (and don't forget
-   "required_vars" and "script/spass"). *)
-val spass_old_config : atp_config =
-  {exec = (["ISABELLE_ATP"], "scripts/spass"),
-   required_vars = [["SPASS_HOME"]],
-   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
-     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
-     |> sos = sosN ? prefix "-SOS=1 ",
+(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
+val spass_config : atp_config =
+  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
+   required_vars = [],
+   arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
+     ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+     |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
-     [(OldSPASS, "SPASS V 3.5"),
-      (OldSPASS, "SPASS V 3.7"),
+     [(OldSPASS, "Unrecognized option Isabelle"),
       (GaveUp, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
@@ -405,47 +404,20 @@
       (InternalError, "Please report this error")] @
       known_perl_failures,
    prem_role = Conjecture,
-   best_slices = fn ctxt =>
+   best_slices = fn _ =>
      (* FUDGE *)
-     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
-      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
-      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
-     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I),
+     [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
+      (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H2SOS))),
+      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_H2LR0LT0))),
+      (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2NuVS0))),
+      (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_H1SOS))),
+      (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
+      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_H2SOS))),
+      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
-val spass_new_H1SOS = "-Heuristic=1 -SOS"
-val spass_new_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
-val spass_new_H2SOS = "-Heuristic=2 -SOS"
-val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
-val spass_new_H2NuVS0Red2 =
-  "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
-
-val spass_new_config : atp_config =
-  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
-   required_vars = [],
-   arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
-     ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
-     |> extra_options <> "" ? prefix (extra_options ^ " "),
-   proof_delims = #proof_delims spass_old_config,
-   known_failures = #known_failures spass_old_config,
-   prem_role = #prem_role spass_old_config,
-   best_slices = fn _ =>
-     (* FUDGE *)
-     [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
-      (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
-      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2LR0LT0))),
-      (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
-      (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
-      (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
-      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
-      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))],
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
-
-val spass =
-  (spassN, fn () => if is_new_spass_version () then spass_new_config
-                    else spass_old_config)
+val spass = (spassN, fn () => spass_config)
 
 (* Vampire *)
 
@@ -677,7 +649,7 @@
 fun effective_term_order ctxt atp =
   let val ord = Config.get ctxt term_order in
     if ord = smartN then
-      if atp = spassN andalso is_new_spass_version () then
+      if atp = spassN then
         {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
       else
         {is_lpo = false, gen_weights = false, gen_prec = false,

--- a/src/HOL/Tools/ATP/scripts/spass	Mon May 28 20:25:38 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-#
-# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
-# Isar proof reconstruction)
-#
-# Author: Jasmin Blanchette, TU Muenchen
-
-options=${@:1:$(($#-1))}
-name=${@:$(($#)):1}
-home=${SPASS_OLD_HOME:-$SPASS_HOME}
-
-"$home/SPASS" -Flotter "$name" \
-    | sed 's/description({$/description({*/' \
-    | sed 's/set_ClauseFormulaRelation()\.//' \
-    > $name.cnf
-cat $name.cnf
-"$home/SPASS" $options "$name.cnf" \
-    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f "$name.cnf"