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