# HG changeset patch
# User blanchet
# Date 1298038659 -3600
# Node ID a710e96583d5358bfec5c7f31bd3fedafcd44be9
# Parent  eb2e39555f981dd30eaff24f62cb7d79799270d7
adjust fudge factors

diff -r eb2e39555f98 -r a710e96583d5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 18 12:32:55 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 18 15:17:39 2011 +0100
@@ -26,10 +26,10 @@
   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_fun_weight_span : 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 e_sym_offs_weight_span : real Unsynchronized.ref
 
   val eN : string
   val spassN : string
@@ -109,12 +109,13 @@
 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 20.0 (* ### *)
+(* FUDGE *)
+val e_default_fun_weight = Unsynchronized.ref 20.0
 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 1.0 (* ### *)
-val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
-val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
+val e_fun_weight_span = Unsynchronized.ref 40.0
+val e_default_sym_offs_weight = Unsynchronized.ref 1.0
+val e_sym_offs_weight_base = Unsynchronized.ref ~20.0
+val e_sym_offs_weight_span = Unsynchronized.ref 60.0
 
 fun e_weight_method_case fw sow =
   case !e_weight_method of
@@ -124,7 +125,7 @@
 
 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)
+  + w * e_weight_method_case (!e_fun_weight_span) (!e_sym_offs_weight_span)
   |> Real.ceil |> signed_string_of_int
 
 fun e_weight_arguments weights =
diff -r eb2e39555f98 -r a710e96583d5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Feb 18 12:32:55 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Feb 18 15:17:39 2011 +0100
@@ -650,8 +650,8 @@
 
 (* FUDGE *)
 val conj_weight = 0.0
-val hyp_weight = 0.05
-val fact_min_weight = 0.1
+val hyp_weight = 0.1
+val fact_min_weight = 0.2
 val fact_max_weight = 1.0
 
 fun add_term_weights weight (ATerm (s, tms)) =