1#!/usr/bin/env python2.7
2
3import sys
4import re
5import string
6
7pick_by_global_performance = True
8optimize_large_class_limit = 200
9
10white_space     = re.compile('\s+')
11trail_space     = re.compile('\s*$')
12arg_term        = re.compile('\s|$')
13full_comment    = re.compile('^#')
14dash            = re.compile('-')
15slash           = re.compile('/')
16match_heuristic = re.compile("-H'?\([^#]*\)'?")
17match_class     = re.compile('CLASS_[a-zA-Z-0-9]*$')
18eval_f_sep      = re.compile('\),')
19problem_ext     = re.compile('\.[a-z]*$')
20
21
22class StratPerf(object):
23    """
24    A class holding the performance of a strategy on a set of
25    problems.
26    """
27    def __init__(self, strat_name):
28        self.strat_name = strat_name
29        self.problems   = {}
30        self.solutions  = 0
31        self.soln_time  = 0.0
32
33    def addProblem(self, prob, status, time):
34        self.problems[prob] = status, time
35
36    def delProblem(self, prob):
37        try:
38            del self.problems[prob]
39        except KeyError:
40            pass
41            #print "Warning: Tried to remove unknown problem "+prob+" from "+self.strat_name
42
43    def getName(self):
44        return self.strat_name
45
46    def isSuccess(self, prob, time_limit, succ_status):
47        status, time = self.problems[prob]
48        return (status in succ_status and time<=time_limit)
49
50    def getCardinality(self):
51        """
52        Return number of problems in the object.
53        """
54        return len(self.problems)
55
56    def getSuccesses(self, time_limit, succ_status):
57        return [(i, self.problems[i]) for i in self.problems if self.isSuccess(i,time_limit, succ_status)]
58
59    def getPerf(self):
60        """
61        Return currently stored performance.
62        """
63        return (self.solutions, self.soln_time)
64
65    def computePerf(self, time_limit, succ_status):
66        """
67        Update and return performance data.
68        """
69        self.solutions  = 0
70        self.soln_time  = 0.0
71        for prob in self.problems:
72            status, time = self.problems[prob]
73            if (status in succ_status) and (time<=time_limit):
74                self.solutions += 1
75                self.soln_time += time
76        return self.getPerf()
77
78    def removeOtherSuccesses(self, other, time_limit, succ_status):
79        """
80        Remove all problems that are solved in other (given the time
81        limit) from self.
82        """
83        for prob in other.problems:
84            if other.isSuccess(prob):
85                self.delProblem(prob)
86
87
88
89class ClassPerf(object):
90    """
91    A class associating with the name of a class the data of several
92    strategies on this class.
93    """
94    def __init__(self, classname):
95        self.name   = classname
96        self.strats = {}
97
98    def addProblem(self, strat_name, prob, status, time):
99        """
100        Add data for one problem from one strategy to the performance
101        object.
102        """
103        if not strat_name in self.strats:
104            set = StratPerf(strat_name)
105            self.strats[strat_name] = set
106        else:
107            set = self.strats[strat_name]
108
109        set.addProblem(prob, status, time)
110
111    def delProblem(self, prob):
112        """
113        Remove data for a problem from all class performance objects.
114        """
115        for k in self.strats.values():
116            k.delProblem(prob)
117
118    def getCardinality(self):
119        """
120        Return number of strategies in the object.
121        """
122        return len(self.strats)
123
124    def computePerf(self, time_limit, succ_status):
125        for i in self.strats.values():
126            i.computePerf(time_limit, succ_status)
127
128    def delStrat(self, strat_name):
129        try:
130            del self.strats[strat_name]
131            return True
132        except KeyError:
133            return False
134
135    def getStrat(self, strat_name):
136        return self.strats[strat_name]
137
138    def getBestStrat(self):
139        solutions = 0
140        soln_time = 1
141        res = None
142        for i in self.strats.values():
143            newsol, newtime = i.getPerf()
144            if (newsol > solutions) or \
145               ((newsol == solutions) and (newtime < soln_time)):
146                solutions = newsol
147                soln_time = newtime
148                res = i.getName()
149        return res, solutions
150
151
152
153def print_dict_lines(dict):
154    for i in dict.keys():
155        print repr(i)+" : "+repr(dict[i])
156
157def print_result(fp, result, opt_res):
158    for i in result.keys():
159        cl  = result[i]
160        res = opt_res[i]
161        fp.write("/* %(i)-17s : %(cl)-30s %(res)-4d */\n" % vars())
162
163
164def print_list_lines(l):
165    for i in xrange(0, len(l)):
166        print l[i]
167
168def compute_problem_stem(key):
169    mr = problem_ext.search(key)
170    if not mr:
171        raise RuntimeError, "Problem name has no extension (?!?) <" + key+">"
172    res = key[0:mr.start()]
173    return res;
174
175# Parse a class file into the problems dictionary, return class size
176#
177# Arguments: File name
178#            Internal name of the class
179#            Dictionary where the problems are stored
180
181def parse_class(c, key, probs):
182    sys.stderr.write("Parsing " + c + " as " + key + "\n")
183    i=0
184    p=open(c,'r')
185    for l in p:
186        l=l[:-1]
187        probs[compute_problem_stem(l)] = key
188        i=i+1
189    p.close
190    return i
191
192def tuple_add2(t1,t2):
193    return (t1[0]+t2[0],t1[1]+t2[1])
194
195def parse_prot(filename, stratname, matrix, succ_cases, time_limit):
196    """
197    Parse the given file with the given strategy name.
198    """
199    sys.stderr.write("Parsing " + stratname + "\n")
200    p=open(filename,'r')
201    l=p.readline()[:-1]
202    desc = "";
203    while l:
204        res = full_comment.match(l)
205        if(res):
206            desc = desc+l
207        else:
208            clean = re.sub(trail_space,'',l)
209            tuple=re.split(white_space,clean)
210            prob = compute_problem_stem(tuple[0]);
211            if (problems.has_key(prob)):
212                time=float(tuple[2])
213                if (tuple[1] in succ_cases) and time<=time_limit:
214                    cl=problems[prob]
215                    old = matrix[cl][stratname]
216                    matrix[cl][stratname]=tuple_add2(old,(1,time))
217                    old = stratperf[stratname];
218                    stratperf[stratname] = tuple_add2(old,(1,time))
219        l=p.readline()
220    p.close()
221    return desc
222
223def parse_prot_new(filename, stratname, prob_assoc, global_class, classdata):
224    """
225    Parse the given file with the given strategy name.
226    """
227    sys.stderr.write("NewParsing " + stratname + "\n")
228    p=open(filename,'r')
229    desc = ""
230    for l in p:
231        res = full_comment.match(l)
232        if(res):
233            desc = desc+l
234        else:
235            clean  = re.sub(trail_space,'',l)
236            tuple  = re.split(white_space,clean)
237            prob   = compute_problem_stem(tuple[0]);
238            try:
239                time   = float(tuple[2])
240            except ValueError:
241                time = 10000
242            status = tuple[1]
243            try:
244                classdata[prob_assoc[prob]].addProblem(stratname, prob, status, time)
245                global_class.addProblem(stratname, prob, status, time)
246            except KeyError:
247                print "Unclassified problem ", prob
248    p.close()
249    return desc
250
251
252
253
254def eval_heuristic(classes,heuristic):
255    res=(0.0,0.0)
256    for i in classes:
257        res=tuple_add2(res,matrix[i][heuristic])
258    return res;
259
260def tuple_is_better2(t1,t2):
261    tmpres = t1[0]>t2[0] or (t1[0]==t2[0] and t1[1]<t2[1])
262    return tmpres
263
264def find_optimal_heuristic(classes, exclude):
265    res  = ""
266    eval = (-1.0,0.0)
267    for i in stratset.keys():
268        if not i in exclude:
269            tmp = eval_heuristic(classes, i)
270            if tuple_is_better2(tmp, eval):
271                eval = tmp;
272                res  = i
273    return res
274
275def find_covered(heuristic,classes):
276    res = []
277    for i in classes:
278        if matrix[i][heuristic][0]==opt_res[i]:
279            res.append(i)
280    return res
281
282def compare_strat_global(strat1, strat2):
283    eval1 = stratperf[strat1]
284    eval2 = stratperf[strat2]
285    if eval1[0] > eval2[0]:
286        return -1
287    if eval1[0] < eval2[0]:
288        return 1
289    if eval1[1] > eval2[1]:
290        return 1
291    if eval1[1] < eval2[1]:
292        return -1
293    return 0
294
295
296def translate_class(cl, opt_res):
297    solved = repr(opt_res[cl])
298    res = "      ( /* "+cl+" Solved: "+solved+ " of " +repr(classsize[cl]) + " */\n"
299    pref = "       ";
300    for i in xrange(6,len(cl)):
301        if cl[i]!="-":
302            res = res+pref+"Spec"+class_int[i][cl[i]]+"(spec)"
303            pref = "&&\n       "
304    res = res+")"
305    return res;
306
307def translate_class_list(cl, opt_res):
308    res = "";
309    pref = "";
310    for i in cl:
311        res = res+pref+translate_class(i, opt_res)+"\n"
312        pref = "       ||\n"
313    return res[0:-1];
314
315def trans_heuristic_name(name):
316    tmp = re.sub('p[^_]*_', "", name);
317    tmp = re.sub(dash,"_", tmp)
318    tmp = re.sub('[.]csv',"", tmp)
319    return tmp
320
321
322def heuristic_define(name):
323    mr = match_heuristic.search(stratdesc[name])
324    if not mr:
325        raise RuntimeError, "No heuristic defined in " + name;
326    res= '"' + trans_heuristic_name(name) + ' = \\n"\n"'
327    tmp = stratdesc[name][mr.start()+2:mr.end()]
328    tmp = re.sub("'", "", tmp);
329    res=res+ re.sub(eval_f_sep,'),"\n" ',tmp) +'\\n"'
330
331    return res
332
333def extract_arg(line, mopt):
334    l = line[mopt.end():]
335    m = arg_term.search(l)
336    res = l[0:m.start()]
337
338    if res == "":
339        raise RuntimeError, "Argument to option in command line missing: "+line[mopt.start():]
340
341    return res
342
343match_ac_l      = re.compile(" --ac-handling=")
344match_acnag_l   = re.compile(" --ac-non-aggressive")
345match_litsel_s  = re.compile(" -W *")
346match_litsel_l  = re.compile(" --literal-selection-strategy=")
347match_op_l      = re.compile(" --select-on-processing-only")
348match_ipl_s     = re.compile(" -i")
349match_ipl_l     = re.compile(" --inherit-paramod-literals")
350match_ipg_s     = re.compile(" -j")
351match_ipg_l     = re.compile(" --inherit-goal-pm-literals")
352match_ipc_l     = re.compile(" --inherit-conjecture-pm-literals")
353match_pic_l     = re.compile(" --prefer-initial-clauses")
354match_split_l   = re.compile(" --split-clauses=")
355match_splitm_l  = re.compile(" --split-method=")
356match_splita_l  = re.compile(" --split-aggressive")
357match_splitr_l  = re.compile(" --split-reuse-defs")
358match_der_l     = re.compile(" --destructive-er")
359match_sder_l    = re.compile(" --strong-destructive-er")
360match_dera_l    = re.compile(" --destructive-er-aggressive")
361match_demod_s   = re.compile(" -F *")
362match_demod_l   = re.compile(" --forward_demod_level=")
363match_snm_l     = re.compile(" --selection-neg-min=")
364match_g_demod_s = re.compile(" --prefer-general-demodulators")
365match_g_demod_l = re.compile(" -g")
366match_unproc_s  = re.compile(" --simplify-with-unprocessed-units=")
367match_unproc_sd = re.compile(" --simplify-with-unprocessed-units")
368match_fcsr      = re.compile(" --forward-context-sr")
369match_fcsra     = re.compile(" --forward-context-sr-aggressive")
370match_bcsr      = re.compile(" --backward-context-sr")
371match_simul_pm  = re.compile("--simul-paramod");
372match_osimul_pm = re.compile("--oriented-simul-paramod");
373match_presat_ir = re.compile("--presat-simplify");
374match_sos_types = re.compile("--sos-uses-input-types");
375match_condense  = re.compile("--condense");
376match_condag    = re.compile("--condense-aggressive");
377
378
379
380def parse_control_info(line):
381    res = ""
382
383
384    #
385    # AC handling and misc. stuff
386    #
387    m = match_ac_l.search(line)
388    if m:
389        arg = extract_arg(line, m)
390        res = res+ "      control->heuristic_parms.ac_handling="+ac_handling[arg]+";\n"
391
392    m = match_acnag_l.search(line)
393    if m:
394        res = res+ "      control->heuristic_parms.ac_res_aggressive=false;\n"
395
396    m = match_pic_l.search(line)
397    if m:
398        res = res+ "      control->heuristic_parms.prefer_initial_clauses=true;\n"
399
400    m = match_unproc_s.search(line)
401    if m:
402        arg = extract_arg(line, m)
403        res = res+ "      control->heuristic_parms.unproc_simplify="+unproc_simpl[arg]+";\n"
404    else:
405        m = match_unproc_sd.search(line)
406        if m:
407            res = res+ "      control->heuristic_parms.unproc_simplify=TopLevelUnitSimplify;\n"
408
409    #
410    # Contextual simplify-reflect
411    #
412
413    m = match_fcsr.search(line)
414    if m:
415        res = res+ "      control->heuristic_parms.forward_context_sr = true;\n"
416
417    m = match_fcsra.search(line)
418    if m:
419        res = res+ "      control->heuristic_parms.forward_context_sr = true;\n"
420        res = res+ "      control->heuristic_parms.forward_context_sr_aggressive = true;\n"
421
422    m = match_bcsr.search(line)
423    if m:
424        res = res+ "      control->heuristic_parms.backward_context_sr = true;\n"
425
426    #
427    # Literal selection parameters
428    #
429    m = match_litsel_s.search(line)
430    if m:
431        arg = extract_arg(line, m)
432        res = res+ "      control->heuristic_parms.selection_strategy="+selstrat[arg]+";\n"
433
434    m = match_litsel_l.search(line)
435    if m:
436        arg = extract_arg(line, m)
437        res = res+ "      control->heuristic_parms.selection_strategy="+selstrat[arg]+";\n"
438
439    m = match_op_l.search(line)
440    if m:
441        res = res+ "      control->heuristic_parms.select_on_proc_only=true;\n"
442
443    m = match_ipl_s.search(line)
444    if m:
445        res = res+ "      control->heuristic_parms.inherit_paramod_lit=true;\n"
446
447    m = match_ipl_l.search(line)
448    if m:
449        res = res+ "      control->heuristic_parms.inherit_paramod_lit=true;\n"
450
451    m = match_ipg_s.search(line)
452    if m:
453        res = res+ "      control->heuristic_parms.inherit_goal_pm_lit=true;\n"
454
455    m = match_ipg_l.search(line)
456    if m:
457        res = res+ "      control->heuristic_parms.inherit_goal_pm_lit=true;\n"
458
459    m = match_ipc_l.search(line)
460    if m:
461        res = res+ "      control->heuristic_parms.inherit_conj_pm_lit=true;\n"
462
463    m = match_snm_l.search(line)
464    if m:
465        arg = extract_arg(line, m)
466        res = res+ "      control->heuristic_parms.neg_lit_sel_min="+arg+";\n"
467
468    #
469    # Splitting parameters
470    #
471    m = match_split_l.search(line)
472    if m:
473        arg = extract_arg(line, m)
474        res = res+ "      control->heuristic_parms.split_clauses="+arg+";\n"
475
476    m = match_splitm_l.search(line)
477    if m:
478        arg = extract_arg(line, m)
479        res = res+ "      control->heuristic_parms.split_method="+arg+";\n"
480
481    m = match_splita_l.search(line)
482    if m:
483        res = res+ "      control->heuristic_parms.split_aggressive=true;\n"
484
485    m = match_splitr_l.search(line)
486    if m:
487        res = res+ "      control->heuristic_parms.split_fresh_defs=false;\n"
488
489    #
490    # Destructive equality resolution parameters
491    #
492    m = match_der_l.search(line)
493    if m:
494        res = res+ "      control->heuristic_parms.er_varlit_destructive=true;\n"
495
496    m = match_sder_l.search(line)
497    if m:
498        res = res+ "      control->heuristic_parms.er_strong_destructive=true;\n"
499        res = res+ "      control->heuristic_parms.er_varlit_destructive=true;\n"
500
501    m = match_dera_l.search(line)
502    if m:
503        res = res+ "      control->heuristic_parms.er_aggressive=true;\n"
504
505    #
506    # Rewriting parameters
507    #
508    m = match_demod_s.search(line)
509    if m:
510        arg = extract_arg(line, m)
511        res = res+ "      control->heuristic_parms.forward_demod="+arg+";\n"
512
513    m = match_demod_l.search(line)
514    if m:
515        arg = extract_arg(line, m)
516        res = res+ "      control->heuristic_parms.forward_demod="+arg+";\n"
517
518    m = match_g_demod_s.search(line)
519    if m:
520        res = res+ "      control->heuristic_parms.prefer_general=true;\n"
521
522    m = match_g_demod_l.search(line)
523    if m:
524        res = res+ "      control->heuristic_parms.prefer_general=true;\n"
525
526    #
527    # Paramodulation
528    #
529    m = match_simul_pm.search(line)
530    if m:
531        res = res+ "      control->heuristic_parms.pm_type=ParamodAlwaysSim;\n"
532
533    m = match_osimul_pm.search(line)
534    if m:
535        res = res+ "      control->heuristic_parms.pm_type=ParamodOrientedSim;\n"
536
537    #
538    # Presaturation simplification
539    #
540    m = match_presat_ir.search(line)
541    if m:
542        res = res+ "      control->heuristic_parms.presat_interreduction=true;\n"
543
544    #
545    # Set of Support determination
546    #
547    m = match_sos_types.search(line)
548    if m:
549        res = res+ "      control->heuristic_parms.use_tptp_sos=true;\n"
550
551    #
552    # Condensation
553    #
554    m = match_condense.search(line)
555    if m:
556        res = res+ "      control->heuristic_parms.condensing=true;\n"
557
558    m = match_condag.search(line)
559    if m:
560        res = res+ "      control->heuristic_parms.condensing_aggressive=true;\n"
561
562
563
564    return res
565
566
567match_sine = re.compile(" --sine=")
568
569def parse_sine(line):
570    m = match_sine.search(line)
571    if m:
572        arg = extract_arg(line, m)
573        return arg
574    else:
575        return None
576
577
578#
579# Regular expressions for ordering related stuff.
580#
581
582match_rlc_l = re.compile(" --restrict-literal-comparisons")
583match_to_s  = re.compile(" -t *")
584match_to_l  = re.compile(" --term-ordering=")
585match_tow_s = re.compile(" -w *")
586match_tow_l = re.compile(" --order-weight-generation=")
587match_top_s = re.compile(" -G *")
588match_top_l = re.compile(" --order-precedence-generation=")
589match_ocw_l = re.compile(" --order-constant-weight=")
590match_ocw_s = re.compile(" -c *")
591match_prc_l = re.compile(" --precedence=")
592
593def parse_ordering_info(line):
594    res = ""
595
596    m = match_rlc_l.search(line)
597    if m:
598        res = res+ "      oparms.no_lit_cmp=true;\n"
599
600    m = match_to_s.search(line)
601    if m:
602        arg = extract_arg(line, m)
603        res = res+ "      oparms.ordertype="+ordering[arg]+";\n"
604
605    m = match_to_l.search(line)
606    if m:
607        arg = extract_arg(line, m)
608        res = res+ "      oparms.ordertype="+ordering[arg]+";\n"
609
610    m = match_tow_s.search(line)
611    if m:
612        arg = extract_arg(line, m)
613        res = res+ "      oparms.to_weight_gen="+weight_gen[arg]+";\n"
614
615    m = match_tow_l.search(line)
616    if m:
617        arg = extract_arg(line, m)
618        res = res+ "      oparms.to_weight_gen="+weight_gen[arg]+";\n"
619
620    m = match_top_s.search(line)
621    if m:
622        arg = extract_arg(line, m)
623        res = res+ "      oparms.to_prec_gen="+prec_gen[arg]+";\n"
624
625    m = match_top_l.search(line)
626    if m:
627        arg = extract_arg(line, m)
628        res = res+ "      oparms.to_prec_gen="+prec_gen[arg]+";\n"
629    m = match_ocw_s.search(line)
630    if m:
631        arg = extract_arg(line, m)
632        res = res+ "      oparms.to_const_weight="+arg+";\n"
633    m = match_top_l.search(line)
634    if m:
635        arg = extract_arg(line, m)
636        res = res+ "      oparms.to_const_weight"+arg+";\n"
637#    m = match_prc_l.search(line)
638#    if m:
639#        arg = extract_arg(line, m)
640#        if arg != "":
641#            raise RuntimeError, "Can only handle empty precedence "+arg
642#       res = res+ "      oparms.to_prec_gen=";\n"
643
644    return res
645
646
647#------------------------------------------------------------------
648# Begin data section
649#------------------------------------------------------------------
650
651class_int={
652    6: {"U": "AxiomsAreUnit", "H": "AxiomsAreNonUnitHorn", "G": "AxiomsAreGeneral"},
653    7: {"U": "GoalsAreUnit", "H": "GoalsAreHorn", "G": "GoalsAreGeneral"},
654    8: {"N": "NoEq", "S": "SomeEq", "P": "PureEq"},
655    9: {"F": "FewNGPosUnits", "S": "SomeNGPosUnits", "M": "ManyNGPosUnits"},
656    10:{"N": "GoalsHaveVars", "G": "GoalsAreGround"},
657    11:{"F": "FewAxioms", "S": "SomeAxioms", "M": "ManyAxioms"},
658    12:{"F": "FewLiterals", "S": "SomeLiterals", "M": "ManyLiterals"},
659    13:{"S": "SmallTerms", "M": "MediumTerms", "L": "LargeTerms"},
660    14:{"F": "FewGroundPos", "S": "SomeGroundPos", "M": "ManyGroundPos"},
661    15:{"0": "MaxFArity0", "1": "MaxFArity1", "2": "MaxFArity2","3": "MaxFArity3Plus"},
662    16:{"0": "AvgFArity0", "1": "AvgFArity1", "2": "AvgFArity2","3": "AvgFArity3Plus"},
663    17:{"S": "SmallFArSum", "M": "MediumFArSum", "L": "LargeFArSum"},
664    18:{"S": "ShallowMaxDepth", "M": "MediumMaxDepth", "D": "DeepMaxDepth"}
665}
666
667selstrat={
668   "NoSelection"                        : "SelectNoLiterals",
669   "NoGeneration"                       : "SelectNoGeneration",
670   "SelectNegativeLiterals"             : "SelectNegativeLiterals",
671   "PSelectNegativeLiterals"            : "PSelectNegativeLiterals",
672   "SelectPureVarNegLiterals"           : "SelectFirstVariableLiteral",
673   "PSelectPureVarNegLiterals"          : "PSelectFirstVariableLiteral",
674   "SelectLargestNegLit"                : "SelectLargestNegativeLiteral",
675   "PSelectLargestNegLit"               : "PSelectLargestNegativeLiteral",
676   "SelectSmallestNegLit"               : "SelectSmallestNegativeLiteral",
677   "PSelectSmallestNegLit"              : "PSelectSmallestNegativeLiteral",
678   "SelectLargestOrientable"            : "SelectLargestOrientableLiteral",
679   "PSelectLargestOrientable"           : "PSelectLargestOrientableLiteral",
680   "MSelectLargestOrientable"           : "MSelectLargestOrientableLiteral",
681   "SelectSmallestOrientable"           : "SelectSmallestOrientableLiteral",
682   "PSelectSmallestOrientable"          : "PSelectSmallestOrientableLiteral",
683   "MSelectSmallestOrientable"          : "MSelectSmallestOrientableLiteral",
684   "SelectDiffNegLit"                   : "SelectDiffNegativeLiteral",
685   "PSelectDiffNegLit"                  : "PSelectDiffNegativeLiteral",
686   "SelectGroundNegLit"                 : "SelectGroundNegativeLiteral",
687   "PSelectGroundNegLit"                : "PSelectGroundNegativeLiteral",
688   "SelectOptimalLit"                   : "SelectOptimalLiteral",
689   "PSelectOptimalLit"                  : "PSelectOptimalLiteral",
690   "SelectMinOptimalLit"                : "SelectMinOptimalLiteral",
691   "PSelectMinOptimalLit"               : "PSelectMinOptimalLiteral",
692   "SelectMinOptimalNoTypePred"         : "SelectMinOptimalNoTypePred",
693   "PSelectMinOptimalNoTypePred"        : "PSelectMinOptimalNoTypePred",
694   "SelectMinOptimalNoXTypePred"        : "SelectMinOptimalNoXTypePred",
695   "PSelectMinOptimalNoXTypePred"       : "PSelectMinOptimalNoXTypePred",
696   "SelectMinOptimalNoRXTypePred"       : "SelectMinOptimalNoRXTypePred",
697   "PSelectMinOptimalNoRXTypePred"      : "PSelectMinOptimalNoRXTypePred",
698   "SelectCondOptimalLit"               : "SelectCondOptimalLiteral",
699   "PSelectCondOptimalLit"              : "PSelectCondOptimaslLiteral",
700   "SelectAllCondOptimalLit"            : "SelectAllCondOptimalLiteral",
701   "PSelectAllCondOptimalLit"           : "PSelectAllCondOptimalLiteral",
702   "SelectOptimalRestrDepth2"           : "SelectDepth2OptimalLiteral",
703   "PSelectOptimalRestrDepth2"          : "PSelectDepth2OptimalLiteral",
704   "SelectOptimalRestrPDepth2"          : "SelectPDepth2OptimalLiteral",
705   "PSelectOptimalRestrPDepth2"         : "PSelectPDepth2OptimalLiteral",
706   "SelectOptimalRestrNDepth2"          : "SelectNDepth2OptimalLiteral",
707   "PSelectOptimalRestrNDepth2"         : "PSelectNDepth2OptimalLiteral",
708   "SelectNonRROptimalLit"              : "SelectNonRROptimalLiteral",
709   "PSelectNonRROptimalLit"             : "PSelectNonRROptimalLiteral",
710   "SelectNonStrongRROptimalLit"        : "SelectNonStrongRROptimalLiteral",
711   "PSelectNonStrongRROptimalLit"       : "PSelectNonStrongRROptimalLiteral",
712   "SelectAntiRROptimalLit"             : "SelectAntiRROptimalLiteral",
713   "PSelectAntiRROptimalLit"            : "PSelectAntiRROptimalLiteral",
714   "SelectNonAntiRROptimalLit"          : "SelectNonAntiRROptimalLiteral",
715   "PSelectNonAntiRROptimalLit"         : "PSelectNonAntiRROptimalLiteral",
716   "SelectStrongRRNonRROptimalLit"      : "SelectStrongRRNonRROptimalLiteral",
717   "PSelectStrongRRNonRROptimalLit"     : "PSelectStrongRRNonRROptimalLiteral",
718   "SelectUnlessUniqMax"                : "SelectUnlessUniqMaxOptimalLiteral",
719   "PSelectUnlessUniqMax"               : "PSelectUnlessUniqMaxOptimalLiteral",
720   "SelectUnlessPosMax"                 : "SelectUnlessPosMaxOptimalLiteral",
721   "PSelectUnlessPosMax"                : "PSelectUnlessPosMaxOptimalLiteral",
722   "SelectUnlessUniqPosMax"             : "SelectUnlessUniqPosMaxOptimalLiteral",
723   "PSelectUnlessUniqPosMax"            : "PSelectUnlessUniqPosMaxOptimalLiteral",
724   "SelectUnlessUniqMaxPos"             : "SelectUnlessUniqMaxPosOptimalLiteral",
725   "PSelectUnlessUniqMaxPos"            : "PSelectUnlessUniqMaxPosOptimalLiteral",
726   "SelectComplex"                      : "SelectComplex",
727   "PSelectComplex"                     : "PSelectComplex",
728   "SelectComplexExceptRRHorn"          : "SelectComplexExceptRRHorn",
729   "PSelectComplexExceptRRHorn"         : "PSelectComplexExceptRRHorn",
730   "SelectLComplex"                     : "SelectLComplex",
731   "PSelectLComplex"                    : "PSelectLComplex",
732   "SelectMaxLComplex"                  : "SelectMaxLComplex",
733   "PSelectMaxLComplex"                 : "PSelectMaxLComplex",
734   "SelectMaxLComplexNoTypePred"        : "SelectMaxLComplexNoTypePred",
735   "PSelectMaxLComplexNoTypePred"       : "PSelectMaxLComplexNoTypePred",
736   "SelectMaxLComplexNoXTypePred"       : "SelectMaxLComplexNoXTypePred",
737   "PSelectMaxLComplexNoXTypePred"      : "PSelectMaxLComplexNoXTypePred",
738   "SelectComplexPreferNEQ"             : "SelectComplexPreferNEQ",
739   "PSelectComplexPreferNEQ"            : "PSelectComplexPreferNEQ",
740   "SelectComplexPreferEQ"              : "SelectComplexPreferEQ",
741   "PSelectComplexPreferEQ"             : "PSelectComplexPreferEQ",
742   "SelectComplexExceptUniqMaxHorn"     : "SelectComplexExceptUniqMaxHorn",
743   "PSelectComplexExceptUniqMaxHorn"    : "PSelectComplexExceptUniqMaxHorn",
744   "MSelectComplexExceptUniqMaxHorn"    : "MSelectComplexExceptUniqMaxHorn",
745   "SelectNewComplex"                   : "SelectNewComplex",
746   "PSelectNewComplex"                  : "PSelectNewComplex",
747   "SelectNewComplexExceptUniqMaxHorn"  : "SelectNewComplexExceptUniqMaxHorn",
748   "PSelectNewComplexExceptUniqMaxHorn" : "PSelectNewComplexExceptUniqMaxHorn",
749   "SelectMinInfpos"                    : "SelectMinInfpos",
750   "PSelectMinInfpos"                   : "PSelectMinInfpos",
751   "HSelectMinInfpos"                   : "HSelectMinInfpos",
752   "GSelectMinInfpos"                   : "GSelectMinInfpos",
753   "SelectMinInfposNoTypePred"          : "SelectMinInfposNoTypePred",
754   "PSelectMinInfposNoTypePred"         : "PSelectMinInfposNoTypePred",
755   "SelectMin2Infpos"                   : "SelectMin2Infpos",
756   "PSelectMin2Infpos"                  : "PSelectMin2Infpos",
757   "SelectComplexExceptUniqMaxPosHorn"  : "SelectComplexExceptUniqMaxPosHorn",
758   "PSelectComplexExceptUniqMaxPosHorn" : "PSelectComplexExceptUniqMaxPosHorn",
759   "SelectUnlessUniqMaxSmallestOrientable" : "SelectUnlessUniqMaxSmallestOrientable",
760   "PSelectUnlessUniqMaxSmallestOrientable": "PSelectUnlessUniqMaxSmallestOrientable",
761   "SelectDivLits"                      : "SelectDiversificationLiterals",
762   "SelectDivPreferIntoLits"            : "SelectDiversificationPreferIntoLiterals",
763   "SelectMaxLComplexG"                 : "SelectMaxLComplexG",
764
765   "SelectMaxLComplexAvoidPosPred"      : "SelectMaxLComplexAvoidPosPred",
766   "SelectMaxLComplexAPPNTNp"           : "SelectMaxLComplexAPPNTNp",
767   "SelectMaxLComplexAvoidPosUPred"     : "SelectMaxLComplexAvoidPosUPred",
768   "SelectComplexG"                     : "SelectComplexG",
769
770   "SelectComplexAHP"                   : "SelectComplexAHP",
771   "PSelectComplexAHP"                  : "PSelectComplexAHP",
772
773   "SelectNewComplexAHP"                : "SelectNewComplexAHP",
774   "PSelectNewComplexAHP"               : "PSelectNewComplexAHP",
775
776   "SelectComplexAHPExceptRRHorn"       : "SelectComplexAHPExceptRRHorn",
777   "PSelectComplexAHPExceptRRHorn"      : "PSelectComplexAHPExceptRRHorn",
778
779   "SelectNewComplexAHPExceptRRHorn"       : "SelectNewComplexAHPExceptRRHorn",
780   "PSelectNewComplexAHPExceptRRHorn"      : "PSelectNewComplexAHPExceptRRHorn",
781
782   "SelectNewComplexAHPExceptUniqMaxHorn" : "SelectNewComplexAHPExceptUniqMaxHorn",
783   "PSelectNewComplexAHPExceptUniqMaxHorn": "PSelectNewComplexAHPExceptUniqMaxHorn",
784
785   "SelectNewComplexAHPNS"              : "SelectNewComplexAHPNS",
786   "SelectVGNonCR"                      : "SelectVGNonCR",
787
788   "SelectCQArEqLast"                   : "SelectCQArEqLast",
789   "SelectCQArEqFirst"                  : "SelectCQArEqFirst",
790   "SelectCQIArEqLast"                  : "SelectCQIArEqLast",
791   "SelectCQIArEqFirst"                 : "SelectCQIArEqFirst",
792   "SelectCQAr"                         : "SelectCQAr",
793   "SelectCQIAr"                        : "SelectCQIAr",
794   "SelectCQArNpEqFirst"                : "SelectCQArNpEqFirst",
795   "SelectCQIArNpEqFirst"               : "SelectCQIArNpEqFirst",
796   "SelectGrCQArEqFirst"                : "SelectGrCQArEqFirst",
797   "SelectCQGrArEqFirst"                : "SelectCQGrArEqFirst",
798   "SelectCQArNTEqFirst"                : "SelectCQArNTEqFirst",
799   "SelectCQIArNTEqFirst"               : "SelectCQIArNTEqFirst",
800   "SelectCQArNTNpEqFirst"              : "SelectCQArNTNpEqFirst",
801   "SelectCQIArNTNpEqFirst"             : "SelectCQIArNTNpEqFirst",
802   "SelectCQArNXTEqFirst"               : "SelectCQArNXTEqFirst",
803   "SelectCQIArNXTEqFirst"              : "SelectCQIArNXTEqFirst",
804
805   "SelectCQArNTNp"                     :  "SelectCQArNTNp",
806   "SelectCQIArNTNp"                    :  "SelectCQIArNTNp",
807   "SelectCQArNT"                       :  "SelectCQArNT",
808   "SelectCQIArNT"                      :  "SelectCQIArNT",
809   "SelectCQArNp"                       :  "SelectCQArNp",
810   "SelectCQIArNp"                      :  "SelectCQIArNp",
811
812   "SelectCQArNpEqFirstUnlessPDom"      : "SelectCQArNpEqFirstUnlessPDom",
813   "SelectCQArNTEqFirstUnlessPDom"      : "SelectCQArNTEqFirstUnlessPDom",
814
815   "SelectCQPrecW"                      : "SelectCQPrecW",
816   "SelectCQIPrecW"                     : "SelectCQIPrecW",
817   "SelectCQPrecWNTNp"                  : "SelectCQPrecWNTNp",
818   "SelectCQIPrecWNTNp"                 : "SelectCQIPrecWNTNp"
819}
820
821
822
823
824ac_handling ={
825    "None"          : "NoACHandling",
826    "DiscardAll"    : "ACDiscardAll",
827    "KeepUnits"     : "ACKeepUnits",
828    "KeepOrientable": "ACKeepOrientable"
829}
830
831ordering={
832    "LPO" :"LPO",
833    "LPO4":"LPO4",
834    "KBO" :"KBO",
835    "KBO6":"KBO6",
836    "KBO1":"KBO"
837}
838
839weight_gen={
840   "none"               : "WNoMethod",
841   "firstmaximal0"      : "WSelectMaximal",
842   "arity"              : "WArityWeight ",
843   "aritymax0"          : "WArityMax0",
844   "modarity"           : "WModArityWeight",
845   "modaritymax0"       : "WModArityMax0",
846   "aritysquared"       : "WAritySqWeight",
847   "aritysquaredmax0"   : "WAritySqMax0",
848   "invarity"           : "WInvArityWeight",
849   "invaritymax0"       : "WInvArityMax0",
850   "invaritysquared"    : "WInvSqArityWeight",
851   "invaritysquaredmax0": "WInvAritySqMax0",
852   "precedence"         : "WPrecedence",
853   "invprecedence"      : "WPrecedenceInv",
854   "precrank5"          : "WPrecRank5",
855   "precrank10"         : "WPrecRank10",
856   "precrank20"         : "WPrecRank20",
857   "freqcount"          : "WFrequency",
858   "invfreqcount"       : "WInvFrequency",
859   "freqrank"           : "WFrequencyRank",
860   "invfreqrank"        : "WInvFrequencyRank",
861   "invconjfreqrank"    : "WInvConjFrequencyRank",
862   "freqranksquare"     : "WFrequencyRankSq",
863   "invfreqranksquare"  : "WInvFrequencyRankSq",
864   "invmodfreqrank"     : "WInvModFreqRank",
865   "invmodfreqrankmax0" : "WInvModFreqRankMax0",
866   "constant"           : "WConstantWeight"
867}
868
869prec_gen={
870   "none"            : "PNoMethod",
871   "unary_first"     : "PUnaryFirst",
872   "unary_freq"      : "PUnaryFirstFreq",
873   "arity"           : "PArity",
874   "invarity"        : "PInvArity",
875   "const_max"       : "PConstFirst ",
876   "const_min"       : "PInvArConstMin",
877   "freq"            : "PByFrequency",
878   "invfreq"         : "PByInvFrequency",
879   "invconjfreq"     : "PByInvConjFrequency",
880   "invfreqconjmax"  : "PByInvFreqConjMax",
881   "invfreqconjmin"  : "PByInvFreqConjMin",
882   "invfreqconstmin" : "PByInvFreqConstMin",
883   "invfreqhack"     : "PByInvFreqHack",
884   "orient_axioms"   : "POrientAxioms"
885}
886
887unproc_simpl={
888    "NoSimplify"     : "NoUnitSimplify",
889    "TopSimplify"    : "TopLevelUnitSimplify",
890    "FullSimplify"   : "FullUnitSimplify"
891}
892
893def print_raw(fp, result, opt_res):
894    fp.write("/* Raw association */\n")
895
896    sum = 0;
897    fp.write("char* raw_class[] = \n{\n")
898    for i in result.keys():
899        res = opt_res[i]
900        cl  = result[i]
901        sum += res
902        fp.write("   \""+i[6:]+"\",  /* %6d %20s */\n"%(res,cl))
903    fp.write("   NULL\n};")
904    fp.write("/* Predicted solutions: %d */\n"%(sum,))
905
906
907def print_strat_once(fp, strat, defined_strats):
908    """
909    If strat is not in defined_strats, print it and add it to
910    defined_strats.
911    """
912    if not strat in defined_strats:
913        fp.write(heuristic_define(strat)+"\n")
914        defined_strats.add(strat)
915
916def generate_output(fp, result, stratdesc, class_dir, raw_class, opt_res,
917                    used, defined_strats):
918    """
919    Generate the actual C code. Parameters:
920    result associates each class name with a strategy name.
921    fp is the filepointer to print to
922    stratdesc associates each strategy name with its parameters (in
923                    the form a string of command line options).
924    class_dir is the name of the directory of classes (only for
925                    generating the useful comment)
926    raw_class is a boolean value switching to a very reduced output
927                    not usable to control E
928    opt_res associates each class name with the expected performance
929                    of it.
930    used is the set of used strategies.
931    """
932    by_heuristic={}
933
934    for i in result.keys():
935        by_heuristic[result[i]]=[]
936
937    for i in result.keys():
938        by_heuristic[result[i]].append(i)
939
940    fp.write( """
941/* -------------------------------------------------------*/
942/* The following code is generated automagically with     */
943/* generate_auto.py. Yes, it is fairly ugly ;-)           */
944/* -------------------------------------------------------*/
945
946""")
947    fp.write( "/* Class dir used: "+class_dir+" */\n\n")
948    print_result(fp, result, opt_res)
949
950    if raw_class:
951        print_raw(fp, result, opt_res)
952    else:
953        fp.write( """
954#ifdef CHE_PROOFCONTROL_INTERNAL
955
956/* Strategies used:                                       */
957
958""")
959        for i in by_heuristic.keys():
960            print_strat_once(fp, i, defined_strats)
961
962        if global_best in by_heuristic.keys():
963            fp.write("/* Global best, "+global_best+", already defined */\n")
964        else:
965            fp.write( "/* Global best (used as a default): */\n")
966            print_strat_once(fp, i, defined_strats)
967
968        fp.write( """#endif
969
970#if defined(CHE_HEURISTICS_INTERNAL) || defined(TO_ORDERING_INTERNAL)
971
972""")
973
974        for i in by_heuristic.keys():
975            fp.write( "   else if(\n")
976            fp.write( translate_class_list(by_heuristic[i], opt_res)+")\n")
977            fp.write( '''   {
978#ifdef CHE_HEURISTICS_INTERNAL
979            res = "''' + trans_heuristic_name(i) +'";\n')
980
981            fp.write( parse_control_info(stratdesc[i])+"\n")
982
983            fp.write( '''#endif
984#ifdef TO_ORDERING_INTERNAL
985''')
986
987            fp.write( parse_ordering_info(stratdesc[i])+"\n")
988            fp.write( "#endif\n   }\n")
989
990
991
992        fp.write( "   else /* Default */\n")
993        fp.write( '''   {
994#ifdef CHE_HEURISTICS_INTERNAL
995  res = "''' + trans_heuristic_name(global_best) +'";\n')
996
997        fp.write( parse_control_info(stratdesc[global_best])+"\n")
998
999        fp.write( '''#endif
1000#ifdef TO_ORDERING_INTERNAL
1001''')
1002        fp.write( parse_ordering_info(stratdesc[global_best])+"\n")
1003        fp.write( "#endif\n   }\n")
1004
1005        fp.write( "#endif\n")
1006
1007        fp.write( "\n/* Total solutions on test set: %d */\n"%(sum(opt_res.values()),))
1008        fp.write("""/* -------------------------------------------------------*/
1009/*     End of automatically generated code.               */
1010/* -------------------------------------------------------*/
1011
1012""")
1013
1014
1015
1016
1017
1018#------------------------------------------------------------------
1019# Begin main
1020#------------------------------------------------------------------
1021
1022argc = len(sys.argv)
1023
1024if argc <= 1:
1025    raise RuntimeError, "Usage: generate_auto.py <classes> <protocols>"
1026
1027i=1
1028
1029problems   = {} # Keys are problems, values are problem classes
1030classlist  = [] # List of all class names
1031classsize  = {} # Class name with associated size
1032stratset   = {} # Names of strategies with associated file names
1033stratdesc  = {} # Names of strategies with associated command line
1034stratperf  = {} # Global performance of strategy (strategy -> sol, time)
1035matrix     = {} # Keys: Class names. Objects: Dictionaries associating
1036                 # strategy with performance in this class
1037
1038classdata  = {} # Associates class name with ClassPerf instance
1039                # describing the performance of (all) strategies on
1040                # this class.
1041
1042class_dir  = ""
1043
1044succ_cases = ["T", "N"]
1045raw_class  = False
1046time_limit = 864000.0
1047
1048
1049for i in sys.argv[1:]:
1050    if i=="--proofs":
1051        succ_cases = ["T"]
1052    elif i=="--models":
1053        succ_cases = ["N"]
1054    elif i=="--raw":
1055        raw_class = True
1056    elif i=="--local":
1057        pick_by_global_performace = False
1058    elif i.startswith("--time="):
1059        time_limit = float(i[7:])
1060    elif i[0:2] == "--":
1061        raise RuntimeError, "Unknown option (probably typo)"
1062
1063sys.argv = filter(lambda x:x[0]!="-", sys.argv) # Take out options
1064
1065for i in sys.argv[1:]:
1066    res = match_class.search(i)
1067    if(res):
1068        key = i[res.start():res.end()]
1069        class_dir = i[0:res.start()]
1070        classlist.append(key)
1071        classsize[key] = parse_class(i, key, problems)
1072        classdata[key] = ClassPerf(key)
1073    else:
1074        key = re.split(slash,i)[-1]
1075        stratset[key] = i
1076
1077global_class = ClassPerf("ALL")
1078
1079# Now problems is a dictionary associating every class with the
1080# associated problems and stratset is a dictionary associating the
1081# "local" name of the protocol with the full (relative or absolute)
1082# file name.
1083
1084for i in stratset.keys():
1085    stratdesc[i] = parse_prot_new(stratset[i], i, problems, global_class, classdata)
1086
1087
1088# Start determining the strategies
1089
1090sys.stderr.write("Parsing done, running optimizer\n")
1091
1092time_limits = [152, 74, 24, 18, 13, 9, 5, 5]
1093
1094itercount = 0;
1095
1096defined_strats = set()
1097
1098for time_limit in time_limits:
1099    print "# Auto-Schedule iteration %d with time limit %d"\
1100          %(itercount, time_limit)
1101
1102    result     = {}
1103    global_class.computePerf(time_limit, succ_cases)
1104    global_best, global_perf = global_class.getBestStrat()
1105
1106    print "# Global best: %s (with %d solutions) out of %d strategies "%\
1107          (global_best, global_perf, global_class.getCardinality())
1108
1109    # print global_class.strats[global_best].getSuccesses(time_limit, succ_cases)
1110
1111    opt_res = {}
1112    used    = set()
1113
1114    used.add(global_best)
1115
1116    for i in classlist:
1117        perf = classdata[i]
1118        perf.computePerf(time_limit, succ_cases)
1119        best, solns = perf.getBestStrat()
1120        if solns == 0:
1121            best = global_best
1122        result[i] = best
1123        opt_res[i] = solns
1124        used.add(best)
1125
1126    # And now we print the results
1127
1128    fp = open("che_X_auto_sched%d.c"%(itercount,), "w")
1129    generate_output(fp, result, stratdesc, class_dir, raw_class,
1130                    opt_res, used, defined_strats)
1131    fp.close()
1132
1133    # Now for the cleanup: For each class, we remove the best
1134    # strategy, and all problems solved by it.
1135
1136    for i in classlist:
1137        perf = classdata[i]
1138        best, solns = perf.getBestStrat()
1139        if solns == 0:
1140            best = global_best
1141        try:
1142            # print "Best: ", best
1143            beststrat = perf.getStrat(best)
1144            # print "found: ", best
1145            solved = beststrat.getSuccesses(time_limit, succ_cases)
1146            for prob in solved:
1147                probname = prob[0]
1148                perf.delProblem(probname)
1149                global_class.delProblem(probname)
1150            perf.delStrat(best)
1151        except KeyError:
1152            pass
1153    itercount += 1
1154