# HG changeset patch
# User blanchet
# Date 1403606205 -7200
# Node ID d473cadda13b9dd3f70d6577a283a0531dc6adfc
# Parent  2502adc3c3f661b8bec660b645f3ef18e847da5d
optimize log

diff -r 2502adc3c3f6 -r d473cadda13b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 12:35:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jun 24 12:36:45 2014 +0200
@@ -512,20 +512,23 @@
 
     fun for i =
       if i = num_facts then () else (learn i (get_feats i) (get_deps i); for (i + 1))
+
+    val ln_afreq = Math.ln (Real.fromInt num_facts)
   in
-    for 0; (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq)
+    for 0;
+    (Array.vector tfreq, Array.vector sfreq,
+     Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) (Array.vector dffreq))
   end
 
 fun naive_bayes_query (kuehlwein_log, kuehlwein_params) num_facts num_visible_facts max_suggs feats
-    (tfreq, sfreq, dffreq) =
+    (tfreq, sfreq, idf) =
   let
     val tau = if kuehlwein_params then 0.05 else 0.02 (* FUDGE *)
     val pos_weight = if kuehlwein_params then 10.0 else 2.0 (* FUDGE *)
     val def_val = ~15.0 (* FUDGE *)
 
-    val afreq = Real.fromInt num_facts
-    fun tfidf feat =
-      Math.ln afreq - (Math.ln (Real.fromInt (Vector.sub (dffreq, feat))) handle Subscript => 0.0)
+    val ln_afreq = Math.ln (Real.fromInt num_facts)
+    fun tfidf feat = Vector.sub (idf, feat) handle Subscript => ln_afreq (* TODO: clean up *)
 
     fun log_posterior i =
       let