Repair/RepairCompiler/MCC/IR/RepairGenerator.java

   1 package MCC.IR;
   2
   3 import java.io.*;
   4 import java.util.*;
   5 import MCC.State;
   6
   7 public class RepairGenerator {
   8     State state;
   9     java.io.PrintWriter outputrepair = null;
  10     java.io.PrintWriter outputaux = null;
  11     java.io.PrintWriter outputhead = null;
  12     String name="foo";
  13     String headername;
  14     static VarDescriptor oldmodel=null;
  15     static VarDescriptor newmodel=null;
  16     static VarDescriptor worklist=null;
  17     static VarDescriptor repairtable=null;
  18     static VarDescriptor goodflag=null;
  19     Rule currentrule=null;
  20     Hashtable updatenames;
  21     HashSet usedupdates;
  22     Termination termination;
  23     Set removed;
  24     HashSet togenerate;
  25     static boolean DEBUG=false;
  26     Cost cost;
  27     Sources sources;
  28
  29     public RepairGenerator(State state, Termination t) {
  30         this.state = state;
  31         updatenames=new Hashtable();
  32         usedupdates=new HashSet();
  33         termination=t;
  34         removed=t.removedset;
  35         togenerate=new HashSet();
  36         togenerate.addAll(termination.conjunctions);
  37         togenerate.removeAll(removed);
  38         GraphNode.computeclosure(togenerate,removed);
  39         cost=new Cost();
  40         sources=new Sources(state);
  41         Repair.repairgenerator=this;
  42     }
  43
  44     private void generatetypechecks(boolean flag) {
  45         if (flag) {
  46             DotExpr.DOTYPECHECKS=true;
  47             VarExpr.DOTYPECHECKS=true;
  48             DotExpr.DONULL=true;
  49             VarExpr.DONULL=true;
  50         } else {
  51             VarExpr.DOTYPECHECKS=false;
  52             DotExpr.DOTYPECHECKS=false;
  53             VarExpr.DONULL=true;
  54             DotExpr.DONULL=true;
  55         }
  56     }
  57
  58
  59     private void name_updates() {
  60         int count=0;
  61         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  62             GraphNode gn=(GraphNode) it.next();
  63             TermNode tn=(TermNode) gn.getOwner();
  64             MultUpdateNode mun=tn.getUpdate();
  65             if (togenerate.contains(gn))
  66             for (int i=0;i<mun.numUpdates();i++) {
  67                 UpdateNode un=mun.getUpdate(i);
  68                 String name="update"+String.valueOf(count++);
  69                 updatenames.put(un,name);
  70             }
  71         }
  72     }
  73
  74     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
  75         this.outputrepair = new java.io.PrintWriter(outputrepair, true);
  76         this.outputaux = new java.io.PrintWriter(outputaux, true);
  77         this.outputhead = new java.io.PrintWriter(outputhead, true);
  78         headername=st;
  79         name_updates();
  80         generatetypechecks(true);
  81         generate_tokentable();
  82         generate_hashtables();
  83         generate_stateobject();
  84         generate_call();
  85         generate_worklist();
  86         generate_rules();
  87         generate_checks();
  88         generate_teardown();
  89         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
  90         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  91         crhead.outputline("};");
  92         craux.outputline("}");
  93         generatetypechecks(false);
  94         generate_computesizes();
  95         generatetypechecks(true);
  96         generate_recomputesizes();
  97         generatetypechecks(false);
  98         generate_updates();
  99         StructureGenerator sg=new StructureGenerator(state,this);
 100         sg.buildall();
 101         crhead.outputline("#endif");
 102     }
 103
 104     String ststate="state";
 105     String stmodel="model";
 106     String strepairtable="repairtable";
 107     String stleft="left";
 108     String stright="right";
 109
 110     private void generate_updates() {
 111         int count=0;
 112         CodeWriter crhead = new StandardCodeWriter(outputhead);
 113         CodeWriter craux = new StandardCodeWriter(outputaux);
 114
 115         /* Rewrite globals */
 116
 117         for (Iterator it=this.state.stGlobals.descriptors();it.hasNext();) {
 118             VarDescriptor vd=(VarDescriptor)it.next();
 119             craux.outputline("#define "+vd.getSafeSymbol()+" "+ststate+"->"+vd.getSafeSymbol());
 120         }
 121
 122         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 123             GraphNode gn=(GraphNode) it.next();
 124             TermNode tn=(TermNode) gn.getOwner();
 125             MultUpdateNode mun=tn.getUpdate();
 126             boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
 127             if (togenerate.contains(gn))
 128             for (int i=0;i<mun.numUpdates();i++) {
 129                 UpdateNode un=mun.getUpdate(i);
 130                 String methodname=(String)updatenames.get(un);
 131
 132                 switch(mun.op) {
 133                 case MultUpdateNode.ADD:
 134                     if (isrelation) {
 135                         crhead.outputline("void "+methodname+"("+name+"_state * " +ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+");");
 136                         craux.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+")");
 137                     } else {
 138                         crhead.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+");");
 139                         craux.outputline("void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+")");
 140                     }
 141                     craux.startblock();
 142                     craux.outputline("int maybe=0;");
 143                     final SymbolTable st = un.getRule().getSymbolTable();
 144                     CodeWriter cr = new StandardCodeWriter(outputaux) {
 145                         public SymbolTable getSymbolTable() { return st; }
 146                     };
 147                     un.generate(cr, false, stleft,stright,this);
 148                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 149                     craux.endblock();
 150                     break;
 151                 case MultUpdateNode.REMOVE:
 152                     Rule r=un.getRule();
 153                     String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
 154                     for(int j=0;j<r.numQuantifiers();j++) {
 155                         Quantifier q=r.getQuantifier(j);
 156                         if (q instanceof SetQuantifier) {
 157                             SetQuantifier sq=(SetQuantifier) q;
 158                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 159                         } else if (q instanceof RelationQuantifier) {
 160                             RelationQuantifier rq=(RelationQuantifier) q;
 161
 162                             methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 163                             methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 164                         } else if (q instanceof ForQuantifier) {
 165                             ForQuantifier fq=(ForQuantifier) q;
 166                             methodcall+=",int "+fq.getVar().getSafeSymbol();
 167                         }
 168                     }
 169                     methodcall+=")";
 170                     crhead.outputline(methodcall+";");
 171                     craux.outputline(methodcall);
 172                     craux.startblock();
 173                     craux.outputline("int maybe=0;");
 174                     final SymbolTable st2 = un.getRule().getSymbolTable();
 175                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 176                         public SymbolTable getSymbolTable() { return st2; }
 177                     };
 178                     un.generate(cr2, true, null,null,this);
 179                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 180                     craux.endblock();
 181                     break;
 182                 case MultUpdateNode.MODIFY:
 183                 default:
 184                     throw new Error("Nonimplement Update");
 185                 }
 186             }
 187         }
 188     }
 189
 190     private void generate_call() {
 191         CodeWriter cr = new StandardCodeWriter(outputrepair);
 192         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
 193         cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
 194         Iterator globals=state.stGlobals.descriptors();
 195         while (globals.hasNext()) {
 196             VarDescriptor vd=(VarDescriptor) globals.next();
 197             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
 198         }
 199         /* Insert repair here */
 200         cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
 201         globals=state.stGlobals.descriptors();
 202         while (globals.hasNext()) {
 203             VarDescriptor vd=(VarDescriptor) globals.next();
 204             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
 205         }
 206         cr.outputline("delete "+vdstate.getSafeSymbol()+";");
 207     }
 208
 209     private void generate_tokentable() {
 210         CodeWriter cr = new StandardCodeWriter(outputrepair);
 211         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
 212
 213         cr.outputline("");
 214         cr.outputline("// Token values");
 215         cr.outputline("");
 216
 217         while (tokens.hasNext()) {
 218             Object token = tokens.next();
 219             cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
 220         }
 221
 222         cr.outputline("");
 223         cr.outputline("");
 224     }
 225
 226     private void generate_stateobject() {
 227         CodeWriter crhead = new StandardCodeWriter(outputhead);
 228         crhead.outputline("class "+name+"_state {");
 229         crhead.outputline("public:");
 230         Iterator globals=state.stGlobals.descriptors();
 231         while (globals.hasNext()) {
 232             VarDescriptor vd=(VarDescriptor) globals.next();
 233             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 234         }
 235         crhead.outputline("void computesizes(int *,int **);");
 236         crhead.outputline("void recomputesizes();");
 237     }
 238
 239     private void generate_computesizes() {
 240         int max=TypeDescriptor.counter;
 241         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 242         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 243             TypeDescriptor ttd=(TypeDescriptor)it.next();
 244             tdarray[ttd.getId()]=ttd;
 245         }
 246         CodeWriter cr=new StandardCodeWriter(outputaux);
 247         cr.outputline("void "+name+"_state::computesizes(int *sizearray,int **numele) {");
 248         for(int i=0;i<max;i++) {
 249             TypeDescriptor td=tdarray[i];
 250             Expr size=td.getSizeExpr();
 251             VarDescriptor vd=VarDescriptor.makeNew("size");
 252             size.generate(cr,vd);
 253             cr.outputline("sizearray["+i+"]="+vd.getSafeSymbol()+";");
 254         }
 255         for(int i=0;i<max;i++) {
 256             TypeDescriptor td=tdarray[i];
 257             if (td instanceof StructureTypeDescriptor) {
 258                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 259                 for(int j=0;j<std.fieldlist.size();j++) {
 260                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 261                     if (fd instanceof ArrayDescriptor) {
 262                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 263                         Expr index=ad.getIndexBound();
 264                         VarDescriptor vd=VarDescriptor.makeNew("index");
 265                         index.generate(cr,vd);
 266                         cr.outputline("numele["+i+"]["+j+"]="+vd.getSafeSymbol()+";");
 267                     }
 268                 }
 269             }
 270         }
 271         cr.outputline("}");
 272     }
 273
 274     private void generate_recomputesizes() {
 275         int max=TypeDescriptor.counter;
 276         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 277         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 278             TypeDescriptor ttd=(TypeDescriptor)it.next();
 279             tdarray[ttd.getId()]=ttd;
 280         }
 281         CodeWriter cr=new StandardCodeWriter(outputaux);
 282         cr.outputline("void "+name+"_state::recomputesizes() {");
 283         for(int i=0;i<max;i++) {
 284             TypeDescriptor td=tdarray[i];
 285             Expr size=td.getSizeExpr();
 286             VarDescriptor vd=VarDescriptor.makeNew("size");
 287             size.generate(cr,vd);
 288         }
 289         for(int i=0;i<max;i++) {
 290             TypeDescriptor td=tdarray[i];
 291             if (td instanceof StructureTypeDescriptor) {
 292                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 293                 for(int j=0;j<std.fieldlist.size();j++) {
 294                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 295                     if (fd instanceof ArrayDescriptor) {
 296                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 297                         Expr index=ad.getIndexBound();
 298                         VarDescriptor vd=VarDescriptor.makeNew("index");
 299                         index.generate(cr,vd);
 300                     }
 301                 }
 302             }
 303         }
 304         cr.outputline("}");
 305     }
 306
 307
 308     private void generate_hashtables() {
 309         CodeWriter craux = new StandardCodeWriter(outputaux);
 310         CodeWriter crhead = new StandardCodeWriter(outputhead);
 311         crhead.outputline("#ifndef "+name+"_h");
 312         crhead.outputline("#define "+name+"_h");
 313         crhead.outputline("#include \"SimpleHash.h\"");
 314         crhead.outputline("extern \"C\" {");
 315         crhead.outputline("#include \"instrument.h\"");
 316         crhead.outputline("}");
 317         crhead.outputline("#include <stdio.h>");
 318         crhead.outputline("#include <stdlib.h>");
 319         crhead.outputline("class "+name+" {");
 320         crhead.outputline("public:");
 321         crhead.outputline(name+"();");
 322         crhead.outputline("~"+name+"();");
 323         craux.outputline("#include \""+headername+"\"");
 324         craux.outputline("#include \"size.h\"");
 325
 326         craux.outputline(name+"::"+name+"() {");
 327         craux.outputline("// creating hashtables ");
 328
 329         /* build sets */
 330         Iterator sets = state.stSets.descriptors();
 331
 332         /* first pass create all the hash tables */
 333         while (sets.hasNext()) {
 334             SetDescriptor set = (SetDescriptor) sets.next();
 335             crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
 336             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
 337         }
 338
 339         /* second pass build relationships between hashtables */
 340         sets = state.stSets.descriptors();
 341
 342         while (sets.hasNext()) {
 343             SetDescriptor set = (SetDescriptor) sets.next();
 344             Iterator subsets = set.subsets();
 345
 346             while (subsets.hasNext()) {
 347                 SetDescriptor subset = (SetDescriptor) subsets.next();
 348                 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
 349             }
 350         }
 351
 352         /* build relations */
 353         Iterator relations = state.stRelations.descriptors();
 354
 355         /* first pass create all the hash tables */
 356         while (relations.hasNext()) {
 357             RelationDescriptor relation = (RelationDescriptor) relations.next();
 358
 359             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 360                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
 361                 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
 362             }
 363
 364             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 365                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
 366                 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
 367             }
 368         }
 369
 370         craux.outputline("}");
 371         crhead.outputline("};");
 372         craux.outputline(name+"::~"+name+"() {");
 373         craux.outputline("// deleting hashtables");
 374
 375         /* build destructor */
 376         sets = state.stSets.descriptors();
 377
 378         /* first pass create all the hash tables */
 379         while (sets.hasNext()) {
 380             SetDescriptor set = (SetDescriptor) sets.next();
 381             craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
 382         }
 383
 384         /* destroy relations */
 385         relations = state.stRelations.descriptors();
 386
 387         /* first pass create all the hash tables */
 388         while (relations.hasNext()) {
 389             RelationDescriptor relation = (RelationDescriptor) relations.next();
 390
 391             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 392                 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
 393             }
 394
 395             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 396                 craux.outputline("delete " + relation.getSafeSymbol() + "_hashinv;");
 397             }
 398         }
 399         craux.outputline("}");
 400     }
 401
 402     private void generate_worklist() {
 403         CodeWriter crhead = new StandardCodeWriter(outputhead);
 404         CodeWriter craux = new StandardCodeWriter(outputaux);
 405         oldmodel=VarDescriptor.makeNew("oldmodel");
 406         newmodel=VarDescriptor.makeNew("newmodel");
 407         worklist=VarDescriptor.makeNew("worklist");
 408         goodflag=VarDescriptor.makeNew("goodflag");
 409         repairtable=VarDescriptor.makeNew("repairtable");
 410         crhead.outputline("void doanalysis();");
 411         craux.outputline("void "+name +"_state::doanalysis()");
 412         craux.startblock();
 413         craux.outputline("int highmark;");
 414         craux.outputline("initializestack(&highmark);");
 415         craux.outputline("typeobject *typeobject1=gettypeobject();");
 416         craux.outputline("typeobject1->computesizes(this);");
 417         craux.outputline("recomputesizes();");
 418         craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
 419         craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
 420         craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 421         craux.outputline("while (1)");
 422         craux.startblock();
 423         craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
 424         craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
 425     }
 426
 427     private void generate_teardown() {
 428         CodeWriter cr = new StandardCodeWriter(outputaux);
 429         cr.endblock();
 430     }
 431
 432     private void generate_rules() {
 433         /* first we must sort the rules */
 434         Iterator allrules = state.vRules.iterator();
 435         Vector emptyrules = new Vector(); // rules with no quantifiers
 436         Vector worklistrules = new Vector(); // the rest of the rules
 437         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 438         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 439
 440         while (allrules.hasNext()) {
 441             Rule rule = (Rule) allrules.next();
 442             ListIterator quantifiers = rule.quantifiers();
 443             boolean noquantifiers = true;
 444             while (quantifiers.hasNext()) {
 445                 Quantifier quantifier = (Quantifier) quantifiers.next();
 446                 if (quantifier instanceof ForQuantifier) {
 447                     // ok, because integers exist already!
 448                 } else {
 449                     // real quantifier
 450                     noquantifiers = false;
 451                     break;
 452                 }
 453             }
 454             if (noquantifiers) {
 455                 emptyrules.add(rule);
 456             } else {
 457                 worklistrules.add(rule);
 458             }
 459         }
 460
 461         Iterator iterator_er = emptyrules.iterator();
 462         while (iterator_er.hasNext()) {
 463             Rule rule = (Rule) iterator_er.next();
 464             {
 465                 final SymbolTable st = rule.getSymbolTable();
 466                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 467                         public SymbolTable getSymbolTable() { return st; }
 468                     };
 469                 cr.outputline("// build " +escape(rule.toString()));
 470                 cr.startblock();
 471                 cr.outputline("int maybe=0;");
 472                 ListIterator quantifiers = rule.quantifiers();
 473                 while (quantifiers.hasNext()) {
 474                     Quantifier quantifier = (Quantifier) quantifiers.next();
 475                     quantifier.generate_open(cr);
 476                 }
 477
 478                 /* pretty print! */
 479                 cr.output("//");
 480                 rule.getGuardExpr().prettyPrint(cr);
 481                 cr.outputline("");
 482
 483                 /* now we have to generate the guard test */
 484                 VarDescriptor guardval = VarDescriptor.makeNew();
 485                 rule.getGuardExpr().generate(cr, guardval);
 486                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 487                 cr.startblock();
 488
 489                 /* now we have to generate the inclusion code */
 490                 currentrule=rule;
 491                 rule.getInclusion().generate(cr);
 492                 cr.endblock();
 493                 while (quantifiers.hasPrevious()) {
 494                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 495                     cr.endblock();
 496                 }
 497                 cr.endblock();
 498                 cr.outputline("");
 499                 cr.outputline("");
 500             }
 501         }
 502
 503         CodeWriter cr2 = new StandardCodeWriter(outputaux);
 504
 505         cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
 506         cr2.startblock();
 507         VarDescriptor idvar=VarDescriptor.makeNew("id");
 508         cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
 509
 510         String elseladder = "if";
 511
 512         Iterator iterator_rules = worklistrules.iterator();
 513         while (iterator_rules.hasNext()) {
 514
 515             Rule rule = (Rule) iterator_rules.next();
 516             int dispatchid = rule.getNum();
 517
 518             {
 519                 final SymbolTable st = rule.getSymbolTable();
 520                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 521                         public SymbolTable getSymbolTable() { return st; }
 522                     };
 523
 524                 cr.indent();
 525                 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 526                 cr.startblock();
 527                 cr.outputline("int maybe=0;");
 528                 VarDescriptor typevar=VarDescriptor.makeNew("type");
 529                 VarDescriptor leftvar=VarDescriptor.makeNew("left");
 530                 VarDescriptor rightvar=VarDescriptor.makeNew("right");
 531                 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
 532                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
 533                 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
 534                 cr.outputline("// build " +escape(rule.toString()));
 535
 536
 537                 for (int j=0;j<rule.numQuantifiers();j++) {
 538                     Quantifier quantifier = rule.getQuantifier(j);
 539                     quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 540                 }
 541
 542                 /* pretty print! */
 543                 cr.output("//");
 544
 545                 rule.getGuardExpr().prettyPrint(cr);
 546                 cr.outputline("");
 547
 548                 /* now we have to generate the guard test */
 549
 550                 VarDescriptor guardval = VarDescriptor.makeNew();
 551                 rule.getGuardExpr().generate(cr, guardval);
 552
 553                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 554                 cr.startblock();
 555
 556                 /* now we have to generate the inclusion code */
 557                 currentrule=rule;
 558                 rule.getInclusion().generate(cr);
 559                 cr.endblock();
 560
 561                 for (int j=0;j<rule.numQuantifiers();j++) {
 562                     cr.endblock();
 563                 }
 564
 565                 // close startblocks generated by DotExpr memory checks
 566                 //DotExpr.generate_memory_endblocks(cr);
 567
 568                 cr.endblock(); // end else-if WORKLIST ladder
 569
 570                 elseladder = "else if";
 571             }
 572         }
 573
 574         cr2.outputline("else");
 575         cr2.startblock();
 576         cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 577         cr2.outputline("exit(1);");
 578         cr2.endblock();
 579         // end block created for worklist
 580         cr2.outputline(worklist.getSafeSymbol()+"->pop();");
 581         cr2.endblock();
 582     }
 583
 584     public static String escape(String s) {
 585         String newstring="";
 586         for(int i=0;i<s.length();i++) {
 587             char c=s.charAt(i);
 588             if (c=='"')
 589                 newstring+="\"";
 590             else
 591                 newstring+=c;
 592         }
 593         return newstring;
 594     }
 595
 596     private void generate_checks() {
 597
 598         /* do constraint checks */
 599         Vector constraints = state.vConstraints;
 600
 601         for (int i = 0; i < constraints.size(); i++) {
 602
 603             Constraint constraint = (Constraint) constraints.elementAt(i);
 604
 605             {
 606
 607                 final SymbolTable st = constraint.getSymbolTable();
 608
 609                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 610                         public SymbolTable getSymbolTable() { return st; }
 611                     };
 612
 613                 cr.outputline("// checking " + escape(constraint.toString()));
 614                 cr.startblock();
 615
 616                 ListIterator quantifiers = constraint.quantifiers();
 617
 618                 while (quantifiers.hasNext()) {
 619                     Quantifier quantifier = (Quantifier) quantifiers.next();
 620                     quantifier.generate_open(cr);
 621                 }
 622
 623                 cr.outputline("int maybe = 0;");
 624
 625                 /* now we have to generate the guard test */
 626
 627                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 628                 constraint.getLogicStatement().generate(cr, constraintboolean);
 629
 630                 cr.outputline("if (maybe)");
 631                 cr.startblock();
 632                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \");");
 633                 cr.outputline("exit(1);");
 634                 cr.endblock();
 635
 636                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 637                 cr.startblock();
 638                 if (DEBUG)
 639                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
 640
 641                 /* Do repairs */
 642                 /* Build new repair table */
 643                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 644                 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 645                 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
 646
 647
 648                 /* Compute cost of each repair */
 649                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 650                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 651                 DNFConstraint dnfconst=constraint.dnfconstraint;
 652                 if (dnfconst.size()<=1) {
 653                     cr.outputline("int "+mincostindex.getSafeSymbol()+"=0;");
 654                 }
 655                 if (dnfconst.size()>1) {
 656                     cr.outputline("int "+mincostindex.getSafeSymbol()+";");
 657                     boolean first=true;
 658                     for(int j=0;j<dnfconst.size();j++) {
 659                         Conjunction conj=dnfconst.get(j);
 660                         GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 661                         if (removed.contains(gn))
 662                             continue;
 663
 664                         VarDescriptor costvar;
 665                         if (first) {
 666                             costvar=mincost;
 667                         } else
 668                             costvar=VarDescriptor.makeNew("cost");
 669                         for(int k=0;k<conj.size();k++) {
 670                             DNFPredicate dpred=conj.get(k);
 671                             Predicate p=dpred.getPredicate();
 672                             boolean negate=dpred.isNegated();
 673                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 674                             p.generate(cr,predvalue);
 675                             if (negate)
 676                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 677                             else
 678                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 679                             if (k==0)
 680                                 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
 681                             else
 682                                 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 683                         }
 684
 685                         if(!first) {
 686                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
 687                             cr.startblock();
 688                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
 689                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 690                             cr.endblock();
 691                         } else
 692                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 693                         first=false;
 694                     }
 695                 }
 696                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
 697                 for(int j=0;j<dnfconst.size();j++) {
 698                     Conjunction conj=dnfconst.get(j);
 699                     GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 700                     if (removed.contains(gn))
 701                         continue;
 702                     cr.outputline("case "+j+":");
 703                     for(int k=0;k<conj.size();k++) {
 704                         DNFPredicate dpred=conj.get(k);
 705                         Predicate p=dpred.getPredicate();
 706                         boolean negate=dpred.isNegated();
 707                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 708                         p.generate(cr,predvalue);
 709                         if (negate)
 710                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 711                         else
 712                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 713                         cr.startblock();
 714                         if (p instanceof InclusionPredicate)
 715                             generateinclusionrepair(conj,dpred, cr);
 716                         else if (p instanceof ExprPredicate) {
 717                             ExprPredicate ep=(ExprPredicate)p;
 718                             if (ep.getType()==ExprPredicate.SIZE)
 719                                 generatesizerepair(conj,dpred,cr);
 720                             else if (ep.getType()==ExprPredicate.COMPARISON)
 721                                 generatecomparisonrepair(conj,dpred,cr);
 722                         } else throw new Error("Unrecognized Predicate");
 723                         cr.endblock();
 724                     }
 725                     /* Update model */
 726                     cr.outputline("break;");
 727                 }
 728                 cr.outputline("}");
 729
 730                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
 731                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 732                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 733                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
 734                 cr.outputline("goto rebuild;");  /* Rebuild model and all */
 735
 736                 cr.endblock();
 737
 738                 while (quantifiers.hasPrevious()) {
 739                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 740                     cr.endblock();
 741                 }
 742                 cr.endblock();
 743                 cr.outputline("");
 744                 cr.outputline("");
 745             }
 746         }
 747         CodeWriter cr = new StandardCodeWriter(outputaux);
 748         cr.outputline("if ("+goodflag.getSafeSymbol()+")");
 749         cr.startblock();
 750         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 751         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 752         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 753         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 754         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
 755         cr.outputline("delete "+worklist.getSafeSymbol()+";");
 756         cr.outputline("resettypemap();");
 757         cr.outputline("break;");
 758         cr.endblock();
 759         cr.outputline("rebuild:");
 760         cr.outputline(";");
 761
 762     }
 763
 764     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
 765         MultUpdateNode mun=null;
 766         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
 767         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
 768             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 769             TermNode tn2=(TermNode)gn2.getOwner();
 770             if (tn2.getType()==TermNode.ABSTRACT) {
 771                 AbstractRepair ar=tn2.getAbstract();
 772                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
 773                     ar.getPredicate()==dpred) {
 774                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 775                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
 776                         if (!removed.contains(gn3)) {
 777                             TermNode tn3=(TermNode)gn3.getOwner();
 778                             if (tn3.getType()==TermNode.UPDATE) {
 779                                 mun=tn3.getUpdate();
 780                                 break;
 781                             }
 782                         }
 783                     }
 784                 }
 785             }
 786         }
 787         return mun;
 788     }
 789
 790     public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 791         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 792         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 793         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 794         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
 795         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 796         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 797         boolean inverted=ep.inverted();
 798         boolean negated=dpred.isNegated();
 799         OpExpr expr=(OpExpr)ep.expr;
 800         Opcode opcode=expr.getOpcode();
 801         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 802         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 803         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
 804         if (!inverted) {
 805             expr.getLeftExpr().generate(cr,leftside);
 806             expr.getRightExpr().generate(cr,newvalue);
 807             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
 808             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 809         } else {
 810             expr.getLeftExpr().generate(cr,rightside);
 811             expr.getRightExpr().generate(cr,newvalue);
 812             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 813             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 814         }
 815         if (negated)
 816             if (opcode==Opcode.GT) {
 817                 opcode=Opcode.LE;
 818             } else if (opcode==Opcode.GE) {
 819                 opcode=Opcode.LT;
 820             } else if (opcode==Opcode.LT) {
 821                 opcode=Opcode.GE;
 822             } else if (opcode==Opcode.LE) {
 823                 opcode=Opcode.GT;
 824             } else if (opcode==Opcode.EQ) {
 825                 opcode=Opcode.NE;
 826             } else if (opcode==Opcode.NE) {
 827                 opcode=Opcode.EQ;
 828             } else {
 829                 throw new Error("Unrecognized Opcode");
 830             }
 831
 832         if (opcode==Opcode.GT) {
 833             cr.outputline(newvalue.getSafeSymbol()+"++;");
 834         } else if (opcode==Opcode.GE) {
 835             /* Equal */
 836         } else if (opcode==Opcode.LT) {
 837             cr.outputline(newvalue.getSafeSymbol()+"--;");
 838         } else if (opcode==Opcode.LE) {
 839             /* Equal */
 840         } else if (opcode==Opcode.EQ) {
 841             /* Equal */
 842         } else if (opcode==Opcode.NE) {
 843             cr.outputline(newvalue.getSafeSymbol()+"++;");
 844         } else {
 845             throw new Error("Unrecognized Opcode");
 846         }
 847         /* Do abstract repairs */
 848         if (usageimage) {
 849             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 850             if (!inverted) {
 851                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 852             } else {
 853                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 854             }
 855         }
 856         if (usageinvimage) {
 857             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 858             if (!inverted) {
 859                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 860             } else {
 861                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 862             }
 863         }
 864         /* Do concrete repairs */
 865         /* Start with scheduling removal */
 866         for(int i=0;i<state.vRules.size();i++) {
 867             Rule r=(Rule)state.vRules.get(i);
 868             if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 869                 for(int j=0;j<munremove.numUpdates();j++) {
 870                     UpdateNode un=munremove.getUpdate(i);
 871                     if (un.getRule()==r) {
 872                         /* Update for rule r */
 873                         String name=(String)updatenames.get(un);
 874                         cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
 875                     }
 876                 }
 877             }
 878         }
 879         /* Now do addition */
 880         UpdateNode un=munadd.getUpdate(0);
 881         String name=(String)updatenames.get(un);
 882         if (!inverted) {
 883             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 884         } else {
 885             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 886         }
 887     }
 888
 889     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
 890         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 891         OpExpr expr=(OpExpr)ep.expr;
 892         Opcode opcode=expr.getOpcode();
 893         {
 894             boolean negated=dpred.isNegated();
 895             if (negated)
 896                 if (opcode==Opcode.GT) {
 897                     opcode=Opcode.LE;
 898                 } else if (opcode==Opcode.GE) {
 899                     opcode=Opcode.LT;
 900                 } else if (opcode==Opcode.LT) {
 901                     opcode=Opcode.GE;
 902                 } else if (opcode==Opcode.LE) {
 903                     opcode=Opcode.GT;
 904                 } else if (opcode==Opcode.EQ) {
 905                     opcode=Opcode.NE;
 906                 } else if (opcode==Opcode.NE) {
 907                     opcode=Opcode.EQ;
 908                 } else {
 909                     throw new Error("Unrecognized Opcode");
 910                 }
 911         }
 912         MultUpdateNode munremove;
 913
 914         MultUpdateNode munadd;
 915         if (ep.getDescriptor() instanceof RelationDescriptor) {
 916             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 917             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 918         } else {
 919             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
 920             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
 921         }
 922         int size=ep.leftsize();
 923         VarDescriptor sizevar=VarDescriptor.makeNew("size");
 924         ((OpExpr)expr).left.generate(cr, sizevar);
 925         VarDescriptor change=VarDescriptor.makeNew("change");
 926         cr.outputline("int "+change.getSafeSymbol()+";");
 927         boolean generateadd=false;
 928         boolean generateremove=false;
 929         if (opcode==Opcode.GT) {
 930             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 931             generateadd=true;
 932             generateremove=false;
 933         } else if (opcode==Opcode.GE) {
 934             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 935             generateadd=true;
 936             generateremove=false;
 937         } else if (opcode==Opcode.LT) {
 938             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
 939             generateadd=false;
 940             generateremove=true;
 941         } else if (opcode==Opcode.LE) {
 942             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 943             generateadd=false;
 944             generateremove=true;
 945         } else if (opcode==Opcode.EQ) {
 946             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 947             if (size==0)
 948                 generateadd=false;
 949             else
 950                 generateadd=true;
 951             generateremove=true;
 952         } else if (opcode==Opcode.NE) {
 953             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 954             generateadd=true;
 955             generateremove=false;
 956         } else {
 957             throw new Error("Unrecognized Opcode");
 958         }
 959         Descriptor d=ep.getDescriptor();
 960         if (generateremove) {
 961             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
 962             cr.startblock();
 963             /* Find element to remove */
 964             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
 965             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
 966             if (d instanceof RelationDescriptor) {
 967                 if (ep.inverted()) {
 968                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 969                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
 970                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
 971                 } else {
 972                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 973                     cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
 974                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
 975                 }
 976             } else {
 977                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
 978             }
 979             /* Generate abstract remove instruction */
 980             if (d instanceof RelationDescriptor) {
 981                 RelationDescriptor rd=(RelationDescriptor) d;
 982                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 983                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 984                 if (usageimage)
 985                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
 986                 if (usageinvimage)
 987                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
 988             } else {
 989                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
 990             }
 991             /* Generate concrete remove instruction */
 992             for(int i=0;i<state.vRules.size();i++) {
 993                 Rule r=(Rule)state.vRules.get(i);
 994                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
 995                     for(int j=0;j<munremove.numUpdates();j++) {
 996                         UpdateNode un=munremove.getUpdate(j);
 997                         if (un.getRule()==r) {
 998                                 /* Update for rule rule r */
 999                             String name=(String)updatenames.get(un);
1000                             if (d instanceof RelationDescriptor) {
1001                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1002                             } else {
1003                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1004                             }
1005                         }
1006                     }
1007                 }
1008             }
1009             cr.endblock();
1010         }
1011         if (generateadd) {
1012
1013             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
1014             cr.startblock();
1015             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
1016             if (d instanceof RelationDescriptor) {
1017                 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
1018                 RelationDescriptor rd=(RelationDescriptor)d;
1019                 if (sources.relsetSource(rd,!ep.inverted())) {
1020                     /* Set Source */
1021                     SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
1022                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1023                     cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1024                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1025                     cr.startblock();
1026                     if (ep.inverted()) {
1027                         cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
1028                     } else {
1029                         cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
1030                     }
1031                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1032                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1033                     cr.endblock();
1034                 } else if (sources.relallocSource(rd,!ep.inverted())) {
1035                     /* Allocation Source*/
1036                     sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
1037                 } else throw new Error("No source for adding to Relation");
1038                 if (ep.inverted()) {
1039                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1040                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1041                     if (usageimage)
1042                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1043                     if (usageinvimage)
1044                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1045
1046                     UpdateNode un=munadd.getUpdate(0);
1047                     String name=(String)updatenames.get(un);
1048                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1049                 } else {
1050                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1051                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1052                     if (usageimage)
1053                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1054                     if (usageinvimage)
1055                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1056                     UpdateNode un=munadd.getUpdate(0);
1057                     String name=(String)updatenames.get(un);
1058                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1059                 }
1060             } else {
1061                 SetDescriptor sd=(SetDescriptor)d;
1062                 if (sources.setSource(sd)) {
1063                     /* Set Source */
1064                     /* Set Source */
1065                     SetDescriptor sourcesd=sources.getSourceSet(sd);
1066                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1067                     cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1068                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1069                     cr.startblock();
1070                     cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
1071                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1072                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1073                     cr.endblock();
1074                 } else if (sources.allocSource(sd)) {
1075                     /* Allocation Source*/
1076                     sources.generateSourceAlloc(cr,newobject,sd);
1077                 } else throw new Error("No source for adding to Set");
1078                 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1079                 UpdateNode un=munadd.getUpdate(0);
1080                 String name=(String)updatenames.get(un);
1081                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1082             }
1083             cr.endblock();
1084         }
1085     }
1086
1087     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1088         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
1089         boolean negated=dpred.isNegated();
1090         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
1091         VarDescriptor leftvar=VarDescriptor.makeNew("left");
1092         ip.expr.generate(cr, leftvar);
1093
1094         if (negated) {
1095             if (ip.setexpr instanceof ImageSetExpr) {
1096                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1097                 VarDescriptor rightvar=ise.getVar();
1098                 boolean inverse=ise.inverted();
1099                 RelationDescriptor rd=ise.getRelation();
1100                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1101                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1102                 if (inverse) {
1103                     if (usageimage)
1104                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1105                     if (usageinvimage)
1106                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1107                 } else {
1108                     if (usageimage)
1109                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1110                     if (usageinvimage)
1111                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1112                 }
1113                 for(int i=0;i<state.vRules.size();i++) {
1114                     Rule r=(Rule)state.vRules.get(i);
1115                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1116                         for(int j=0;j<mun.numUpdates();j++) {
1117                             UpdateNode un=mun.getUpdate(i);
1118                             if (un.getRule()==r) {
1119                                 /* Update for rule rule r */
1120                                 String name=(String)updatenames.get(un);
1121                                 if (inverse) {
1122                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1123                                 } else {
1124                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1125                                 }
1126                             }
1127                         }
1128                     }
1129                 }
1130             } else {
1131                 SetDescriptor sd=ip.setexpr.sd;
1132                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1133
1134                 for(int i=0;i<state.vRules.size();i++) {
1135                     Rule r=(Rule)state.vRules.get(i);
1136                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1137                         for(int j=0;j<mun.numUpdates();j++) {
1138                             UpdateNode un=mun.getUpdate(i);
1139                             if (un.getRule()==r) {
1140                                 /* Update for rule rule r */
1141                                 String name=(String)updatenames.get(un);
1142                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1143                             }
1144                         }
1145                     }
1146                 }
1147             }
1148         } else {
1149             /* Generate update */
1150             if (ip.setexpr instanceof ImageSetExpr) {
1151                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1152                 VarDescriptor rightvar=ise.getVar();
1153                 boolean inverse=ise.inverted();
1154                 RelationDescriptor rd=ise.getRelation();
1155                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1156                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1157                 if (inverse) {
1158                     if (usageimage)
1159                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1160                     if (usageinvimage)
1161                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1162                 } else {
1163                     if (usageimage)
1164                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1165                     if (usageinvimage)
1166                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1167                 }
1168                 UpdateNode un=mun.getUpdate(0);
1169                 String name=(String)updatenames.get(un);
1170                 if (inverse) {
1171                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1172                 } else {
1173                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1174                 }
1175             } else {
1176                 SetDescriptor sd=ip.setexpr.sd;
1177                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1178
1179                 UpdateNode un=mun.getUpdate(0);
1180                 /* Update for rule rule r */
1181                 String name=(String)updatenames.get(un);
1182                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1183             }
1184         }
1185     }
1186
1187
1188
1189     public static Vector getrulelist(Descriptor d) {
1190         Vector dispatchrules = new Vector();
1191         Vector rules = State.currentState.vRules;
1192
1193         for (int i = 0; i < rules.size(); i++) {
1194             Rule rule = (Rule) rules.elementAt(i);
1195             Set requiredsymbols = rule.getRequiredDescriptors();
1196
1197             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1198             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1199             // fashion...
1200
1201             if (rule.getRequiredDescriptors().contains(d)) {
1202                 dispatchrules.addElement(rule);
1203             }
1204         }
1205         return dispatchrules;
1206     }
1207
1208     private boolean need_compensation(Rule r) {
1209         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1210         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1211             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1212             GraphNode gn2=edge.getTarget();
1213             if (!removed.contains(gn2)) {
1214                 TermNode tn2=(TermNode)gn2.getOwner();
1215                 if (tn2.getType()==TermNode.CONSEQUENCE)
1216                     return false;
1217             }
1218         }
1219         return true;
1220     }
1221
1222     private UpdateNode find_compensation(Rule r) {
1223         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1224         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1225             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1226             GraphNode gn2=edge.getTarget();
1227             if (!removed.contains(gn2)) {
1228                 TermNode tn2=(TermNode)gn2.getOwner();
1229                 if (tn2.getType()==TermNode.UPDATE) {
1230                     MultUpdateNode mun=tn2.getUpdate();
1231                     for(int i=0;i<mun.numUpdates();i++) {
1232                         UpdateNode un=mun.getUpdate(i);
1233                         if (un.getRule()==r)
1234                             return un;
1235                     }
1236                 }
1237             }
1238         }
1239         throw new Error("No Compensation Update could be found");
1240     }
1241
1242     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1243         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1244         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1245
1246         if (!(usageinvimage||usageimage)) /* not used at all*/
1247             return;
1248
1249         cr.outputline("// RELATION DISPATCH ");
1250         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1251         if (usageimage)
1252             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1253         else
1254             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1255         cr.startblock(); {
1256             /* Adding new item */
1257             /* Perform safety checks */
1258             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1259             cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1260             cr.startblock(); {
1261                 /* Have update to call into */
1262                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1263                 String parttype="";
1264                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1265                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1266                         parttype=parttype+", int, int";
1267                     else
1268                         parttype=parttype+", int";
1269                 }
1270                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1271                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1272                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1273                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1274                     Quantifier q=currentrule.getQuantifier(i);
1275                     if (q instanceof SetQuantifier) {
1276                         SetQuantifier sq=(SetQuantifier) q;
1277                         methodcall+=","+sq.getVar().getSafeSymbol();
1278                     } else if (q instanceof RelationQuantifier) {
1279                         RelationQuantifier rq=(RelationQuantifier) q;
1280                         methodcall+=","+rq.x.getSafeSymbol();
1281                         methodcall+=","+rq.y.getSafeSymbol();
1282                     } else if (q instanceof ForQuantifier) {
1283                         ForQuantifier fq=(ForQuantifier) q;
1284                         methodcall+=","+fq.getVar().getSafeSymbol();
1285                     }
1286                 }
1287                 methodcall+=");";
1288                 cr.outputline(methodcall);
1289                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1290                 cr.outputline("continue;");
1291             }
1292             cr.endblock();
1293             /* Build standard compensation actions */
1294             if (need_compensation(currentrule)) {
1295                 UpdateNode un=find_compensation(currentrule);
1296                 String name=(String)updatenames.get(un);
1297                 usedupdates.add(un); /* Mark as used */
1298                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1299                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1300                     Quantifier q=currentrule.getQuantifier(i);
1301                     if (q instanceof SetQuantifier) {
1302                         SetQuantifier sq=(SetQuantifier) q;
1303                         methodcall+=","+sq.getVar().getSafeSymbol();
1304                     } else if (q instanceof RelationQuantifier) {
1305                         RelationQuantifier rq=(RelationQuantifier) q;
1306                         methodcall+=","+rq.x.getSafeSymbol();
1307                         methodcall+=","+rq.y.getSafeSymbol();
1308                     } else if (q instanceof ForQuantifier) {
1309                         ForQuantifier fq=(ForQuantifier) q;
1310                         methodcall+=","+fq.getVar().getSafeSymbol();
1311                     }
1312                 }
1313                 methodcall+=");";
1314                 cr.outputline(methodcall);
1315                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1316                 cr.outputline("continue;");
1317             }
1318         }
1319         cr.endblock();
1320
1321         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1322         cr.outputline("int " + addeditem + ";");
1323         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1324             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar+ ");");
1325         }
1326
1327         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1328             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1329         }
1330
1331         cr.outputline("if (" + addeditem + ")");
1332         cr.startblock();
1333
1334         Vector dispatchrules = getrulelist(rd);
1335
1336         if (dispatchrules.size() == 0) {
1337             cr.outputline("// nothing to dispatch");
1338             cr.endblock();
1339             return;
1340         }
1341
1342         for(int i = 0; i < dispatchrules.size(); i++) {
1343             Rule rule = (Rule) dispatchrules.elementAt(i);
1344             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1345                 /* Guard depends on this relation, so we recomput everything */
1346                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1347             } else {
1348                 for (int j=0;j<rule.numQuantifiers();j++) {
1349                     Quantifier q=rule.getQuantifier(j);
1350                     if (q.getRequiredDescriptors().contains(rd)) {
1351                         /* Generate add */
1352                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1353                     }
1354                 }
1355             }
1356         }
1357         cr.endblock();
1358     }
1359
1360
1361     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1362
1363         cr.outputline("// SET DISPATCH ");
1364
1365         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1366         cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1367         cr.startblock(); {
1368             /* Adding new item */
1369             /* Perform safety checks */
1370             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1371             cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1372             cr.startblock(); {
1373                 /* Have update to call into */
1374                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1375                 String parttype="";
1376                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1377                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1378                         parttype=parttype+", int, int";
1379                     else
1380                         parttype=parttype+", int";
1381                 }
1382                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1383                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1384                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1385                               repairtable.getSafeSymbol();
1386                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1387                     Quantifier q=currentrule.getQuantifier(i);
1388                     if (q instanceof SetQuantifier) {
1389                         SetQuantifier sq=(SetQuantifier) q;
1390                         methodcall+=","+sq.getVar().getSafeSymbol();
1391                     } else if (q instanceof RelationQuantifier) {
1392                         RelationQuantifier rq=(RelationQuantifier) q;
1393                         methodcall+=","+rq.x.getSafeSymbol();
1394                         methodcall+=","+rq.y.getSafeSymbol();
1395                     } else if (q instanceof ForQuantifier) {
1396                         ForQuantifier fq=(ForQuantifier) q;
1397                         methodcall+=","+fq.getVar().getSafeSymbol();
1398                     }
1399                 }
1400                 methodcall+=");";
1401                 cr.outputline(methodcall);
1402                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1403                 cr.outputline("continue;");
1404             }
1405             cr.endblock();
1406             /* Build standard compensation actions */
1407             if (need_compensation(currentrule)) {
1408                 UpdateNode un=find_compensation(currentrule);
1409                 String name=(String)updatenames.get(un);
1410                 usedupdates.add(un); /* Mark as used */
1411
1412                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1413                               repairtable.getSafeSymbol();
1414                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1415                     Quantifier q=currentrule.getQuantifier(i);
1416                     if (q instanceof SetQuantifier) {
1417                         SetQuantifier sq=(SetQuantifier) q;
1418                         methodcall+=","+sq.getVar().getSafeSymbol();
1419                     } else if (q instanceof RelationQuantifier) {
1420                         RelationQuantifier rq=(RelationQuantifier) q;
1421                         methodcall+=","+rq.x.getSafeSymbol();
1422                         methodcall+=","+rq.y.getSafeSymbol();
1423                     } else if (q instanceof ForQuantifier) {
1424                         ForQuantifier fq=(ForQuantifier) q;
1425                         methodcall+=","+fq.getVar().getSafeSymbol();
1426                     }
1427                 }
1428                 methodcall+=");";
1429                 cr.outputline(methodcall);
1430                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1431                 cr.outputline("continue;");
1432             }
1433         }
1434         cr.endblock();
1435
1436         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1437         cr.outputline("int " + addeditem + " = 1;");
1438         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1439         cr.startblock();
1440         Vector dispatchrules = getrulelist(sd);
1441
1442         if (dispatchrules.size() == 0) {
1443             cr.outputline("// nothing to dispatch");
1444             cr.endblock();
1445             return;
1446         }
1447
1448         for(int i = 0; i < dispatchrules.size(); i++) {
1449             Rule rule = (Rule) dispatchrules.elementAt(i);
1450             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1451                 /* Guard depends on this relation, so we recompute everything */
1452                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1453             } else {
1454                 for (int j=0;j<rule.numQuantifiers();j++) {
1455                     Quantifier q=rule.getQuantifier(j);
1456                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1457                         /* Generate add */
1458                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1459                     }
1460                 }
1461             }
1462         }
1463         cr.endblock();
1464     }
1465 }