--- 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_selection_weight_methodK = "e_selection_weight_method"
+val e_selection_heuristicK = "e_selection_heuristic"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val max_callsK = "max_calls"
@@ -376,7 +376,7 @@
SH_ERROR
fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
- uncurried_aliases e_selection_weight_method force_sos hard_timeout
+ uncurried_aliases e_selection_heuristic force_sos hard_timeout
timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
max_mono_itersLST dir pos st =
let
@@ -394,8 +394,8 @@
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.e_selection_heuristic)
+ e_selection_heuristic |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I))
val params as {relevance_thresholds, max_relevant, slice, ...} =
@@ -492,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_selection_weight_method = AList.lookup (op =) args e_selection_weight_methodK
+ val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
val dir = AList.lookup (op =) args keepK
@@ -508,7 +508,7 @@
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_selection_weight_method force_sos hard_timeout
+ uncurried_aliases e_selection_heuristic force_sos hard_timeout
timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
max_mono_itersLST dir pos st
in
--- 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
@@ -2746,13 +2746,13 @@
|> sort (prod_ord Real.compare string_ord o pairself swap)
end
-fun have_head_rolling (ATerm (s, args)) =
- (* ugly hack: may make innocent victims *)
+fun make_head_roll (ATerm (s, args)) =
+ (* ugly hack: may make innocent victims (collateral damage) *)
if String.isPrefix app_op_name s andalso length args = 2 then
- have_head_rolling (hd args) ||> append (tl args)
+ make_head_roll (hd args) ||> append (tl args)
else
(s, args)
- | have_head_rolling _ = ("", [])
+ | make_head_roll _ = ("", [])
val max_term_order_weight = 2147483647
@@ -2764,7 +2764,7 @@
| add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
if is_tptp_equal s then
- let val (head, rest) = have_head_rolling lhs in
+ let val (head, rest) = make_head_roll lhs in
fold (add_term_deps head) (rhs :: rest)
end
else
--- 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
@@ -26,11 +26,12 @@
Proof.context -> (real * (bool * (slice_spec * string))) list}
val force_sos : bool Config.T
+ val term_order : string Config.T
val e_smartN : string
val e_autoN : string
val e_fun_weightN : string
val e_sym_offset_weightN : string
- val e_selection_weight_method : string Config.T
+ val e_selection_heuristic : string Config.T
val e_default_fun_weight : real Config.T
val e_fun_weight_base : real Config.T
val e_fun_weight_span : real Config.T
@@ -161,6 +162,16 @@
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
+val smartN = "smart"
+val kboN = "kbo"
+val lpoN = "lpo"
+val weightsN = "_weights"
+val precsN = "_precs"
+val lrN = "_lr" (* SPASS-specific *)
+
+val term_order =
+ Attrib.setup_config_string @{binding atp_term_order} (K smartN)
+
(* Alt-Ergo *)
@@ -200,8 +211,8 @@
val e_fun_weightN = "fun_weight"
val e_sym_offset_weightN = "sym_offset_weight"
-val e_selection_weight_method =
- Attrib.setup_config_string @{binding atp_e_selection_weight_method} (K e_smartN)
+val e_selection_heuristic =
+ Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
(* FUDGE *)
val e_default_fun_weight =
Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
@@ -216,15 +227,15 @@
val e_sym_offs_weight_span =
Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
-fun e_selection_weight_method_case method fw sow =
+fun e_selection_heuristic_case method fw sow =
if method = e_fun_weightN then fw
else if method = e_sym_offset_weightN then sow
else raise Fail ("unexpected " ^ quote method)
fun scaled_e_selection_weight ctxt method w =
- w * Config.get ctxt (e_selection_weight_method_case method
+ w * Config.get ctxt (e_selection_heuristic_case method
e_fun_weight_span e_sym_offs_weight_span)
- + Config.get ctxt (e_selection_weight_method_case method
+ + Config.get ctxt (e_selection_heuristic_case method
e_fun_weight_base e_sym_offs_weight_base)
|> Real.ceil |> signed_string_of_int
@@ -237,10 +248,9 @@
\--destructive-er-aggressive --destructive-er --presat-simplify \
\--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
- \-H'(4*" ^
- e_selection_weight_method_case method "FunWeight" "SymOffsetWeight" ^
+ \-H'(4*" ^ e_selection_heuristic_case method "FunWeight" "SymOffsetWeight" ^
"(SimulateSOS, " ^
- (e_selection_weight_method_case method
+ (e_selection_heuristic_case method
e_default_fun_weight e_default_sym_offs_weight
|> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
",20,1.5,1.5,1" ^
@@ -252,9 +262,8 @@
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
\FIFOWeight(PreferProcessed))'"
-fun effective_e_selection_weight_method ctxt =
- if is_old_e_version () then e_autoN
- else Config.get ctxt e_selection_weight_method
+fun effective_e_selection_heuristic ctxt =
+ if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic
val e_config : atp_config =
{exec = ("E_HOME", "eproof"),
@@ -273,7 +282,7 @@
conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
best_slices = fn ctxt =>
- let val method = effective_e_selection_weight_method ctxt in
+ let val method = effective_e_selection_heuristic ctxt in
(* FUDGE *)
if method = e_smartN then
[(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),