--- 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) =>
--- 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
--- 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
--- 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 =
--- 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)) =