Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adjust fudge factors
authorblanchet
Fri, 18 Feb 2011 15:17:39 +0100
changeset 41770 a710e96583d5
parent 41769 eb2e39555f98
child 41771 70d4585b11a6
child 41774 13b97824aec6
adjust fudge factors
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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 =
--- 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)) =
isabelle