--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Sat Dec 07 18:06:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Dec 09 04:03:30 2013 +0100
@@ -96,12 +96,19 @@
return nameId
def add_feature(self,featureName):
- if not self.featureIdDict.has_key(featureName):
- self.featureIdDict[featureName] = self.maxFeatureId
- self.maxFeatureId += 1
- self.changed = True
- fId = self.featureIdDict[featureName]
- return fId
+ fMul = featureName.split('|')
+ fIds = []
+ for f in fMul:
+ if not self.featureIdDict.has_key(f):
+ self.featureIdDict[f] = self.maxFeatureId
+ self.maxFeatureId += 1
+ self.changed = True
+ fId = self.featureIdDict[f]
+ fIds.append(fId)
+ if len(fIds) == 1:
+ return fIds[0]
+ else:
+ return fIds
def get_features(self,line):
featureNames = [f.strip() for f in line[1].split()]
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py Sat Dec 07 18:06:49 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py Mon Dec 09 04:03:30 2013 +0100
@@ -112,7 +112,19 @@
for f,w in features.iteritems():
# DEBUG
#w = 1.0
- if f in fA:
+ # Test for multiple features
+ isMatch = False
+ if not isinstance( f, ( int, long ) ):
+ f = f[0]
+ inter = set(f).intersection(fA)
+ if len(inter) > 0:
+ isMatch = True
+ else:
+ if f in fA:
+ isMatch = True
+
+ if isMatch:
+ #if f in fA:
if fWeightsA[f] == 0:
resultA += w*self.defVal
else: