# HG changeset patch
# User blanchet
# Date 1297177808 -3600
# Node ID 7cca2de892960596e773c1eb7fa4f87cb122c745
# Parent  14d135c09bec6a381c4e1f12990e3362356c4246
added support for bleeding-edge E weighting function "SymOffsetsWeight"

diff -r 14d135c09bec -r 7cca2de89296 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 08 16:10:07 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 08 16:10:08 2011 +0100
@@ -20,10 +20,16 @@
      explicit_forall: bool,
      use_conjecture_for_hypotheses: bool}
 
+  datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+
   (* for experimentation purposes -- do not use in production code *)
-  val e_weights : bool Unsynchronized.ref
-  val e_weight_factor : real Unsynchronized.ref
-  val e_default_weight : real Unsynchronized.ref
+  val e_weight_method : e_weight_method Unsynchronized.ref
+  val e_default_fun_weight : real Unsynchronized.ref
+  val e_fun_weight_base : real Unsynchronized.ref
+  val e_fun_weight_factor : real Unsynchronized.ref
+  val e_default_sym_offs_weight : real Unsynchronized.ref
+  val e_sym_offs_weight_base : real Unsynchronized.ref
+  val e_sym_offs_weight_factor : real Unsynchronized.ref
 
   val eN : string
   val spassN : string
@@ -95,28 +101,46 @@
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
-val e_weights = Unsynchronized.ref true
-val e_weight_factor = Unsynchronized.ref 40.0
-val e_default_weight = Unsynchronized.ref 0.5
+datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+
+val e_weight_method = Unsynchronized.ref E_Fun_Weight
+val e_default_fun_weight = Unsynchronized.ref 0.5
+val e_fun_weight_base = Unsynchronized.ref 0.0
+val e_fun_weight_factor = Unsynchronized.ref 40.0
+val e_default_sym_offs_weight = Unsynchronized.ref 0.0
+val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
+val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
+
+fun e_weight_method_case fw sow =
+  case !e_weight_method of
+    E_Auto => raise Fail "Unexpected \"E_Auto\""
+  | E_Fun_Weight => fw
+  | E_Sym_Offset_Weight => sow
+
+fun scaled_e_weight w =
+  e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base)
+  + w * e_weight_method_case (!e_fun_weight_factor) (!e_sym_offs_weight_factor)
+  |> Real.ceil |> signed_string_of_int
 
 fun e_weight_arguments weights =
-  if !e_weights andalso string_ord (getenv "E_VERSION", "1.2w") <> LESS then
+  if !e_weight_method = E_Auto orelse
+     string_ord (getenv "E_VERSION", "1.2w") = LESS then
+    "-xAutoDev"
+  else
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
-    \-H'(4*FunWeight(SimulateSOS, " ^
-    string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^
+    \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
+    "(SimulateSOS, " ^
+    scaled_e_weight (e_weight_method_case (!e_default_fun_weight)
+                                          (!e_default_sym_offs_weight)) ^
     ",20,1.5,1.5,1" ^
-    (weights ()
-     |> map (fn (s, w) => "," ^ s ^ ":" ^
-                          string_of_int (Real.ceil (w * !e_weight_factor)))
-     |> implode) ^
+    (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight 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))'"
-  else
-    "-xAutoDev"
 
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),