# HG changeset patch
# User blanchet
# Date 1332200670 -3600
# Node ID 72802e2edda464f61d6f743474b5cf051e31977f
# Parent  e3a3f161ad70e21a1a34d3942ee620ed96baabb3
renamed E weight attribute

diff -r e3a3f161ad70 -r 72802e2edda4 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Mar 19 23:17:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
@@ -30,7 +30,7 @@
   val e_autoN : string
   val e_fun_weightN : string
   val e_sym_offset_weightN : string
-  val e_weight_method : string Config.T
+  val e_selection_weight_method : 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
@@ -200,8 +200,8 @@
 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_smartN)
+val e_selection_weight_method =
+  Attrib.setup_config_string @{binding atp_e_selection_weight_method} (K e_smartN)
 (* FUDGE *)
 val e_default_fun_weight =
   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
@@ -216,19 +216,19 @@
 val e_sym_offs_weight_span =
   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
 
-fun e_weight_method_case method fw sow =
+fun e_selection_weight_method_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_weight ctxt method w =
-  w * Config.get ctxt
-          (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
-  + Config.get ctxt
-        (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
+fun scaled_e_selection_weight ctxt method w =
+  w * Config.get ctxt (e_selection_weight_method_case method
+                           e_fun_weight_span e_sym_offs_weight_span)
+  + Config.get ctxt (e_selection_weight_method_case method
+                         e_fun_weight_base e_sym_offs_weight_base)
   |> Real.ceil |> signed_string_of_int
 
-fun e_weight_arguments ctxt method weights =
+fun e_selection_weight_arguments ctxt method weights =
   if method = e_autoN then
     "-xAutoDev"
   else
@@ -237,27 +237,32 @@
     \--destructive-er-aggressive --destructive-er --presat-simplify \
     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
-    \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
+    \-H'(4*" ^
+    e_selection_weight_method_case method "FunWeight" "SymOffsetWeight" ^
     "(SimulateSOS, " ^
-    (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
+    (e_selection_weight_method_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" ^
     (weights ()
-     |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
+     |> map (fn (s, w) => "," ^ s ^ ":" ^
+                          scaled_e_selection_weight ctxt method w)
      |> implode) ^
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))'"
 
-fun effective_e_weight_method ctxt =
-  if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
+fun effective_e_selection_weight_method ctxt =
+  if is_old_e_version () then e_autoN
+  else Config.get ctxt e_selection_weight_method
 
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments =
      fn ctxt => fn _ => fn method => fn timeout => fn weights =>
-        "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
+        "--tstp-in --tstp-out -l5 " ^
+        e_selection_weight_arguments ctxt method weights ^
         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
@@ -268,7 +273,7 @@
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
-     let val method = effective_e_weight_method ctxt in
+     let val method = effective_e_selection_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
          [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),