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