Need {} around case statements because we define variables...C++ is lame.
[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                 Vector dnfconst=new Vector();
745                 dnfconst.addAll((Set)termination.conjunctionmap.get(constraint));
746
747                 if (dnfconst.size()<=1) {
748                     cr.outputline("int "+mincostindex.getSafeSymbol()+"=0;");
749                 }
750                 if (dnfconst.size()>1) {
751                     cr.outputline("int "+mincostindex.getSafeSymbol()+";");
752                     boolean first=true;
753                     for(int j=0;j<dnfconst.size();j++) {
754                         GraphNode gn=(GraphNode)dnfconst.get(j);
755                         Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
756                         if (removed.contains(gn))
757                             continue;
758                         
759                         VarDescriptor costvar;
760                         if (first) {
761                             costvar=mincost;
762                         } else
763                             costvar=VarDescriptor.makeNew("cost");
764                         for(int k=0;k<conj.size();k++) {
765                             DNFPredicate dpred=conj.get(k);
766                             Predicate p=dpred.getPredicate();
767                             boolean negate=dpred.isNegated();
768                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
769                             p.generate(cr,predvalue);
770                             if (k==0)
771                                 cr.outputline("int "+costvar.getSafeSymbol()+"=0;");
772
773                             if (negate)
774                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
775                             else
776                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
777                             cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
778                         }
779
780                         if(!first) {
781                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
782                             cr.startblock();
783                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
784                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
785                             cr.endblock();
786                         } else
787                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
788                         first=false;
789                     }
790                 }
791                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
792                 for(int j=0;j<dnfconst.size();j++) {
793                     GraphNode gn=(GraphNode)dnfconst.get(j);
794                     Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
795
796                     if (removed.contains(gn))
797                         continue;
798                     cr.outputline("case "+j+":");
799                     cr.startblock();
800                     for(int k=0;k<conj.size();k++) {
801                         DNFPredicate dpred=conj.get(k);
802                         Predicate p=dpred.getPredicate();
803                         boolean negate=dpred.isNegated();
804                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
805                         p.generate(cr,predvalue);
806                         if (negate)
807                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
808                         else
809                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
810                         cr.startblock();
811                         if (p instanceof InclusionPredicate)
812                             generateinclusionrepair(conj,dpred, cr);
813                         else if (p instanceof ExprPredicate) {
814                             ExprPredicate ep=(ExprPredicate)p;
815                             if (ep.getType()==ExprPredicate.SIZE)
816                                 generatesizerepair(conj,dpred,cr);
817                             else if (ep.getType()==ExprPredicate.COMPARISON)
818                                 generatecomparisonrepair(conj,dpred,cr);
819                         } else throw new Error("Unrecognized Predicate");
820                         cr.endblock();
821                     }
822                     /* Update model */
823                     cr.endblock();
824                     cr.outputline("break;");
825                 }
826                 cr.outputline("}");
827
828                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
829                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
830                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
831                 cr.outputline("goto rebuild;");  /* Rebuild model and all */
832                 }
833                 cr.endblock();
834                 
835                 while (quantifiers.hasPrevious()) {
836                     Quantifier quantifier = (Quantifier) quantifiers.previous();
837                     cr.endblock();
838                 }
839                 cr.endblock();
840                 cr.outputline("");
841                 cr.outputline("");
842             }
843         }
844         CodeWriter cr = new StandardCodeWriter(outputaux);
845         cr.startblock();
846         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
847         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
848         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
849         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
850         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
851         cr.outputline("delete "+worklist.getSafeSymbol()+";");
852         cr.outputline("resettypemap();");
853         cr.outputline("break;");
854         cr.endblock();
855         cr.outputline("rebuild:");
856         cr.outputline(";");     
857         
858     }
859     
860     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
861         MultUpdateNode mun=null;
862         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
863         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
864             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
865             TermNode tn2=(TermNode)gn2.getOwner();
866             if (tn2.getType()==TermNode.ABSTRACT) {
867                 AbstractRepair ar=tn2.getAbstract();
868                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
869                     ar.getPredicate()==dpred) {
870                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
871                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
872                         if (!removed.contains(gn3)) {
873                             TermNode tn3=(TermNode)gn3.getOwner();
874                             if (tn3.getType()==TermNode.UPDATE) {
875                                 mun=tn3.getUpdate();
876                                 break;
877                             }
878                         }
879                     }
880                 }
881             }
882         }
883         return mun;
884     }
885
886     /** Generates abstract (and concrete) repair for a comparison */
887
888     private void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
889         MultUpdateNode munmodify=getmultupdatenode(conj,dpred,AbstractRepair.MODIFYRELATION);
890         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
891         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
892         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
893         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
894         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
895         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
896         boolean inverted=ep.inverted();
897         boolean negated=dpred.isNegated();
898         OpExpr expr=(OpExpr)ep.expr;
899         Opcode opcode=expr.getOpcode();
900         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
901         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
902         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
903         if (!inverted) {
904             ((RelationExpr)expr.getLeftExpr()).getExpr().generate(cr,leftside);
905             expr.getRightExpr().generate(cr,newvalue);
906             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
907             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
908         } else {
909             ((RelationExpr)expr.getLeftExpr()).getExpr().generate(cr,rightside);
910             expr.getRightExpr().generate(cr,newvalue);
911             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
912             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
913         }
914         if (negated)
915             if (opcode==Opcode.GT) {
916                 opcode=Opcode.LE;
917             } else if (opcode==Opcode.GE) {
918                 opcode=Opcode.LT;
919             } else if (opcode==Opcode.LT) {
920                 opcode=Opcode.GE;
921             } else if (opcode==Opcode.LE) {
922                 opcode=Opcode.GT;
923             } else if (opcode==Opcode.EQ) {
924                 opcode=Opcode.NE;
925             } else if (opcode==Opcode.NE) {
926                 opcode=Opcode.EQ;
927             } else {
928                 throw new Error("Unrecognized Opcode");
929             }
930
931         if (opcode==Opcode.GT) {
932             cr.outputline(newvalue.getSafeSymbol()+"++;");
933         } else if (opcode==Opcode.GE) {
934             /* Equal */
935         } else if (opcode==Opcode.LT) {
936             cr.outputline(newvalue.getSafeSymbol()+"--;");
937         } else if (opcode==Opcode.LE) {
938             /* Equal */
939         } else if (opcode==Opcode.EQ) {
940             /* Equal */
941         } else if (opcode==Opcode.NE) { /* search for FLAGNE if this is changed*/
942             cr.outputline(newvalue.getSafeSymbol()+"++;");
943         } else {
944             throw new Error("Unrecognized Opcode");
945         }
946         /* Do abstract repairs */
947         if (usageimage) {
948             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
949             if (!inverted) {
950                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
951             } else {
952                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
953             }
954         }
955         if (usageinvimage) {
956             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
957             if (!inverted) {
958                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
959             } else {
960                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
961             }
962         }
963         /* Do concrete repairs */
964         if (munmodify!=null) {
965             for(int i=0;i<state.vRules.size();i++) {
966                 Rule r=(Rule)state.vRules.get(i);
967                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
968                     for(int j=0;j<munmodify.numUpdates();j++) {
969                         UpdateNode un=munmodify.getUpdate(j);
970                         if (un.getRule()==r) {
971                             /* Update for rule r */
972                             String name=(String)updatenames.get(un);
973                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+","+newvalue.getSafeSymbol()+");");
974                         }
975                     }
976                 }
977             }
978
979         } else {
980             /* Start with scheduling removal */
981             for(int i=0;i<state.vRules.size();i++) {
982                 Rule r=(Rule)state.vRules.get(i);
983                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
984                     for(int j=0;j<munremove.numUpdates();j++) {
985                         UpdateNode un=munremove.getUpdate(i);
986                         if (un.getRule()==r) {
987                             /* Update for rule r */
988                             String name=(String)updatenames.get(un);
989                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
990                         }
991                     }
992                 }
993             }
994             /* Now do addition */
995             UpdateNode un=munadd.getUpdate(0);
996             String name=(String)updatenames.get(un);
997             if (!inverted) {
998                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
999             } else {
1000                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
1001             }
1002         }
1003     }
1004
1005     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
1006         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
1007         OpExpr expr=(OpExpr)ep.expr;
1008         Opcode opcode=expr.getOpcode();
1009         opcode=Opcode.translateOpcode(dpred.isNegated(),opcode);
1010
1011         MultUpdateNode munremove;
1012
1013         MultUpdateNode munadd;
1014         if (ep.getDescriptor() instanceof RelationDescriptor) {
1015             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
1016             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
1017         } else {
1018             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
1019             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
1020         }
1021         int size=ep.rightSize();
1022         VarDescriptor sizevar=VarDescriptor.makeNew("size");
1023         ((OpExpr)expr).left.generate(cr, sizevar);
1024         VarDescriptor change=VarDescriptor.makeNew("change");
1025         cr.outputline("int "+change.getSafeSymbol()+";");
1026         boolean generateadd=false;
1027         boolean generateremove=false;
1028         if (opcode==Opcode.GT) {
1029             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
1030             generateadd=true;
1031             generateremove=false;
1032         } else if (opcode==Opcode.GE) {
1033             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1034             generateadd=true;
1035             generateremove=false;
1036         } else if (opcode==Opcode.LT) {
1037             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
1038             generateadd=false;
1039             generateremove=true;
1040         } else if (opcode==Opcode.LE) {
1041             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1042             generateadd=false;
1043             generateremove=true;
1044         } else if (opcode==Opcode.EQ) {
1045             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1046             if (size==0)
1047                 generateadd=false;
1048             else 
1049                 generateadd=true;
1050             generateremove=true;
1051         } else if (opcode==Opcode.NE) {
1052             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
1053             generateadd=true;
1054             generateremove=false;
1055         } else {
1056             throw new Error("Unrecognized Opcode");
1057         }
1058
1059 // In some cases the analysis has determined that generating removes
1060 // is unnecessary
1061         if (generateremove&&munremove==null) 
1062             generateremove=false;
1063
1064         Descriptor d=ep.getDescriptor();
1065         if (generateremove) {
1066             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
1067             cr.startblock();
1068             /* Find element to remove */
1069             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
1070             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
1071             if (d instanceof RelationDescriptor) {
1072                 if (ep.inverted()) {
1073                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1074                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
1075                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1076                 } else {
1077                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1078                     cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
1079                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1080                 }
1081             } else {
1082                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
1083             }
1084             /* Generate abstract remove instruction */
1085             if (d instanceof RelationDescriptor) {
1086                 RelationDescriptor rd=(RelationDescriptor) d;
1087                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1088                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1089                 if (usageimage)
1090                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1091                 if (usageinvimage)
1092                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1093             } else {
1094                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1095             }
1096             /* Generate concrete remove instruction */
1097             for(int i=0;i<state.vRules.size();i++) {
1098                 Rule r=(Rule)state.vRules.get(i);
1099                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
1100                     for(int j=0;j<munremove.numUpdates();j++) {
1101                         UpdateNode un=munremove.getUpdate(j);
1102                         if (un.getRule()==r) {
1103                                 /* Update for rule rule r */
1104                             String name=(String)updatenames.get(un);
1105                             if (d instanceof RelationDescriptor) {
1106                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1107                             } else {
1108                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1109                             }
1110                         }
1111                     }
1112                 }
1113             }
1114             cr.endblock();
1115         }
1116         if (generateadd) {
1117
1118             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
1119             cr.startblock();
1120             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
1121             if (d instanceof RelationDescriptor) {
1122                 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
1123                 RelationDescriptor rd=(RelationDescriptor)d;
1124                 if (termination.sources.relsetSource(rd,!ep.inverted())) {
1125                     /* Set Source */
1126                     SetDescriptor sd=termination.sources.relgetSourceSet(rd,!ep.inverted());
1127                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1128                     cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1129                     cr.outputline("SimpleIterator "+iterator.getSafeSymbol()+";");
1130                     cr.outputline("for("+sd.getSafeSymbol()+"_hash->iterator("+ iterator.getSafeSymbol() +");"+iterator.getSafeSymbol()+".hasNext();)");
1131                     cr.startblock();
1132                     if (ep.inverted()) {
1133                         cr.outputline("if (!"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+".key(),"+otherside.getSafeSymbol()+"))");
1134                     } else {
1135                         cr.outputline("if (!"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+".key()))");
1136                     }
1137                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1138                     cr.outputline(iterator.getSafeSymbol()+".next();");
1139                     cr.endblock();
1140                 } else if (termination.sources.relallocSource(rd,!ep.inverted())) {
1141                     /* Allocation Source*/
1142                     termination.sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
1143                 } else throw new Error("No source for adding to Relation");
1144                 if (ep.inverted()) {
1145                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1146                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1147                     if (usageimage)
1148                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1149                     if (usageinvimage)
1150                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1151
1152                     UpdateNode un=munadd.getUpdate(0);
1153                     String name=(String)updatenames.get(un);
1154                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1155                 } else {
1156                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1157                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1158                     if (usageimage)
1159                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1160                     if (usageinvimage)
1161                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1162                     UpdateNode un=munadd.getUpdate(0);
1163                     String name=(String)updatenames.get(un);
1164                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1165                 }
1166             } else {
1167                 SetDescriptor sd=(SetDescriptor)d;
1168                 if (termination.sources.setSource(sd)) {
1169                     /* Set Source */
1170                     /* Set Source */
1171                     SetDescriptor sourcesd=termination.sources.getSourceSet(sd);
1172                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1173                     cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1174                     cr.outputline("SimpleIterator "+iterator.getSafeSymbol()+";");
1175                     cr.outputline("for("+sourcesd.getSafeSymbol()+"_hash->iterator("+iterator.getSafeSymbol()+");"+iterator.getSafeSymbol()+".hasNext();)");
1176                     cr.startblock();
1177                     cr.outputline("if (!"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+".key()))");
1178                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1179                     cr.outputline(iterator.getSafeSymbol()+".next();");
1180                     cr.endblock();
1181                 } else if (termination.sources.allocSource(sd)) {
1182                     /* Allocation Source*/
1183                     termination.sources.generateSourceAlloc(cr,newobject,sd);
1184                 } else throw new Error("No source for adding to Set");
1185                 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1186                 UpdateNode un=munadd.getUpdate(0);
1187                 String name=(String)updatenames.get(un);
1188                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1189             }
1190             cr.endblock();
1191         }
1192     }
1193
1194     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1195         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
1196         boolean negated=dpred.isNegated();
1197         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
1198         VarDescriptor leftvar=VarDescriptor.makeNew("left");
1199         ip.expr.generate(cr, leftvar);
1200
1201         if (negated) {
1202             if (ip.setexpr instanceof ImageSetExpr) {
1203                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1204                 VarDescriptor rightvar=ise.getVar();
1205                 boolean inverse=ise.inverted();
1206                 RelationDescriptor rd=ise.getRelation();
1207                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1208                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1209                 if (inverse) {
1210                     if (usageimage)
1211                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1212                     if (usageinvimage)
1213                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1214                 } else {
1215                     if (usageimage)
1216                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1217                     if (usageinvimage)
1218                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1219                 }
1220                 for(int i=0;i<state.vRules.size();i++) {
1221                     Rule r=(Rule)state.vRules.get(i);
1222                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1223                         for(int j=0;j<mun.numUpdates();j++) {
1224                             UpdateNode un=mun.getUpdate(j);
1225                             if (un.getRule()==r) {
1226                                 /* Update for rule rule r */
1227                                 String name=(String)updatenames.get(un);
1228                                 if (inverse) {
1229                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1230                                 } else {
1231                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1232                                 }
1233                             }
1234                         }
1235                     }
1236                 }
1237             } else {
1238                 SetDescriptor sd=ip.setexpr.sd;
1239                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1240
1241                 for(int i=0;i<state.vRules.size();i++) {
1242                     Rule r=(Rule)state.vRules.get(i);
1243                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1244                         for(int j=0;j<mun.numUpdates();j++) {
1245                             UpdateNode un=mun.getUpdate(j);
1246                             if (un.getRule()==r) {
1247                                 /* Update for rule rule r */
1248                                 String name=(String)updatenames.get(un);
1249                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1250                             }
1251                         }
1252                     }
1253                 }
1254             }
1255         } else {
1256             /* Generate update */
1257             if (ip.setexpr instanceof ImageSetExpr) {
1258                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1259                 VarDescriptor rightvar=ise.getVar();
1260                 boolean inverse=ise.inverted();
1261                 RelationDescriptor rd=ise.getRelation();
1262                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1263                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1264                 if (inverse) {
1265                     if (usageimage)
1266                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1267                     if (usageinvimage)
1268                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1269                 } else {
1270                     if (usageimage)
1271                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1272                     if (usageinvimage)
1273                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1274                 }
1275                 UpdateNode un=mun.getUpdate(0);
1276                 String name=(String)updatenames.get(un);
1277                 if (inverse) {
1278                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1279                 } else {
1280                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1281                 }
1282             } else {
1283                 SetDescriptor sd=ip.setexpr.sd;
1284                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1285
1286                 UpdateNode un=mun.getUpdate(0);
1287                 /* Update for rule rule r */
1288                 String name=(String)updatenames.get(un);
1289                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1290             }
1291         }
1292     }
1293
1294     public static Vector getrulelist(Descriptor d) {
1295         Vector dispatchrules = new Vector();
1296         Vector rules = State.currentState.vRules;
1297
1298         for (int i = 0; i < rules.size(); i++) {
1299             Rule rule = (Rule) rules.elementAt(i);
1300             Set requiredsymbols = rule.getRequiredDescriptors();
1301             
1302             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1303             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1304             // fashion...
1305
1306             if (rule.getRequiredDescriptors().contains(d)) {
1307                 dispatchrules.addElement(rule);
1308             }
1309         }
1310         return dispatchrules;
1311     }
1312
1313     private boolean need_compensation(Rule r) {
1314         if (!Compiler.REPAIR)
1315             return false;
1316         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1317         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1318             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1319             GraphNode gn2=edge.getTarget();
1320             if (!removed.contains(gn2)) {
1321                 TermNode tn2=(TermNode)gn2.getOwner();
1322                 if (tn2.getType()==TermNode.CONSEQUENCE)
1323                     return false;
1324             }
1325         }
1326         return true;
1327     }
1328
1329     private UpdateNode find_compensation(Rule r) {
1330         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1331         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1332             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1333             GraphNode gn2=edge.getTarget();
1334             if (!removed.contains(gn2)) {
1335                 TermNode tn2=(TermNode)gn2.getOwner();
1336                 if (tn2.getType()==TermNode.UPDATE) {
1337                     MultUpdateNode mun=tn2.getUpdate();
1338                     for(int i=0;i<mun.numUpdates();i++) {
1339                         UpdateNode un=mun.getUpdate(i);
1340                         if (un.getRule()==r)
1341                             return un;
1342                     }
1343                 }
1344             }
1345         }
1346         throw new Error("No Compensation Update could be found");
1347     }
1348
1349     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1350         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1351         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1352
1353         if (!(usageinvimage||usageimage)) /* not used at all*/
1354             return;
1355
1356         cr.outputline("// RELATION DISPATCH ");
1357         if (Compiler.REPAIR) {
1358             cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1359             if (usageimage)
1360                 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1361             else
1362                 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1363
1364             cr.startblock(); {
1365                 /* Adding new item */
1366                 /* Perform safety checks */
1367                 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1368                 cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1369                 cr.startblock(); {
1370                     /* Have update to call into */
1371                     VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr");
1372                     VarDescriptor ismdfyptr=VarDescriptor.makeNew("ismodifyptr");
1373                     cr.outputline("int "+ismdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->ismodify("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1374
1375
1376
1377                     
1378                     String parttype="";
1379                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1380                         if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1381                             parttype=parttype+", int, int";
1382                         else
1383                             parttype=parttype+", int";
1384                     }
1385                     VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1386                     VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr");
1387                     
1388                     String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1389                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1390                         Quantifier q=currentrule.getQuantifier(i);
1391                         if (q instanceof SetQuantifier) {
1392                             SetQuantifier sq=(SetQuantifier) q;
1393                             methodcall+=","+sq.getVar().getSafeSymbol();
1394                         } else if (q instanceof RelationQuantifier) {
1395                             RelationQuantifier rq=(RelationQuantifier) q;
1396                             methodcall+=","+rq.x.getSafeSymbol();
1397                             methodcall+=","+rq.y.getSafeSymbol();
1398                         } else if (q instanceof ForQuantifier) {
1399                             ForQuantifier fq=(ForQuantifier) q;
1400                             methodcall+=","+fq.getVar().getSafeSymbol();
1401                         }
1402                     }
1403                     
1404                     
1405                     
1406                     cr.outputline("void *"+tmpptr.getSafeSymbol()+"=");
1407                     cr.outputline("(void *) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1408                     cr.outputline("if ("+ismdfyptr.getSafeSymbol()+")");
1409                     {
1410                         cr.startblock();
1411                         cr.outputline("int "+mdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->getrelation2("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1412                         cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+",int,int,int)) "+tmpptr.getSafeSymbol()+";");
1413                         cr.outputline(methodcall+","+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
1414                         cr.endblock();
1415                     }
1416                     cr.outputline("else ");
1417                     {
1418                         cr.startblock();
1419                         cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol()+";");
1420                         cr.outputline(methodcall+");");
1421                         cr.endblock();
1422                     }
1423                     cr.outputline("delete "+newmodel.getSafeSymbol()+";");
1424                     cr.outputline("goto rebuild;");
1425                 }
1426                 cr.endblock();
1427                 
1428                 /* Build standard compensation actions */
1429                 if (need_compensation(currentrule)) {
1430                     UpdateNode un=find_compensation(currentrule);
1431                     String name=(String)updatenames.get(un);
1432                     usedupdates.add(un); /* Mark as used */
1433                     String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1434                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1435                         Quantifier q=currentrule.getQuantifier(i);
1436                         if (q instanceof SetQuantifier) {
1437                             SetQuantifier sq=(SetQuantifier) q;
1438                             methodcall+=","+sq.getVar().getSafeSymbol();
1439                         } else if (q instanceof RelationQuantifier) {
1440                             RelationQuantifier rq=(RelationQuantifier) q;
1441                             methodcall+=","+rq.x.getSafeSymbol();
1442                             methodcall+=","+rq.y.getSafeSymbol();
1443                         } else if (q instanceof ForQuantifier) {
1444                             ForQuantifier fq=(ForQuantifier) q;
1445                             methodcall+=","+fq.getVar().getSafeSymbol();
1446                         }
1447                     }
1448                     methodcall+=");";
1449                     cr.outputline(methodcall);
1450                     cr.outputline("delete "+newmodel.getSafeSymbol()+";");
1451                     cr.outputline("goto rebuild;");
1452                 }
1453             }
1454             cr.endblock();
1455         }
1456
1457         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1458         cr.outputline("int " + addeditem + "=0;");
1459
1460         String ifstring="if (!maybe&&";
1461         boolean dogenerate=false;
1462         if (rd.getDomain().getType() instanceof StructureTypeDescriptor)  {
1463             dogenerate=true;
1464             ifstring+=leftvar;
1465         }
1466
1467         if (rd.getRange().getType() instanceof StructureTypeDescriptor)  {
1468             if (dogenerate)
1469                 ifstring+="&&"+rightvar;
1470             else
1471                 ifstring+=rightvar;
1472             dogenerate=true;
1473         }
1474
1475         ifstring+=")";
1476
1477         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1478             cr.outputline(ifstring);
1479             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar+ ");");
1480         }
1481         
1482         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1483             cr.outputline(ifstring);
1484             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1485         }
1486         
1487
1488         Vector dispatchrules = getrulelist(rd);
1489         
1490         Set toremove=new HashSet();
1491         for(int i=0;i<dispatchrules.size();i++) {
1492             Rule r=(Rule)dispatchrules.get(i);
1493             if (!ruleset.contains(r))
1494                 toremove.add(r);
1495         }
1496         dispatchrules.removeAll(toremove);
1497         if (dispatchrules.size() == 0) {
1498             cr.outputline("// nothing to dispatch");
1499             return;
1500         }
1501
1502         cr.outputline("if (" + addeditem + ")");
1503         cr.startblock();
1504        
1505         for(int i = 0; i < dispatchrules.size(); i++) {
1506             Rule rule = (Rule) dispatchrules.elementAt(i);
1507             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1508                 /* Guard depends on this relation, so we recomput everything */
1509                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1510             } else {
1511                 for (int j=0;j<rule.numQuantifiers();j++) {
1512                     Quantifier q=rule.getQuantifier(j);
1513                     if (q.getRequiredDescriptors().contains(rd)) {
1514                         /* Generate add */
1515                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1516                     }
1517                 }
1518             }
1519         }
1520
1521         cr.endblock();
1522     }
1523
1524
1525     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1526                
1527         cr.outputline("// SET DISPATCH ");
1528         if (Compiler.REPAIR) {
1529             cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1530             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1531             cr.startblock(); {
1532                 /* Adding new item */
1533                 /* Perform safety checks */
1534                 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1535                 cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1536                 cr.startblock(); {
1537                     /* Have update to call into */
1538                     VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1539                     String parttype="";
1540                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1541                         if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1542                             parttype=parttype+", int, int";
1543                         else
1544                             parttype=parttype+", int";
1545                     }
1546                     cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1547                     cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1548                     String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1549                         repairtable.getSafeSymbol();
1550                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1551                         Quantifier q=currentrule.getQuantifier(i);
1552                         if (q instanceof SetQuantifier) {
1553                             SetQuantifier sq=(SetQuantifier) q;
1554                             methodcall+=","+sq.getVar().getSafeSymbol();
1555                         } else if (q instanceof RelationQuantifier) {
1556                             RelationQuantifier rq=(RelationQuantifier) q;
1557                             methodcall+=","+rq.x.getSafeSymbol();
1558                             methodcall+=","+rq.y.getSafeSymbol();
1559                         } else if (q instanceof ForQuantifier) {
1560                             ForQuantifier fq=(ForQuantifier) q;
1561                             methodcall+=","+fq.getVar().getSafeSymbol();
1562                         }
1563                     }
1564                     methodcall+=");";
1565                     cr.outputline(methodcall);
1566                     cr.outputline("delete "+newmodel.getSafeSymbol()+";");
1567                     cr.outputline("goto rebuild;");
1568                 }
1569                 cr.endblock();
1570                 /* Build standard compensation actions */
1571                 if (need_compensation(currentrule)) {
1572                     UpdateNode un=find_compensation(currentrule);
1573                     String name=(String)updatenames.get(un);
1574                     usedupdates.add(un); /* Mark as used */
1575                     
1576                     String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1577                         repairtable.getSafeSymbol();
1578                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1579                         Quantifier q=currentrule.getQuantifier(i);
1580                         if (q instanceof SetQuantifier) {
1581                             SetQuantifier sq=(SetQuantifier) q;
1582                             methodcall+=","+sq.getVar().getSafeSymbol();
1583                         } else if (q instanceof RelationQuantifier) {
1584                             RelationQuantifier rq=(RelationQuantifier) q;
1585                             methodcall+=","+rq.x.getSafeSymbol();
1586                             methodcall+=","+rq.y.getSafeSymbol();
1587                         } else if (q instanceof ForQuantifier) {
1588                             ForQuantifier fq=(ForQuantifier) q;
1589                             methodcall+=","+fq.getVar().getSafeSymbol();
1590                         }
1591                     }
1592                     methodcall+=");";
1593                     cr.outputline(methodcall);
1594                     cr.outputline("delete "+newmodel.getSafeSymbol()+";");
1595                     cr.outputline("goto rebuild;");
1596                 }
1597             }
1598             cr.endblock();
1599         }
1600
1601         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1602         cr.outputline("int " + addeditem + " = 0;");
1603         if (sd.getType() instanceof StructureTypeDescriptor)  {
1604             cr.outputline("if (!maybe&&"+setvar+")");
1605         } else
1606             cr.outputline("if (!maybe)");
1607         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1608         cr.startblock();
1609         Vector dispatchrules = getrulelist(sd);
1610
1611         Set toremove=new HashSet();
1612         for(int i=0;i<dispatchrules.size();i++) {
1613             Rule r=(Rule)dispatchrules.get(i);
1614             if (!ruleset.contains(r))
1615                 toremove.add(r);
1616         }
1617         dispatchrules.removeAll(toremove);
1618
1619         if (dispatchrules.size() == 0) {
1620             cr.outputline("// nothing to dispatch");
1621             cr.endblock();
1622             return;
1623         }
1624         cr.outputline("if ("+addeditem+")");
1625         cr.startblock();
1626         for(int i = 0; i < dispatchrules.size(); i++) {
1627             Rule rule = (Rule) dispatchrules.elementAt(i);
1628             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1629                 /* Guard depends on this relation, so we recompute everything */
1630                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1631             } else {
1632                 for (int j=0;j<rule.numQuantifiers();j++) {
1633                     Quantifier q=rule.getQuantifier(j);
1634                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1635                         /* Generate add */
1636                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1637                     }
1638                 }
1639             }
1640         }
1641         cr.endblock();
1642         cr.endblock();
1643     }
1644 }