compute proper weight for "p proves p" in MaSh
authorblanchet
Thu, 31 Jan 2013 11:20:12 +0100
changeset 50997 31f9ba85dc2e
parent 50996 51ad7b4ac096
child 50998 501200635659
compute proper weight for "p proves p" in MaSh
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