new version of MaSh

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/singleNaiveBayes.py	Thu Dec 27 10:21:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/singleNaiveBayes.py	Thu Dec 27 12:34:06 2012 +0100
@@ -70,12 +70,12 @@
             self.counts[f] = [posCount,negCount]
 
             
-    def overwrite(self,features,label):
+    def overwrite(self,features,labelOld,labelNew):
         """
         Deletes the old dependencies of problemId and replaces them with the new ones. Updates the model accordingly.
         """
-        self.delete(features,label)
-        self.update(features,label)
+        self.delete(features,labelOld)
+        self.update(features,labelNew)
     
     def predict_sparse(self,features):
         """

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/theoryModels.py	Thu Dec 27 10:21:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/theoryModels.py	Thu Dec 27 12:34:06 2012 +0100
@@ -26,7 +26,7 @@
         '''
         self.theoryModels = {}
         self.theoryDict = {}
-        self.accessibleTheories = []
+        self.accessibleTheories = set([])
         self.currentTheory = None
   
     def init(self,depFile,dicts):      
@@ -46,7 +46,7 @@
             if not self.theoryDict.has_key(theory):
                 assert not theory == self.currentTheory
                 if not self.currentTheory == None:
-                    self.accessibleTheories.append(self.currentTheory)
+                    self.accessibleTheories.add(self.currentTheory)
                 self.currentTheory = theory
                 self.theoryDict[theory] = set([nameId])
                 theoryModel = singleNBClassifier()
@@ -75,7 +75,17 @@
         IS.close()
     
     def overwrite(self,problemId,newDependencies,dicts):
-        pass
+        features = dicts.featureDict[problemId]
+        unExpAccessibles = dicts.accessibleDict[problemId]
+        accessibles = dicts.expand_accessibles(unExpAccessibles)
+        accTheories = []
+        for x in accessibles:
+            xArt = (dicts.idNameDict[x]).split('.')[0]
+            accTheories.append(xArt)    
+        oldTheories = set([x.split('.')[0] for x in dicts.dependenciesDict[problemId]])
+        newTheories = set([x.split('.')[0] for x in newDependencies])    
+        for a in self.accTheories:                
+            self.theoryModels[a].overwrite(features,a in oldTheories,a in newTheories) 
     
     def delete(self):
         pass
@@ -89,12 +99,13 @@
         currentTheory = (dicts.idNameDict[problemId]).split('.')[0]       
         # Create new theory model, if there is a new theory 
         if not self.theoryDict.has_key(currentTheory):
-            assert not currentTheory == self.currentTheory
+            assert not currentTheory == self.currentTheory            
             if not currentTheory == None:
                 self.theoryDict[currentTheory] = []
                 self.currentTheory = currentTheory
                 theoryModel = singleNBClassifier()
-                self.theoryModels[currentTheory] = theoryModel          
+                self.theoryModels[currentTheory] = theoryModel
+                self.accessibleTheories.add(self.currentTheory)          
         if not len(usedTheories) == 0:
             for a in self.accessibleTheories:                
                 self.theoryModels[a].update(features,a in usedTheories)