# HG changeset patch # User blanchet # Date 1308559262 -7200 # Node ID fb2713b803e69682c943347da66d30eb3ec80c58 # Parent ac6db8f44e5d4b5c4c08fc5a89c36670e083c040 deal with ATP time slices in a more flexible/robust fashion diff -r ac6db8f44e5d -r fb2713b803e6 src/HOL/Tools/ATP/atp_proof.ML --- 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 diff -r ac6db8f44e5d -r fb2713b803e6 src/HOL/Tools/ATP/atp_systems.ML --- 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 = diff -r ac6db8f44e5d -r fb2713b803e6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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)