# HG changeset patch
# User blanchet
# Date 1386558210 -3600
# Node ID 5ce1b96137058bff883a61748cc92ecba3bbe816
# Parent  506312c293f53fa93b6f85ddb87c214c1defe1cc
added multiple feature capability to MaSh

diff -r 506312c293f5 -r 5ce1b9613705 src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py
--- 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()]
diff -r 506312c293f5 -r 5ce1b9613705 src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py
--- 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: