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