1#!/usr/bin/env python2.7
2# ----------------------------------
3#
4# Usage: problem_classifyer.py <prot1> ... <protn>
5#
6# Read E protocols and return a suggested class for each proof problem
7# found.
8#
9# Copyright 2003 Stephan Schulz, schulz@informatik.tu-muenchen.de
10#
11# This code is part of the support structure for the equational
12# theorem prover E. Visit
13#
14#  http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
15#
16# for more information.
17#
18# This program is free software; you can redistribute it and/or modify
19# it under the terms of the GNU General Public License as published by
20# the Free Software Foundation; either version 2 of the License, or
21# (at your option) any later version.
22#
23# This program is distributed in the hope that it will be useful,
24# but WITHOUT ANY WARRANTY; without even the implied warranty of
25# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
26# GNU General Public License for more details.
27#
28# You should have received a copy of the GNU General Public License
29# along with this program ; if not, write to the Free Software
30# Foundation, Inc., 59 Temple Place, Suite 330, Boston,
31# MA  02111-1307 USA
32#
33# The original copyright holder can be contacted as
34#
35# Stephan Schulz (I4)
36# Technische Universitaet Muenchen
37# Institut fuer Informatik
38# Boltzmannstrasse 3
39# Garching bei Muenchen
40# Germany
41#
42# or via email (address above).
43
44import sys
45import re
46
47import pylib_io
48import pylib_eprots
49from pylib_discretize import *
50
51para_re  = re.compile("[0-9]+(\.[0-9]+)?")
52
53files   = pylib_io.get_args()
54options = pylib_io.get_options()
55formats = filter(lambda x:x[0:2]=="-r", options)
56stuff   = filter(lambda x:x[0:2]!="-r", options)
57
58protlist = pylib_eprots.eprot_set(files);
59
60for i in stuff:
61    if i=="-h"or i=="--help":
62        print """
63problem_classifier 0.1
64
65Usage: problem_classifier.py [-r<format1> ...-r<formatn>]  <protocols>
66
67Read a set of E protocols and suggest various assignments of protocols
68(i.e. heuristics) to proof problems. Only problems occurring in the
69best overal protocol are handled.
70
71Options:
72
73-r<format>: Select an algorithms for computing the
74            assignment.
75     Available:
76
77     const   : Each problem is assigned the globally best heuristic
78               that solves it.
79     equidist: Times are rounded to the nearest k seconds, each
80               problem is assigned the globally best heuristic that
81               solves it in minimal time.
82     prop    : Times are rounded to the nearest [1,2,5]*10^X, each
83               problem is assigned the globally best heuristic that
84               solves it in minimal time.
85     log     : Times are rounded to the nearest k*2^X, each
86               problem is assigned the globally best heuristic that
87               solves it in minimal time.
88     none    : Each problem is assigned the globally best heuristic
89               that solves it in minimal time.
90
91equidist and log accept an numeric argument for k, e.g. -rlog0.5 or
92-requidist10.
93
94Suggestions are preceded by an mnemonic string denoting the algorithm
95and a colon, so you can grep and cut suitable results out. Parsing is
96expensive, computing assignments is cheap, so it makes sense to
97compute all assignments at once. Other output fields are problem name,
98status, and suggested class.
99
100If no -r option is given, uses prop algorithm, but ommits mnemonic
101strings.
102"""
103        sys.exit(1)
104
105def get_param(option, default):
106    mr = para_re.search(option)
107    if mr:
108        tmp = mr.group()
109        try:
110            res = int(tmp)
111        except ValueError:
112            res = float(tmp)
113        return res
114    return default
115
116if len(formats) == 0:
117    res = protlist.make_classification(prop_round)
118    res.printout()
119else:
120    for o in formats:
121        if o.startswith("-rconst"):
122            res = protlist.make_classification(const_round)
123            res.printout("const :")
124        elif o.startswith("-rprop"):
125            res = protlist.make_classification(prop_round)
126            res.printout("prop  : ")
127        elif o.startswith("-rlog"):
128            res = protlist.make_classification(log_round(get_param(o, 0.5)))
129            res.printout("log%02d :" % get_param(o, 5))
130        elif o.startswith("-requidist"):
131            res = protlist.make_classification(equidist_round(get_param(o, 5)))
132            res.printout("equi%02d:" % get_param(o, 5))
133        elif o.startswith("-rnone"):
134            res = protlist.make_classification(no_round)
135            res.printout("none  :")
136        else:
137            raise pylib_io.UsageErrorException
138
139
140
141
142