# HG changeset patch
# User blanchet
# Date 1332200670 -3600
# Node ID 73cdeed236c0c102ef67a4f6a6a4b7a782624167
# Parent  26dd49368db6ed5f3365574820c4e521e0787a01
more weight attribute tuning

diff -r 26dd49368db6 -r 73cdeed236c0 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_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
diff -r 26dd49368db6 -r 73cdeed236c0 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
@@ -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
diff -r 26dd49368db6 -r 73cdeed236c0 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
@@ -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))),