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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50222
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     1
#     Title:      HOL/Tools/Sledgehammer/MaSh/src/predefined.py
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     2
#     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     3
#     Copyright   2012
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     4
#
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     5
# A classifier that uses the Meng-Paulson predictions.
40e3c3be6bca added file headers
blanchet
parents: 50220
diff changeset
     6
50220
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     7
'''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     8
Created on Jul 11, 2012
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     9
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    10
@author: Daniel Kuehlwein
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    11
'''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    12
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    13
from cPickle import dump,load
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    14
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    15
class Predefined(object):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    16
    '''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    17
    A classifier that uses the Meng-Paulson predictions.
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    18
    Only used to easily compare statistics between the old Sledgehammer algorithm and the new machine learning ones.
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    19
    '''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    20
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    21
    def __init__(self,mpPredictionFile):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    22
        '''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    23
        Constructor
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    24
        '''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    25
        self.predictionFile = mpPredictionFile
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    26
    
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    27
    def initializeModel(self,_trainData,dicts):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    28
        """
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    29
        Load predictions.
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    30
        """        
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    31
        self.predictions = {}
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    32
        IS = open(self.predictionFile,'r')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    33
        for line in IS:
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    34
            line = line.split(':')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    35
            name = line[0].strip()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    36
            predId = dicts.get_name_id(name)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    37
            line = line[1].split()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    38
            preds = [dicts.get_name_id(x.strip())for x in line]
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    39
            self.predictions[predId] = preds
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    40
        IS.close()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    41
        return dicts
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    42
    
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    43
    def update(self,dataPoint,features,dependencies):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    44
        """
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    45
        Updates the Model.
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    46
        """
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    47
        # No Update needed since we assume that we got all predictions
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    48
        pass
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    49
            
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    50
    
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    51
    def predict(self,problemId):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    52
        """
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    53
        Return the saved predictions.
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    54
        """
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    55
        return self.predictions[problemId] 
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    56
    
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    57
    def save(self,fileName):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    58
        OStream = open(fileName, 'wb')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    59
        dump((self.predictionFile,self.predictions),OStream)        
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    60
        OStream.close()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    61
        
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    62
    def load(self,fileName):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    63
        OStream = open(fileName, 'rb')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    64
        self.predictionFile,self.predictions = load(OStream)      
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    65
        OStream.close()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    66