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