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