src/HOL/Tools/Sledgehammer/MaSh/src/stats.py

added weights to MaSh (by Daniel Kuehlwein)

#     Title:      HOL/Tools/Sledgehammer/MaSh/src/stats.py
#     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
#     Copyright   2012
#
# Statistics collector.

'''
Created on Jul 9, 2012

@author: Daniel Kuehlwein
'''

import logging,string
from cPickle import load,dump

class Statistics(object):
    '''
    Class for all the statistics
    '''

    def __init__(self,cutOff=500):
        '''
        Constructor
        '''
        self.logger = logging.getLogger('Statistics')
        self.avgAUC = 0.0
        self.avgRecall100 = 0.0
        self.avgAvailable = 0.0
        self.avgDepNr = 0.0
        self.problems = 0.0
        self.cutOff = cutOff
        self.recallData = [0]*cutOff
        self.recall100Data = [0]*cutOff
        self.aucData = []
        self.premiseOccurenceCounter = {}
        self.firstDepAppearance = {}
        self.depAppearances = []

    def update(self,predictions,dependencies,statementCounter):
        """
        Evaluates AUC, dependencies, recall100 and number of available premises of a prediction.
        """
        available = len(predictions)
        predictions = predictions[:self.cutOff]
        dependencies = set(dependencies)
        # No Stats for if no dependencies
        if len(dependencies) == 0:
            self.logger.debug('No Dependencies for statement %s' % statementCounter )
            self.badPreds = []
            return
        if len(predictions) < self.cutOff:
            for i in range(len(predictions),self.cutOff):
                self.recall100Data[i] += 1
                self.recallData[i] += 1
        for d in dependencies:
            if self.premiseOccurenceCounter.has_key(d):
                self.premiseOccurenceCounter[d] += 1
            else:
                self.premiseOccurenceCounter[d] = 1
            if self.firstDepAppearance.has_key(d):
                self.depAppearances.append(statementCounter-self.firstDepAppearance[d])
            else:
                self.firstDepAppearance[d] = statementCounter
        depNr = len(dependencies)
        aucSum = 0.
        posResults = 0.
        positives, negatives = 0, 0
        recall100 = 0.0
        badPreds = []
        depsFound = []
        for index,pId in enumerate(predictions):
            if pId in dependencies:        #positive
                posResults+=1
                positives+=1
                recall100 = index+1
                depsFound.append(pId)
                if index > 200:
                    badPreds.append(pId)
            else:
                aucSum += posResults
                negatives+=1
            # Update Recall and Recall100 stats
            if depNr == positives:
                self.recall100Data[index] += 1
            if depNr == 0:
                self.recallData[index] += 1
            else:
                self.recallData[index] += float(positives)/depNr

        if not depNr == positives:
            depsFound = set(depsFound)
            missing = []
            for dep in dependencies:
                if not dep in depsFound:
                    missing.append(dep)
                    badPreds.append(dep)
                    recall100 = len(predictions)+1
                    positives+=1
            self.logger.debug('Dependencies missing for %s in accessibles! Estimating Statistics.',\
                              string.join([str(dep) for dep in missing],','))

        if positives == 0 or negatives == 0:
            auc = 1.0
        else:
            auc = aucSum/(negatives*positives)

        self.aucData.append(auc)
        self.avgAUC += auc
        self.avgRecall100 += recall100
        self.problems += 1
        self.badPreds = badPreds
        self.avgAvailable += available
        self.avgDepNr += depNr
        self.logger.info('Statement: %s: AUC: %s \t Needed: %s \t Recall100: %s \t Available: %s \t cutOff:%s',\
                          statementCounter,round(100*auc,2),depNr,recall100,available,self.cutOff)

    def printAvg(self):
        self.logger.info('Average results:')
        self.logger.info('avgAUC: %s \t avgDepNr: %s \t avgRecall100: %s \t cutOff:%s', \
                         round(100*self.avgAUC/self.problems,2),round(self.avgDepNr/self.problems,2),round(self.avgRecall100/self.problems,2),self.cutOff)

        #try:
        if True:
            from matplotlib.pyplot import plot,figure,show,xlabel,ylabel,axis,hist
            avgRecall = [float(x)/self.problems for x in self.recallData]
            figure('Recall')
            plot(range(self.cutOff),avgRecall)
            ylabel('Average Recall')
            xlabel('Highest ranked premises')
            axis([0,self.cutOff,0.0,1.0])
            figure('100%Recall')
            plot(range(self.cutOff),self.recall100Data)
            ylabel('100%Recall')
            xlabel('Highest ranked premises')
            axis([0,self.cutOff,0,self.problems])
            figure('AUC Histogram')
            hist(self.aucData,bins=100)
            ylabel('Problems')
            xlabel('AUC')
            maxCount = max(self.premiseOccurenceCounter.values())
            minCount = min(self.premiseOccurenceCounter.values())
            figure('Dependency Occurances')
            hist(self.premiseOccurenceCounter.values(),bins=range(minCount,maxCount+2),align = 'left')
            #ylabel('Occurences')
            xlabel('Number of Times a Dependency Occurs')
            figure('Dependency Appearance in Problems after Introduction.')
            hist(self.depAppearances,bins=50)
            figure('Dependency Appearance in Problems after Introduction in Percent.')
            xAxis = range(max(self.depAppearances)+1)
            yAxis = [0] * (max(self.depAppearances)+1)
            for val in self.depAppearances:
                yAxis[val] += 1
            yAxis = [float(x)/len(self.firstDepAppearance.keys()) for x in yAxis]
            plot(xAxis,yAxis)
            show()
        #except:
        #    self.logger.warning('Matplotlib module missing. Skipping graphs.')

    def save(self,fileName):
        oStream = open(fileName, 'wb')
        dump((self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData,self.premiseOccurenceCounter),oStream)
        oStream.close()
    def load(self,fileName):
        iStream = open(fileName, 'rb')
        self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData,self.premiseOccurenceCounter = load(iStream)
        iStream.close()