compute proper weight for "p proves p" in MaSh
authorblanchet
Thu, 31 Jan 2013 11:20:12 +0100
changeset 5217931f9ba85dc2e
parent 52178 51ad7b4ac096
child 52180 501200635659
compute proper weight for "p proves p" in MaSh
src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py
     1.1 --- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Tue Jan 15 12:13:27 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Thu Jan 31 11:20:12 2013 +0100
     1.3 @@ -34,15 +34,13 @@
     1.4          """
     1.5          for d in trainData:            
     1.6              dFeatureCounts = {}
     1.7 -            # Give p |- p a higher weight
     1.8 +            # Add p proves p with weight self.defaultPriorWeight
     1.9              if not self.defaultPriorWeight == 0:            
    1.10                  for f,_w in dicts.featureDict[d]:
    1.11                      dFeatureCounts[f] = self.defaultPriorWeight
    1.12              self.counts[d] = [self.defaultPriorWeight,dFeatureCounts]
    1.13  
    1.14 -        for key in dicts.dependenciesDict.keys():
    1.15 -            # Add p proves p
    1.16 -            keyDeps = [key]+dicts.dependenciesDict[key]
    1.17 +        for key,keyDeps in dicts.dependenciesDict.iteritems():
    1.18              for dep in keyDeps:
    1.19                  self.counts[dep][0] += 1
    1.20                  depFeatures = dicts.featureDict[key]
    1.21 @@ -105,7 +103,7 @@
    1.22              resultA = log(posA)
    1.23              for f,w in features:
    1.24                  # DEBUG
    1.25 -                #w = 1
    1.26 +                #w = 1.0
    1.27                  if f in fA:
    1.28                      if fWeightsA[f] == 0:
    1.29                          resultA += w*self.defVal