# HG changeset patch
# User blanchet
# Date 1359627612 -3600
# Node ID 31f9ba85dc2e990e57022103d25bbba3b8d0ce99
# Parent  51ad7b4ac0967f44a2df503ce656207749f8a190
compute proper weight for "p proves p" in MaSh

diff -r 51ad7b4ac096 -r 31f9ba85dc2e src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Tue Jan 15 12:13:27 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Thu Jan 31 11:20:12 2013 +0100
@@ -34,15 +34,13 @@
         """
         for d in trainData:            
             dFeatureCounts = {}
-            # Give p |- p a higher weight
+            # Add p proves p with weight self.defaultPriorWeight
             if not self.defaultPriorWeight == 0:            
                 for f,_w in dicts.featureDict[d]:
                     dFeatureCounts[f] = self.defaultPriorWeight
             self.counts[d] = [self.defaultPriorWeight,dFeatureCounts]
 
-        for key in dicts.dependenciesDict.keys():
-            # Add p proves p
-            keyDeps = [key]+dicts.dependenciesDict[key]
+        for key,keyDeps in dicts.dependenciesDict.iteritems():
             for dep in keyDeps:
                 self.counts[dep][0] += 1
                 depFeatures = dicts.featureDict[key]
@@ -105,7 +103,7 @@
             resultA = log(posA)
             for f,w in features:
                 # DEBUG
-                #w = 1
+                #w = 1.0
                 if f in fA:
                     if fWeightsA[f] == 0:
                         resultA += w*self.defVal