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