src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py
author blanchet
Mon, 26 Nov 2012 13:35:05 +0100
changeset 50222 40e3c3be6bca
parent 50220 90280d85cd03
child 50388 a5b666e0c3c2
permissions -rw-r--r--
added file headers

#     Title:      HOL/Tools/Sledgehammer/MaSh/src/predefined.py
#     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
#     Copyright   2012
#
# A classifier that uses the Meng-Paulson predictions.

'''
Created on Jul 11, 2012

@author: Daniel Kuehlwein
'''

from cPickle import dump,load

class Predefined(object):
    '''
    A classifier that uses the Meng-Paulson predictions.
    Only used to easily compare statistics between the old Sledgehammer algorithm and the new machine learning ones.
    '''

    def __init__(self,mpPredictionFile):
        '''
        Constructor
        '''
        self.predictionFile = mpPredictionFile
    
    def initializeModel(self,_trainData,dicts):
        """
        Load predictions.
        """        
        self.predictions = {}
        IS = open(self.predictionFile,'r')
        for line in IS:
            line = line.split(':')
            name = line[0].strip()
            predId = dicts.get_name_id(name)
            line = line[1].split()
            preds = [dicts.get_name_id(x.strip())for x in line]
            self.predictions[predId] = preds
        IS.close()
        return dicts
    
    def update(self,dataPoint,features,dependencies):
        """
        Updates the Model.
        """
        # No Update needed since we assume that we got all predictions
        pass
            
    
    def predict(self,problemId):
        """
        Return the saved predictions.
        """
        return self.predictions[problemId] 
    
    def save(self,fileName):
        OStream = open(fileName, 'wb')
        dump((self.predictionFile,self.predictions),OStream)        
        OStream.close()
        
    def load(self,fileName):
        OStream = open(fileName, 'rb')
        self.predictionFile,self.predictions = load(OStream)      
        OStream.close()