# HG changeset patch # User blanchet # Date 1338230728 -7200 # Node ID eeede26f272109b703fba173c7a57177c18bf284 # Parent 989a34fa72b3dda1c224b8a10b70ad3c6b4638a0 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8 diff -r 989a34fa72b3 -r eeede26f2721 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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), diff -r 989a34fa72b3 -r eeede26f2721 src/HOL/Tools/ATP/atp_proof.ML --- 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: [0:] || -> . derived from formulae * *) -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 _ [] = [] diff -r 989a34fa72b3 -r eeede26f2721 src/HOL/Tools/ATP/atp_systems.ML --- 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, diff -r 989a34fa72b3 -r eeede26f2721 src/HOL/Tools/ATP/scripts/spass --- 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"