src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
author blanchet
Mon, 26 Nov 2012 12:04:32 +0100
changeset 50220 90280d85cd03
child 50222 40e3c3be6bca
permissions -rwxr-xr-x
moved MaSh's Python code into Isabelle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50220
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     1
#!/usr/bin/python
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     2
'''
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     3
Created on Jul 13, 2012
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     4
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     5
@author: Daniel Kuehlwein
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     6
'''
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
import sys
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
     9
from argparse import ArgumentParser,RawDescriptionHelpFormatter
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    10
from matplotlib.pyplot import plot,figure,show,legend,xlabel,ylabel,axis,hist
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    11
from stats import Statistics
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
parser = ArgumentParser(description='Compare Statistics.  \n\n\
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    14
Loads different statistics and displays a comparison. Requires the matplotlib module.\n\n\
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    15
-------- Example Usage ---------------\n\
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    16
./compareStats.py --statFiles ../tmp/natISANB.stats ../tmp/natATPNB.stats -b 30\n\n\
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    17
Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    18
parser.add_argument('--statFiles', default=None, nargs='+', 
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    19
                    help='The names of the saved statistic files.')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    20
parser.add_argument('-b','--bins',default=50,help="Number of bins for the AUC histogram. Default=50.",type=int)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    21
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    22
def main(argv = sys.argv[1:]):
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    23
    args = parser.parse_args(argv)  
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    24
    if args.statFiles == None:
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    25
        print 'Filenames missing.'
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    26
        sys.exit(-1)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    27
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    28
    aucData = []
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    29
    aucLabels = []
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    30
    for statFile in args.statFiles:
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    31
        s = Statistics()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    32
        s.load(statFile)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    33
        avgRecall = [float(x)/s.problems for x in s.recallData]
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    34
        figure('Recall')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    35
        plot(range(s.cutOff),avgRecall,label=statFile)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    36
        legend(loc='lower right')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    37
        ylabel('Average Recall')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    38
        xlabel('Highest ranked premises')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    39
        axis([0,s.cutOff,0.0,1.0])
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    40
        figure('100%Recall')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    41
        plot(range(s.cutOff),s.recall100Data,label=statFile)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    42
        legend(loc='lower right')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    43
        ylabel('100%Recall')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    44
        xlabel('Highest ranked premises')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    45
        axis([0,s.cutOff,0,s.problems])
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    46
        aucData.append(s.aucData)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    47
        aucLabels.append(statFile)
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    48
    figure('AUC Histogram')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    49
    hist(aucData,bins=args.bins,label=aucLabels,histtype='bar')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    50
    legend(loc='upper left')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    51
    ylabel('Problems')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    52
    xlabel('AUC')
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    53
        
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    54
    show()
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    55
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    56
if __name__ == '__main__':
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    57
    #args = ['--statFiles','../tmp/natISANB.stats','../tmp/natATPNB.stats','-b','30']
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    58
    #sys.exit(main(args))
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    59
    sys.exit(main())
90280d85cd03 moved MaSh's Python code into Isabelle
blanchet
parents:
diff changeset
    60