# HG changeset patch # User blanchet # Date 1332200670 -3600 # Node ID 7e80e14247fc9ffea71bf09294c862d69e8ca174 # Parent 72802e2edda464f61d6f743474b5cf051e31977f internal renamings diff -r 72802e2edda4 -r 7e80e14247fc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 20 00:44:30 2012 +0100 @@ -13,7 +13,7 @@ val sliceK = "slice" val lam_transK = "lam_trans" val uncurried_aliasesK = "uncurried_aliases" -val e_weight_methodK = "e_weight_method" +val e_selection_weight_methodK = "e_selection_weight_method" val force_sosK = "force_sos" val max_relevantK = "max_relevant" val max_callsK = "max_calls" @@ -376,9 +376,9 @@ SH_ERROR fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans - uncurried_aliases e_weight_method force_sos hard_timeout timeout - preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST - dir pos st = + uncurried_aliases e_selection_weight_method force_sos hard_timeout + timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST + max_mono_itersLST dir pos st = let val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 @@ -391,12 +391,13 @@ ^ serial_string ()) | set_file_name NONE = I val st' = - st |> Proof.map_context - (set_file_name dir - #> (Option.map (Config.put ATP_Systems.e_weight_method) - e_weight_method |> the_default I) - #> (Option.map (Config.put ATP_Systems.force_sos) - force_sos |> the_default I)) + st + |> Proof.map_context + (set_file_name dir + #> (Option.map (Config.put ATP_Systems.e_selection_weight_method) + e_selection_weight_method |> the_default I) + #> (Option.map (Config.put ATP_Systems.force_sos) + force_sos |> the_default I)) val params as {relevance_thresholds, max_relevant, slice, ...} = Sledgehammer_Isar.default_params ctxt ([("verbose", "true"), @@ -491,7 +492,7 @@ val slice = AList.lookup (op =) args sliceK |> the_default "true" val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK - val e_weight_method = AList.lookup (op =) args e_weight_methodK + val e_selection_weight_method = AList.lookup (op =) args e_selection_weight_methodK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") val dir = AList.lookup (op =) args keepK @@ -507,9 +508,9 @@ val hard_timeout = SOME (2 * timeout) val (msg, result) = run_sh prover_name prover type_enc strict max_relevant slice lam_trans - uncurried_aliases e_weight_method force_sos hard_timeout timeout - preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST - dir pos st + uncurried_aliases e_selection_weight_method force_sos hard_timeout + timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST + max_mono_itersLST dir pos st in case result of SH_OK (time_isa, time_prover, names) => diff -r 72802e2edda4 -r 7e80e14247fc src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 00:44:30 2012 +0100 @@ -85,7 +85,7 @@ val rankN : string val minimum_rank : int val default_rank : int - val default_kbo_weight : int + val default_term_order_weight : int val is_tptp_equal : string -> bool val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool @@ -211,7 +211,7 @@ val minimum_rank = 0 val default_rank = 1000 -val default_kbo_weight = 1 +val default_term_order_weight = 1 (* Currently, only newer versions of SPASS, with sorted DFG format support, can process Isabelle metainformation. *) @@ -496,7 +496,7 @@ | str_for_formula top_level (AAtom tm) = str_for_term top_level tm in str_for_formula true end -fun dfg_lines flavor kbo_weights problem = +fun dfg_lines flavor ord_weights problem = let val sorted = (flavor = DFG_Sorted) val format = DFG flavor @@ -533,10 +533,10 @@ if s = tptp_type_of_types then SOME sym else NONE | _ => NONE) @ [[dfg_individual_type]] |> flat |> commas |> enclose "sorts [" "]." - fun do_kbo_weights () = - kbo_weights () |> map spair |> commas |> enclose "weights [" "]." + fun do_term_order_weights () = + ord_weights () |> map spair |> commas |> enclose "weights [" "]." val syms = - [func_aries] @ (if sorted then [do_kbo_weights ()] else []) @ + [func_aries] @ (if sorted then [do_term_order_weights ()] else []) @ [pred_aries] @ (if sorted then [sorts ()] else []) fun func_sigs () = filt (fn Decl (_, sym, ty) => @@ -570,11 +570,11 @@ ["end_problem.\n"] end -fun lines_for_atp_problem format kbo_weights problem = +fun lines_for_atp_problem format ord_weights problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: (case format of - DFG flavor => dfg_lines flavor kbo_weights + DFG flavor => dfg_lines flavor ord_weights | _ => tptp_lines format) problem diff -r 72802e2edda4 -r 7e80e14247fc src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 @@ -107,8 +107,8 @@ -> ((string * stature) * term) list -> string problem * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table - val atp_problem_relevance_weights : string problem -> (string * real) list - val atp_problem_kbo_weights : string problem -> (string * int) list + val atp_problem_selection_weights : string problem -> (string * real) list + val atp_problem_term_order_weights : string problem -> (string * int) list end; structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = @@ -2710,7 +2710,7 @@ val type_info_default_weight = 0.8 (* Weights are from 0.0 (most important) to 1.0 (least important). *) -fun atp_problem_relevance_weights problem = +fun atp_problem_selection_weights problem = let fun add_term_weights weight (ATerm (s, tms)) = is_tptp_user_symbol s ? Symtab.default (s, weight) @@ -2754,9 +2754,9 @@ (s, args) | have_head_rolling _ = ("", []) -val max_kbo_weight = 2147483647 +val max_term_order_weight = 2147483647 -fun atp_problem_kbo_weights problem = +fun atp_problem_term_order_weights problem = let fun add_term_deps head (ATerm (s, args)) = is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head))) @@ -2780,7 +2780,7 @@ val graph = Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem |> fold (fold (add_line_deps simpN) o snd) problem - fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1 + fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1 fun add_weights _ [] = I | add_weights weight syms = fold (AList.update (op =) o rpair weight) syms diff -r 72802e2edda4 -r 7e80e14247fc src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 00:44:30 2012 +0100 @@ -228,7 +228,7 @@ e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int -fun e_selection_weight_arguments ctxt method weights = +fun e_selection_weight_arguments ctxt method sel_weights = if method = e_autoN then "-xAutoDev" else @@ -244,7 +244,7 @@ e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ - (weights () + (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_selection_weight ctxt method w) |> implode) ^ @@ -260,9 +260,9 @@ {exec = ("E_HOME", "eproof"), required_execs = [], arguments = - fn ctxt => fn _ => fn method => fn timeout => fn weights => + fn ctxt => fn _ => fn method => fn timeout => fn sel_weights => "--tstp-in --tstp-out -l5 " ^ - e_selection_weight_arguments ctxt method weights ^ + e_selection_weight_arguments ctxt method sel_weights ^ " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout), proof_delims = tstp_proof_delims, known_failures = diff -r 72802e2edda4 -r 7e80e14247fc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 00:44:30 2012 +0100 @@ -709,17 +709,17 @@ |> prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc false lam_trans uncurried_aliases readable_names true hyp_ts concl_t - fun rel_weights () = atp_problem_relevance_weights atp_problem - fun kbo_weights () = atp_problem_kbo_weights atp_problem + fun sel_weights () = atp_problem_selection_weights atp_problem + fun ord_weights () = atp_problem_term_order_weights atp_problem val full_proof = debug orelse isar_proof val command = File.shell_path command ^ " " ^ - arguments ctxt full_proof extra slice_timeout rel_weights ^ + arguments ctxt full_proof extra slice_timeout sel_weights ^ " " ^ File.shell_path prob_file |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" val _ = atp_problem - |> lines_for_atp_problem format kbo_weights + |> lines_for_atp_problem format ord_weights |> cons ("% " ^ command ^ "\n") |> File.write_list prob_file val ((output, run_time), (atp_proof, outcome)) =