046e06062ba0481f9f21aa9a4d270f8475c9dc02
[repair.git] / Repair / RepairCompiler / MCC / IR / Termination.java
1 package MCC.IR;
2 import java.util.*;
3 import java.io.*;
4 import MCC.State;
5 import MCC.Compiler;
6
7 public class Termination {
8     HashSet conjunctions;
9     Hashtable conjunctionmap;
10
11     HashSet abstractrepair;
12     HashSet abstractrepairadd;
13
14     HashSet updatenodes;
15     HashSet consequencenodes;
16
17     HashSet scopenodes;
18     Hashtable scopesatisfy;
19     Hashtable scopefalsify;
20     Hashtable consequence;
21     Hashtable abstractadd;
22     Hashtable abstractremove;
23     Hashtable conjtonodemap;
24     Hashtable predtoabstractmap;
25     Set removedset;
26     ComputeMaxSize maxsize;
27     State state;
28     AbstractInterferes abstractinterferes;
29     ConcreteInterferes concreteinterferes;
30     ConstraintDependence constraintdependence;
31     ExactSize exactsize;
32     ArrayAnalysis arrayanalysis;
33     Sources sources;
34     static String conjoption="style=bold";
35     static String absrepoption="shape=box,color=blue,style=bold";
36     static String updateoption="shape=box,color=red,style=bold";
37     static String scopeoption="color=brown";
38     static String conseqoption="style=bold,color=green";
39     static String compoption="shape=box,color=purple,style=bold";
40
41     public Termination(State state) {
42         this.state=state;
43         conjunctions=new HashSet();
44         conjunctionmap=new Hashtable();
45         abstractrepair=new HashSet();
46         abstractrepairadd=new HashSet();
47         scopenodes=new HashSet();
48         scopesatisfy=new Hashtable();
49         scopefalsify=new Hashtable();
50         consequence=new Hashtable();
51         updatenodes=new HashSet();
52         consequencenodes=new HashSet();
53         abstractadd=new Hashtable();
54         abstractremove=new Hashtable();
55         conjtonodemap=new Hashtable();
56         predtoabstractmap=new Hashtable();
57         if (!Compiler.REPAIR)
58             return;
59
60
61         for(int i=0;i<state.vRules.size();i++)
62             System.out.println(state.vRules.get(i));
63         for(int i=0;i<state.vConstraints.size();i++)
64             System.out.println(state.vConstraints.get(i));
65
66         sources=new Sources(state);
67         maxsize=new ComputeMaxSize(state);
68         exactsize=new ExactSize(state);
69         arrayanalysis=new ArrayAnalysis(state,this);
70
71         abstractinterferes=new AbstractInterferes(this);
72         concreteinterferes=new ConcreteInterferes(this);
73         generateconjunctionnodes();
74         constraintdependence=new ConstraintDependence(state,this);
75
76         debugmsg("*****Generating scope nodes*****");
77         generatescopenodes();
78         debugmsg("*****Generating repair nodes*****");
79         generaterepairnodes();
80         debugmsg("*****Generating data structure nodes*****");
81         generatedatastructureupdatenodes();
82         debugmsg("*****Generating compensation nodes*****");
83         if (!Compiler.OMITCOMP)
84             generatecompensationnodes();
85         debugmsg("*****Generating abstract edges*****");
86         generateabstractedges();
87         debugmsg("*****Generating scope edges*****");
88         generatescopeedges();
89         debugmsg("*****Generating update edges*****");
90         generateupdateedges();
91
92
93         HashSet superset=new HashSet();
94         superset.addAll(conjunctions);
95         HashSet closureset=new HashSet();
96         debugmsg("Computing closure");
97         GraphNode.computeclosure(superset,closureset);
98         try {
99             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
100         } catch (Exception e) {
101             e.printStackTrace();
102             System.exit(-1);
103         }
104
105         generatedebuggraphs();
106
107         for(Iterator it=updatenodes.iterator();it.hasNext();) {
108             GraphNode gn=(GraphNode)it.next();
109             TermNode tn=(TermNode)gn.getOwner();
110             MultUpdateNode mun=tn.getUpdate();
111             System.out.println(gn.getTextLabel());
112             System.out.println(mun.toString());
113         }
114         GraphAnalysis ga=new GraphAnalysis(this);
115         removedset=ga.doAnalysis();
116         if (removedset==null) {
117             System.out.println("Can't generate terminating repair algorithm!");
118             System.exit(-1);
119         }
120
121         System.out.println("Removing:");
122         for(Iterator it=removedset.iterator();it.hasNext();) {
123             GraphNode gn=(GraphNode)it.next();
124             System.out.println(gn.getTextLabel());
125         }
126
127         superset=new HashSet();
128         superset.addAll(conjunctions);
129         superset.removeAll(removedset);
130         GraphNode.computeclosure(superset,removedset);
131         try {
132             GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
133         } catch (Exception e) {
134             e.printStackTrace();
135             System.exit(-1);
136         }
137         constraintdependence.traversedependences(this);
138     }
139
140     void generatedebuggraphs() {
141         for (int i=0;i<Compiler.debuggraphs.size();i++) {
142             DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
143             HashSet superset=new HashSet();
144             Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
145
146             if (di.conjunctionnum==-1) {
147                 superset.addAll((Set)conjunctionmap.get(constr));
148             } else {
149                 DNFConstraint dnf=constr.dnfconstraint;
150                 superset.add(conjtonodemap.get(dnf.get(di.conjunctionnum)));
151             }
152
153             GraphNode.boundedcomputeclosure(superset,null,di.depth);
154             try {
155                 GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+(di.conjunctionnum==-1?"":"-"+di.conjunctionnum)+".dot"),superset);
156             } catch (Exception e) {
157                 e.printStackTrace();
158                 System.exit(-1);
159             }
160         }
161     }
162
163
164     /** This method generates a node for each conjunction in the DNF
165      * form of each constraint.  It also converts the quantifiers into
166      * conjunctions also - constraints can be satisfied by removing
167      * items from the sets and relations they are quantified over */
168
169     void generateconjunctionnodes() {
170         Vector constraints=state.vConstraints;
171         // Constructs conjunction nodes
172         for(int i=0;i<constraints.size();i++) {
173             Constraint c=(Constraint)constraints.get(i);
174             DNFConstraint dnf=c.dnfconstraint;
175             for(int j=0;j<dnf.size();j++) {
176                 TermNode tn=new TermNode(c,dnf.get(j));
177                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
178                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
179                                            ,tn);
180                 gn.setOption(conjoption);
181                 conjunctions.add(gn);
182                 if (!conjunctionmap.containsKey(c))
183                     conjunctionmap.put(c,new HashSet());
184                 ((Set)conjunctionmap.get(c)).add(gn);
185                 conjtonodemap.put(dnf.get(j),gn);
186             }
187             // Construct quantifier "conjunction" nodes
188             for(int j=0;j<c.numQuantifiers();j++) {
189                 Quantifier q=c.getQuantifier(j);
190                 if (q instanceof SetQuantifier) {
191                     SetQuantifier sq=(SetQuantifier)q;
192                     VarExpr ve=new VarExpr(sq.getVar());
193                     InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
194                     DNFConstraint dconst=new DNFConstraint(ip);
195                     dconst=dconst.not();
196                     TermNode tn=new TermNode(c,dconst.get(0));
197                     tn.setquantifiernode();
198                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
199                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
200                                                ,tn);
201                     gn.setOption(conjoption);
202                     conjunctions.add(gn);
203                     if (!conjunctionmap.containsKey(c))
204                         conjunctionmap.put(c,new HashSet());
205                     ((Set)conjunctionmap.get(c)).add(gn);
206                     conjtonodemap.put(dconst.get(0),gn);
207
208                 } else if (q instanceof RelationQuantifier) {
209                     RelationQuantifier rq=(RelationQuantifier)q;
210                     VarExpr ve=new VarExpr(rq.y);
211                     InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
212                     DNFConstraint dconst=new DNFConstraint(ip);
213                     dconst=dconst.not();
214                     TermNode tn=new TermNode(c,dconst.get(0));
215                     tn.setquantifiernode();
216                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
217                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
218                                                ,tn);
219                     gn.setOption(conjoption);
220                     conjunctions.add(gn);
221                     if (!conjunctionmap.containsKey(c))
222                         conjunctionmap.put(c,new HashSet());
223                     ((Set)conjunctionmap.get(c)).add(gn);
224                     conjtonodemap.put(dconst.get(0),gn);
225                 }
226             }
227         }
228     }
229
230     void generateupdateedges() {
231         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
232             GraphNode gn=(GraphNode)updateiterator.next();
233             TermNode tn=(TermNode)gn.getOwner();
234             MultUpdateNode mun=tn.getUpdate();
235             for(int i=0;i<mun.numUpdates();i++) {
236                 UpdateNode un=mun.getUpdate(i);
237                 for(int j=0;j<un.numUpdates();j++) {
238                     Updates u=un.getUpdate(j);
239                     if (u.getType()==Updates.ABSTRACT) {
240                         Expr e=u.getLeftExpr();
241                         boolean negated=u.negate;
242                         if (e instanceof TupleOfExpr) {
243                             TupleOfExpr toe=(TupleOfExpr)e;
244                             if (negated) {
245                                 GraphNode agn=(GraphNode)abstractremove.get(toe.relation);
246                                 GraphNode.Edge edge=new GraphNode.Edge("requirestupleremove",agn);
247                                 gn.addEdge(edge);
248                             } else {
249                                 GraphNode agn=(GraphNode)abstractadd.get(toe.relation);
250                                 GraphNode.Edge edge=new GraphNode.Edge("requirestupleadd",agn);
251                                 gn.addEdge(edge);
252                             }
253                         } else if (e instanceof ElementOfExpr) {
254                             ElementOfExpr eoe=(ElementOfExpr)e;
255                             if (negated) {
256                                 GraphNode agn=(GraphNode)abstractremove.get(eoe.set);
257                                 GraphNode.Edge edge=new GraphNode.Edge("requireselementremove",agn);
258                                 gn.addEdge(edge);
259                             } else {
260                                 GraphNode agn=(GraphNode)abstractadd.get(eoe.set);
261                                 GraphNode.Edge edge=new GraphNode.Edge("requireselementadd",agn);
262                                 gn.addEdge(edge);
263                             }
264                         } else throw new Error("Unrecognized Abstract Update");
265                     }
266                 }
267             }
268             /* Cycle through the rules to look for possible conflicts */
269             for(int i=0;i<state.vRules.size();i++) {
270                 Rule r=(Rule) state.vRules.get(i);
271                 if (Compiler.DEBUGGRAPH) {
272                     System.out.println(gn.getLabel()+"--->"+((GraphNode)scopesatisfy.get(r)).getLabel());
273                 }
274                 if (concreteinterferes.interferes(mun,r,true)) {
275                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
276                     GraphNode.Edge e=new GraphNode.Edge("satisfyscopeinterferes",scopenode);
277                     gn.addEdge(e);
278                 }
279                 if (Compiler.DEBUGGRAPH) {
280                     System.out.println(gn.getLabel()+"--->"+((GraphNode)scopefalsify.get(r)).getLabel());
281                 }
282                 if (concreteinterferes.interferes(mun,r,false)) {
283                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
284                     GraphNode.Edge e=new GraphNode.Edge("falsifyscopeinterferes",scopenode);
285                     gn.addEdge(e);
286                 }
287             }
288         }
289     }
290
291     void generateabstractedges() {
292         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
293             GraphNode gn=(GraphNode)absiterator.next();
294             TermNode tn=(TermNode)gn.getOwner();
295             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
296
297             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
298                 GraphNode gn2=(GraphNode)conjiterator.next();
299                 TermNode tn2=(TermNode)gn2.getOwner();
300                 Conjunction conj=tn2.getConjunction();
301                 Constraint cons=tn2.getConstraint();
302                 /* See if this is a relation wellformedness constraint
303                    that is trivially satisfied. */
304                 if (abstractinterferes.checkrelationconstraint(ar, cons))
305                     continue;
306                 if (AbstractInterferes.interferesquantifier(ar,cons)) {
307                     GraphNode.Edge e=new GraphNode.Edge("interferesquantifier",gn2);
308                     gn.addEdge(e);
309                 } else {
310                     for(int i=0;i<conj.size();i++) {
311                         DNFPredicate dp=conj.get(i);
312
313                         if (!abstractinterferes.interfereswithpredicate(ar,dp))
314                             continue;
315                         if (getConstraint(gn)==null||
316                             !abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons)) {
317                             GraphNode.Edge e=new GraphNode.Edge("interferesmodify",gn2);
318                             gn.addEdge(e);
319                             break;
320                         }
321                     }
322                 }
323             }
324             for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
325                 GraphNode gn2=(GraphNode)scopeiterator.next();
326                 TermNode tn2=(TermNode)gn2.getOwner();
327                 ScopeNode sn2=tn2.getScope();
328                 if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
329                     GraphNode.Edge e=new GraphNode.Edge("interfereswithrule",gn2);
330                     gn.addEdge(e);
331                 }
332             }
333         }
334     }
335
336     Constraint getConstraint(GraphNode gn) {
337         for(Iterator it=gn.inedges();it.hasNext();) {
338             GraphNode.Edge e=(GraphNode.Edge)it.next();
339             GraphNode gnsource=e.getSource();
340             TermNode tnsource=(TermNode)gnsource.getOwner();
341             if (tnsource.getType()==TermNode.CONJUNCTION) {
342                 return tnsource.getConstraint();
343             }
344         }
345         return null;
346     }
347
348     void generatescopenodes() {
349         for(int i=0;i<state.vRules.size();i++) {
350             Rule r=(Rule) state.vRules.get(i);
351             ScopeNode satisfy=new ScopeNode(r,true);
352             TermNode tnsatisfy=new TermNode(satisfy);
353             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
354             gnsatisfy.setOption(scopeoption);
355             if (Compiler.MERGENODES)
356                 gnsatisfy.setMerge();
357             ConsequenceNode cnsatisfy=new ConsequenceNode();
358             TermNode ctnsatisfy=new TermNode(cnsatisfy);
359             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
360             cgnsatisfy.setOption(conseqoption);
361             consequence.put(satisfy,cgnsatisfy);
362             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
363             gnsatisfy.addEdge(esat);
364             consequencenodes.add(cgnsatisfy);
365             scopesatisfy.put(r,gnsatisfy);
366             scopenodes.add(gnsatisfy);
367
368             ScopeNode falsify=new ScopeNode(r,false);
369             TermNode tnfalsify=new TermNode(falsify);
370             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
371             gnfalsify.setOption(scopeoption);
372             if (Compiler.MERGENODES)
373                 gnfalsify.setMerge();
374             ConsequenceNode cnfalsify=new ConsequenceNode();
375             TermNode ctnfalsify=new TermNode(cnfalsify);
376             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
377             cgnfalsify.setOption(conseqoption);
378             consequence.put(falsify,cgnfalsify);
379             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
380             gnfalsify.addEdge(efals);
381             consequencenodes.add(cgnfalsify);
382             scopefalsify.put(r,gnfalsify);
383             scopenodes.add(gnfalsify);
384         }
385     }
386
387     void generatescopeedges() {
388         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
389             GraphNode gn=(GraphNode)scopeiterator.next();
390             TermNode tn=(TermNode)gn.getOwner();
391             ScopeNode sn=tn.getScope();
392
393             /* Interference edges with conjunctions */
394             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
395                 GraphNode gn2=(GraphNode)conjiterator.next();
396                 TermNode tn2=(TermNode)gn2.getOwner();
397                 Conjunction conj=tn2.getConjunction();
398                 Constraint constr=tn2.getConstraint();
399                 for(int i=0;i<conj.size();i++) {
400                     DNFPredicate dp=conj.get(i);
401                     if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
402                         AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
403                         GraphNode.Edge e=new GraphNode.Edge("interferesconjunction",gn2);
404                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
405                         gnconseq.addEdge(e);
406                         break;
407                     }
408                 }
409             }
410
411             /* Now see if this could effect other model defintion rules */
412             for(int i=0;i<state.vRules.size();i++) {
413                 Rule r=(Rule) state.vRules.get(i);
414                 if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
415                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
416                     GraphNode.Edge e=new GraphNode.Edge("interferesscopesatisfy2",scopenode);
417                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
418                     gnconseq.addEdge(e);
419                 }
420                 if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
421                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
422                     GraphNode.Edge e=new GraphNode.Edge("interferesscopefalsify2",scopenode);
423                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
424                     gnconseq.addEdge(e);
425                 }
426             }
427         }
428     }
429
430     /** This method generates the abstract repair nodes. */
431     void generaterepairnodes() {
432         /* Generate repairs of conjunctions */
433         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
434             GraphNode gn=(GraphNode)conjiterator.next();
435             TermNode tn=(TermNode)gn.getOwner();
436             Conjunction conj=tn.getConjunction();
437         loop:
438             for(int i=0;i<conj.size();i++) {
439                 DNFPredicate dp=conj.get(i);
440                 int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
441                 Descriptor d=dp.getPredicate().getDescriptor();
442                 if ((dp.getPredicate() instanceof ExprPredicate)&&
443                     (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
444                     boolean neg=dp.isNegated();
445                     Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
446                     int size=((ExprPredicate)dp.getPredicate()).rightSize();
447                     op=Opcode.translateOpcode(neg,op);
448                     if (((size==1)&&(op==Opcode.EQ))||
449                         ((size!=1)&&(op==Opcode.NE))||
450                         ((size<=1)&&(op==Opcode.GE))||
451                         ((size<1)&&(op==Opcode.GT))||
452                         ((size>1)&&(op==Opcode.LT))||
453                         ((size>=1)&&(op==Opcode.LE))) {
454                         for(int i2=0;i2<conj.size();i2++) {
455                             DNFPredicate dp2=conj.get(i2);
456                             if ((dp2.getPredicate() instanceof ExprPredicate)&&
457                                 (((ExprPredicate)dp2.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
458                                 if (equivalent(((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr,
459                                                (RelationExpr)((OpExpr)((ExprPredicate)dp2.getPredicate()).expr).left))
460                                     continue loop; // comparison predicate ensure that size expr is true - no need to generate abstract repairs...
461                             }
462                         }
463                     }
464                 }
465
466                 for(int j=0;j<array.length;j++) {
467                     AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
468                     TermNode tn2=new TermNode(ar);
469                     //              GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
470                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),dp.name()+" "+ar.type(),tn2);
471                     gn2.setOption(absrepoption);
472                     GraphNode.Edge e=new GraphNode.Edge("abstractedge1",gn2);
473                     gn.addEdge(e);
474                     if (!predtoabstractmap.containsKey(dp))
475                         predtoabstractmap.put(dp,new HashSet());
476                     ((Set)predtoabstractmap.get(dp)).add(gn2);
477                     abstractrepair.add(gn2);
478                 }
479             }
480         }
481         /* Generate additional abstract repairs */
482         Vector setdescriptors=state.stSets.getAllDescriptors();
483         for(int i=0;i<setdescriptors.size();i++) {
484             SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
485
486             VarExpr ve=new VarExpr("DUMMY");
487             InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
488             DNFPredicate tp=new DNFPredicate(false,ip);
489             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd,sources);
490             TermNode tn=new TermNode(ar);
491             GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
492             gn.setOption(absrepoption);
493             if (!predtoabstractmap.containsKey(tp))
494                 predtoabstractmap.put(tp,new HashSet());
495             ((Set)predtoabstractmap.get(tp)).add(gn);
496             abstractrepair.add(gn);
497             abstractrepairadd.add(gn);
498             abstractadd.put(sd,gn);
499
500             DNFPredicate tp2=new DNFPredicate(true,ip);
501             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd,sources);
502             TermNode tn2=new TermNode(ar2);
503             GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
504             gn2.setOption(absrepoption);
505             if (!predtoabstractmap.containsKey(tp2))
506                 predtoabstractmap.put(tp2,new HashSet());
507             ((Set)predtoabstractmap.get(tp2)).add(gn2);
508             abstractrepair.add(gn2);
509             abstractrepairadd.add(gn2);
510             abstractremove.put(sd,gn2);
511         }
512
513         Vector relationdescriptors=state.stRelations.getAllDescriptors();
514         for(int i=0;i<relationdescriptors.size();i++) {
515             RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
516             VarDescriptor vd1=new VarDescriptor("DUMMY1");
517             VarExpr ve2=new VarExpr("DUMMY2");
518
519             InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
520
521             DNFPredicate tp=new DNFPredicate(false,ip);
522             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd,sources);
523             TermNode tn=new TermNode(ar);
524             GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
525             gn.setOption(absrepoption);
526             if (!predtoabstractmap.containsKey(tp))
527                 predtoabstractmap.put(tp,new HashSet());
528             ((Set)predtoabstractmap.get(tp)).add(gn);
529             abstractrepair.add(gn);
530             abstractrepairadd.add(gn);
531             abstractadd.put(rd,gn);
532
533             DNFPredicate tp2=new DNFPredicate(true,ip);
534             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd,sources);
535             TermNode tn2=new TermNode(ar2);
536             GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
537             gn2.setOption(absrepoption);
538             if (!predtoabstractmap.containsKey(tp2))
539                 predtoabstractmap.put(tp2,new HashSet());
540             ((Set)predtoabstractmap.get(tp2)).add(gn2);
541             abstractrepair.add(gn2);
542             abstractrepairadd.add(gn2);
543             abstractremove.put(rd,gn2);
544         }
545     }
546
547     int compensationcount=0;
548     void generatecompensationnodes() {
549         for(int i=0;i<state.vRules.size();i++) {
550             Rule r=(Rule) state.vRules.get(i);
551             Vector possiblerules=new Vector();
552
553             for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
554                 GraphNode gn=(GraphNode)scopesatisfy.get(r);
555                 TermNode tn=(TermNode) gn.getOwner();
556                 ScopeNode sn=tn.getScope();
557                 MultUpdateNode mun=new MultUpdateNode(sn);
558                 TermNode tn2=new TermNode(mun);
559                 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
560                 gn2.setOption(compoption);
561                 UpdateNode un=new UpdateNode(r);
562
563                 if (j<r.numQuantifiers()) {
564                     /* Remove quantifier */
565                     Quantifier q=r.getQuantifier(j);
566                     if (q instanceof RelationQuantifier) {
567                         RelationQuantifier rq=(RelationQuantifier)q;
568                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
569                         toe.td=ReservedTypeDescriptor.INT;
570                         Updates u=new Updates(toe,true);
571                         un.addUpdate(u);
572                         if (abstractremove.containsKey(rq.relation)) {
573                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
574                             GraphNode.Edge e=new GraphNode.Edge("requiresremove1",agn);
575                             gn2.addEdge(e);
576                         } else {
577                             continue; /* Abstract repair doesn't exist */
578                         }
579                     } else if (q instanceof SetQuantifier) {
580                         SetQuantifier sq=(SetQuantifier)q;
581                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
582                         eoe.td=ReservedTypeDescriptor.INT;
583                         Updates u=new Updates(eoe,true);
584                         un.addUpdate(u);
585                         if (abstractremove.containsKey(sq.set)) {
586                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
587                             GraphNode.Edge e=new GraphNode.Edge("requiresremove2",agn);
588                             gn2.addEdge(e);
589                         } else {
590                             continue; /* Abstract repair doesn't exist */
591                         }
592                     } else {
593                         continue;
594                     }
595                 } else {
596                     /* Negate conjunction */
597                     int c=j-r.numQuantifiers();
598                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c),null)) {
599                         continue;
600                     }
601                 }
602                 if (!un.checkupdates()) /* Make sure we have a good update */
603                     continue;
604
605                 mun.addUpdate(un);
606                 GraphNode.Edge e=new GraphNode.Edge("abstractcomp"+compensationcount,gn2);
607                 compensationcount++;
608                 gn.addEdge(e);
609                 updatenodes.add(gn2);
610             }
611         }
612     }
613
614     void generatedatastructureupdatenodes() {
615         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
616             GraphNode gn=(GraphNode)absiterator.next();
617             System.out.println("Analysing: "+gn.getTextLabel());
618             TermNode tn=(TermNode) gn.getOwner();
619             AbstractRepair ar=tn.getAbstract();
620             if (ar.getType()==AbstractRepair.ADDTOSET) {
621                 generateaddtosetrelation(gn,ar);
622             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
623                 generateremovefromsetrelation(gn,ar);
624             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
625                 generateaddtosetrelation(gn,ar);
626             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
627                 generateremovefromsetrelation(gn,ar);
628             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
629                 /* Generate remove/add pairs */
630                 if (ar.needsRemoves(state))
631                     generateremovefromsetrelation(gn,ar);
632                 generateaddtosetrelation(gn,ar);
633                 /* Generate atomic modify */
634                 generatemodifyrelation(gn,ar);
635             }
636         }
637     }
638
639
640     /** This method generates concrete data structure updates which
641      * remove an object (or tuple) from a set (or relation).*/
642
643     int removefromcount=0;
644     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
645         /* Construct the set of all rules which could add something to the given set or relation */
646
647         Vector possiblerules=new Vector();
648         for(int i=0;i<state.vRules.size();i++) {
649             Rule r=(Rule) state.vRules.get(i);
650             if ((r.getInclusion() instanceof SetInclusion)&&
651                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
652                 possiblerules.add(r);
653             if ((r.getInclusion() instanceof RelationInclusion)&&
654                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
655                 possiblerules.add(r);
656         }
657         if (possiblerules.size()==0)
658             return;
659
660         /* Loop through different ways of falsifying each of these rules */
661         int[] count=new int[possiblerules.size()];
662         while(remains(count,possiblerules,true)) {
663             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
664             TermNode tn=new TermNode(mun);
665             GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
666             gn2.setOption(updateoption);
667
668             boolean goodflag=true;
669             for(int i=0;i<possiblerules.size();i++) {
670                 Rule r=(Rule)possiblerules.get(i);
671                 UpdateNode un=new UpdateNode(r);
672
673                 if (count[i]<r.numQuantifiers()) {
674                     /* Remove quantifier */
675                     Quantifier q=r.getQuantifier(count[i]);
676                     if (q instanceof RelationQuantifier) {
677                         RelationQuantifier rq=(RelationQuantifier)q;
678                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
679                         toe.td=ReservedTypeDescriptor.INT;
680                         Updates u=new Updates(toe,true);
681                         un.addUpdate(u);
682                         if (abstractremove.containsKey(rq.relation)) {
683                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
684                             GraphNode.Edge e=new GraphNode.Edge("requiresremove3",agn);
685                             gn2.addEdge(e);
686                         } else {
687                             goodflag=false;break; /* Abstract repair doesn't exist */
688                         }
689                     } else if (q instanceof SetQuantifier) {
690                         SetQuantifier sq=(SetQuantifier)q;
691                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
692                         eoe.td=ReservedTypeDescriptor.INT;
693                         Updates u=new Updates(eoe,true);
694                         un.addUpdate(u);
695                         if (abstractremove.containsKey(sq.set)) {
696                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
697                             GraphNode.Edge e=new GraphNode.Edge("requiresremove4",agn);
698                             gn2.addEdge(e);
699                         } else {
700                             goodflag=false;break; /* Abstract repair doesn't exist */
701                         }
702                     } else {goodflag=false;break;}
703                 } else {
704                     int c=count[i]-r.numQuantifiers();
705                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c),null)) {
706                         goodflag=false;break;
707                     }
708                 }
709                 if (!un.checkupdates()) {
710                     goodflag=false;
711                     break;
712                 }
713                 mun.addUpdate(un);
714             }
715             if (goodflag) {
716                 GraphNode.Edge e=new GraphNode.Edge("abstract3"+(removefromcount++),gn2);
717                 gn.addEdge(e);
718                 updatenodes.add(gn2);
719             }
720             increment(count,possiblerules,true);
721         }
722     }
723
724     /** This method increments to the next possibility. */
725
726     static private void increment(int count[], Vector rules,boolean isremove) {
727         count[0]++;
728         for(int i=0;i<(rules.size()-1);i++) {
729             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
730             if (count[i]>=num) {
731                 count[i+1]++;
732                 count[i]=0;
733             } else break;
734         }
735     }
736
737
738     /** This method test if there remain any possibilities to loop
739      * through. */
740     static private boolean remains(int count[], Vector rules, boolean isremove) {
741         for(int i=0;i<rules.size();i++) {
742             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
743             if (count[i]>=num) {
744                 return false;
745             }
746         }
747         return true;
748     }
749
750     /** This method generates data structure updates to implement the
751      *  abstract atomic modification specified by ar. */
752
753     int modifycount=0;
754     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
755         RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
756         ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
757         boolean inverted=exprPredicate.inverted();
758         int leftindex=0;
759         int rightindex=1;
760         if (inverted)
761             leftindex=2;
762         else
763             rightindex=2;
764
765         // construct set of possible rules
766         Vector possiblerules=new Vector();
767         for(int i=0;i<state.vRules.size();i++) {
768             Rule r=(Rule) state.vRules.get(i);
769             if ((r.getInclusion() instanceof RelationInclusion)&&
770                 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
771                 possiblerules.add(r);
772         }
773         if (possiblerules.size()==0)
774             return;
775
776         // increment through this set
777         int[] count=new int[possiblerules.size()];
778         while(remains(count,possiblerules,false)) {
779             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
780             TermNode tn=new TermNode(mun);
781             GraphNode gn2=new GraphNode("UpdateMod"+modifycount,tn);
782             gn2.setOption(updateoption);
783
784             boolean goodflag=true;
785             for(int i=0;i<possiblerules.size();i++) {
786                 Rule r=(Rule)possiblerules.get(i);
787                 UpdateNode un=new UpdateNode(r);
788
789                 int c=count[i];
790                 if (!processconjunction(un,r.getDNFGuardExpr().get(c),null)) {
791                     goodflag=false;break;
792                 }
793                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
794                 if (!(ri.getLeftExpr() instanceof VarExpr)) {
795                     if (ri.getLeftExpr().isValue(ri.getRelation().getDomain().getType())) {
796                         Updates up=new Updates(ri.getLeftExpr(),leftindex,ri.getRelation().getDomain().getType());
797                         un.addUpdate(up);
798                     } else {
799                         if (inverted)
800                             goodflag=false;
801                         else un.addInvariant(ri.getLeftExpr());
802                     }
803                 } else {
804                     VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
805                     if (vd.isGlobal()) {
806                         Updates up=new Updates(ri.getLeftExpr(),leftindex,null);
807                         un.addUpdate(up);
808                     } else if (inverted)
809                         goodflag=false;
810                 }
811                 if (!(ri.getRightExpr() instanceof VarExpr)) {
812                     if (ri.getRightExpr().isValue(ri.getRelation().getRange().getType())) {
813                         Updates up=new Updates(ri.getRightExpr(),rightindex,ri.getRelation().getRange().getType());
814                         un.addUpdate(up);
815                     } else {
816                         if (!inverted)
817                             goodflag=false;
818                         else
819                             un.addInvariant(ri.getLeftExpr());
820                     }
821                 } else {
822                     VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
823                     if (vd.isGlobal()) {
824                         Updates up=new Updates(ri.getRightExpr(),rightindex,null);
825                         un.addUpdate(up);
826                     } else if (!inverted)
827                         goodflag=false;
828                 }
829
830                 if (!un.checkupdates()) {
831                     goodflag=false;
832                     break;
833                 }
834                 mun.addUpdate(un);
835             }
836             if (goodflag) {
837                 GraphNode.Edge e=new GraphNode.Edge("abstract4"+modifycount,gn2);
838                 modifycount++;
839                 gn.addEdge(e);
840                 updatenodes.add(gn2);
841             }
842             increment(count,possiblerules,false);
843         }
844     }
845
846     /** Generate concrete data structure update to add an object(or
847      * tuple) to a set (or relation). */
848
849     static int addtocount=0;
850     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
851         for(int i=0;i<state.vRules.size();i++) {
852             Rule r=(Rule) state.vRules.get(i);
853
854
855             /* See if this is a good rule*/
856             if ((r.getInclusion() instanceof SetInclusion&&
857                  ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
858                 (r.getInclusion() instanceof RelationInclusion&&
859                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
860
861                 /* First solve for quantifiers */
862                 Vector bindings=new Vector();
863                 /* Construct bindings */
864
865                 Hashtable setmapping=new Hashtable();
866                 System.out.println("Attempting to construct bindings");
867
868                 if (!constructbindings(bindings,r,ar,setmapping,false))
869                     continue;
870                 System.out.println("Bindings constructed");
871                 //Generate add instruction
872                 DNFRule dnfrule=r.getDNFGuardExpr();
873                  endloop:
874                 for(int j=0;j<dnfrule.size();j++) {
875                     Inclusion inc=r.getInclusion();
876                     UpdateNode un=new UpdateNode(r);
877                     un.addBindings(bindings);
878                     /* Now build update for tuple/set inclusion condition */
879                     if(inc instanceof SetInclusion) {
880                         SetInclusion si=(SetInclusion)inc;
881                         Expr e=si.elementexpr;
882
883                         while(e instanceof CastExpr) {
884                             CastExpr ce=(CastExpr)e;
885                             if (ce.getType()!=si.getSet().getType())
886                                 continue endloop;
887                             e=ce.getExpr();
888                         }
889
890                         if (!(e instanceof VarExpr)) {
891                             if (e.isValue(si.getSet().getType())) {
892                                 Updates up=new Updates(e,0,si.getSet().getType());
893                                 un.addUpdate(up);
894                             } else {
895                                 /* We're an add to set*/
896                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
897                                 SetDescriptor set=sources.setSource(si.getSet())?
898                                     sources.getSourceSet(si.getSet()):null;
899                                 if (set==null)
900                                     continue;
901                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
902                                 if (rap==ArrayAnalysis.AccessPath.NONE)
903                                     continue;
904                                 if (!rap.equal(ap))
905                                     continue;
906                                 if (!constructarrayupdate(un, e, rap, 0))
907                                     continue;
908                             }
909                         } else {
910                             VarDescriptor vd=((VarExpr)e).getVar();
911                             if (vd.isGlobal()) {
912                                 Updates up=new Updates(e,0,null);
913                                 un.addUpdate(up);
914                             }
915                         }
916                     } else if (inc instanceof RelationInclusion) {
917                         RelationInclusion ri=(RelationInclusion)inc;
918
919                         Expr e=ri.getLeftExpr();
920
921                         while(e instanceof CastExpr) {
922                             CastExpr ce=(CastExpr)e;
923                             if (ce.getType()!=ri.getRelation().getDomain().getType())
924                                 continue endloop;
925                             e=ce.getExpr();
926                         }
927                         if (!(e instanceof VarExpr)) {
928                             if (e.isValue(ri.getRelation().getDomain().getType())) {
929                                 Updates up=new Updates(e,0,ri.getRelation().getDomain().getType());
930                                 if (ar.getDomainSet()!=null)
931                                     setmapping.put(e,ar.getDomainSet());
932                                 un.addUpdate(up);
933                             } else {
934                                 /* We don't handly relation modifies */
935                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
936                                     continue;
937                                 /* We're an add to relation*/
938                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
939                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),true /* Domain*/)?
940                                     sources.relgetSourceSet(ri.getRelation(),true):null;
941                                 if (set==null)
942                                     continue;
943                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
944                                 if (rap==ArrayAnalysis.AccessPath.NONE||
945                                     !rap.equal(ap)||
946                                     !constructarrayupdate(un, e, rap, 0))
947                                     continue;
948                                 if (ar.getDomainSet()!=null)
949                                     setmapping.put(e,ar.getDomainSet());
950
951                             }
952                         } else {
953                             VarDescriptor vd=((VarExpr)e).getVar();
954                             if (vd.isGlobal()) {
955                                 Updates up=new Updates(e,0,null);
956                                 if (ar.getDomainSet()!=null)
957                                     setmapping.put(e,ar.getDomainSet());
958                                 un.addUpdate(up);
959                             }
960                         }
961
962                         e=ri.getRightExpr();
963
964                         while(e instanceof CastExpr) {
965                             CastExpr ce=(CastExpr)e;
966                             if (ce.getType()!=ri.getRelation().getRange().getType())
967                                 continue endloop;
968                             e=ce.getExpr();
969                         }
970                         if (!(e instanceof VarExpr)) {
971                             if (e.isValue(ri.getRelation().getRange().getType())) {
972                                 Updates up=new Updates(e,1,ri.getRelation().getRange().getType());
973                                 un.addUpdate(up);
974                             } else {
975                                 /* We don't handly relation modifies */
976                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
977                                     continue;
978                                 /* We're an add to relation*/
979                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
980                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),false /* Range*/)?
981                                     sources.relgetSourceSet(ri.getRelation(),false):null;
982                                 if (set==null)
983                                     continue;
984                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
985
986                                 if (rap==ArrayAnalysis.AccessPath.NONE||
987                                     !rap.equal(ap)||
988                                     !constructarrayupdate(un, e, rap, 1))
989                                     continue;
990                                 if (ar.getRangeSet()!=null)
991                                     setmapping.put(e,ar.getRangeSet());
992                             }
993                         } else {
994                             VarDescriptor vd=((VarExpr)e).getVar();
995                             if (vd.isGlobal()) {
996                                 Updates up=new Updates(e,1,null);
997                                 if (ar.getRangeSet()!=null)
998                                     setmapping.put(e,ar.getRangeSet());
999                                 un.addUpdate(up);
1000                             }
1001                         }
1002                     }
1003                     System.out.println("Built inclusion condition updates.");
1004                     //Finally build necessary updates to satisfy conjunction
1005                     RuleConjunction ruleconj=dnfrule.get(j);
1006
1007                     /* Add in updates for quantifiers */
1008                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
1009                     TermNode tn=new TermNode(mun);
1010                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
1011                     gn2.setOption(updateoption);
1012
1013                     if (debugmsg("Start processing quantifiers")&&
1014                         processquantifiers(gn2,un, r,setmapping)&&
1015                         debugmsg("Finished processing quantifiers")&&
1016                         processconjunction(un,ruleconj,setmapping)&&
1017                         debugmsg("Finished processing conjunction")&&
1018                         un.checkupdates()&&
1019                         debugmsg("Updates checked")) {
1020                         mun.addUpdate(un);
1021                         GraphNode.Edge e=new GraphNode.Edge("abstract5"+addtocount,gn2);
1022                         addtocount++;
1023                         gn.addEdge(e);
1024                         updatenodes.add(gn2);
1025                     }
1026                 }
1027             }
1028         }
1029     }
1030
1031     boolean debugmsg(String st) {
1032         System.out.println(st);
1033         return true;
1034     }
1035
1036     boolean constructarrayupdate(UpdateNode un, Expr lexpr, ArrayAnalysis.AccessPath ap, int slotnumber) {
1037         System.out.println("Constructing array update");
1038         Expr e=null;
1039         for (int i=ap.numFields()-1;i>=0;i--) {
1040             if (e==null)
1041                 e=lexpr;
1042             else
1043                 e=((DotExpr)e).getExpr();
1044
1045             while (e instanceof CastExpr)
1046                 e=((CastExpr)e).getExpr();
1047
1048             DotExpr de=(DotExpr)e;
1049             FieldDescriptor fd=ap.getField(i);
1050             if (fd instanceof ArrayDescriptor) {
1051                 // We have an ArrayDescriptor!
1052                 Expr index=de.getIndex();
1053                 if (!index.isValue(null)) {/* Not assignable */
1054                     System.out.println("ERROR:Index isn't assignable");
1055                     return false;
1056                 }
1057                 Updates updates=new Updates(index,i,ap,lexpr,slotnumber);
1058                 un.addUpdate(updates);
1059             }
1060         }
1061         return true;
1062     }
1063
1064     /** This method constructs bindings for an update using rule
1065      * r. The boolean flag isremoval indicates that the update
1066      * performs a removal.  The function returns true if it is able to
1067      * generate a valid set of bindings and false otherwise. */
1068
1069     boolean constructbindings(Vector bindings, Rule r, AbstractRepair ar, Hashtable setmapping, boolean isremoval) {
1070         boolean goodupdate=true;
1071         Inclusion inc=r.getInclusion();
1072
1073         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1074             Quantifier q=(Quantifier)iterator.next();
1075             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
1076                 VarDescriptor vd=null;
1077                 SetDescriptor set=null;
1078                 if (q instanceof SetQuantifier) {
1079                     vd=((SetQuantifier)q).getVar();
1080                     set=((SetQuantifier)q).getSet();
1081                 } else {
1082                     vd=((ForQuantifier)q).getVar();
1083                 }
1084                 if(inc instanceof SetInclusion) {
1085                     SetInclusion si=(SetInclusion)inc;
1086                     Expr tmpe=si.elementexpr;
1087                     Expr e=si.elementexpr;
1088
1089                     while(e instanceof CastExpr) {
1090                         CastExpr ce=(CastExpr)e;
1091                         if (ce.getType()!=si.getSet().getType())
1092                             return false;
1093                         e=ce.getExpr();
1094                     }
1095
1096                     if ((e instanceof VarExpr)&&
1097                         (((VarExpr)e).getVar()==vd)) {
1098                         /* Can solve for v */
1099                         if (set==null||!si.getSet().getType().isSubtypeOf(set.getType()))
1100                             return false;
1101                         Binding binding=new Binding(vd,0);
1102                         bindings.add(binding);
1103                     } else {
1104                         goodupdate=false;
1105                     }
1106                 } else if (inc instanceof RelationInclusion) {
1107                     RelationInclusion ri=(RelationInclusion)inc;
1108                     boolean f1=true;
1109                     boolean f2=true;
1110
1111                     Expr e=ri.getLeftExpr();
1112
1113                     while(e instanceof CastExpr) {
1114                         CastExpr ce=(CastExpr)e;
1115                         if (ce.getType()!=ri.getRelation().getDomain().getType())
1116                             return false;
1117                         e=ce.getExpr();
1118                     }
1119
1120                     if ((e instanceof VarExpr)&&
1121                         (((VarExpr)e).getVar()==vd)) {
1122                                 /* Can solve for v */
1123                         Binding binding=new Binding(vd,0);
1124                         if (!ri.getRelation().getDomain().getType().isSubtypeOf(set.getType()))
1125                             return false;
1126                         if (ar.getDomainSet()!=null)
1127                             setmapping.put(ri.getLeftExpr(),ar.getDomainSet());
1128                         bindings.add(binding);
1129                     } else f1=false;
1130
1131
1132                     e=ri.getRightExpr();
1133
1134                     while(e instanceof CastExpr) {
1135                         CastExpr ce=(CastExpr)e;
1136                         if (ce.getType()!=ri.getRelation().getRange().getType())
1137                             return false;
1138                         e=ce.getExpr();
1139                     }
1140
1141                     if ((e instanceof VarExpr)&&
1142                         (((VarExpr)e).getVar()==vd)) {
1143                                 /* Can solve for v */
1144                         Binding binding=new Binding(vd,1);
1145                         if (!ri.getRelation().getRange().getType().isSubtypeOf(set.getType()))
1146                             return false;
1147                         if (ar.getRangeSet()!=null)
1148                             setmapping.put(ri.getRightExpr(),ar.getRangeSet());
1149                         bindings.add(binding);
1150                     } else f2=false;
1151                     if (!(f1||f2))
1152                         goodupdate=false;
1153                 } else throw new Error("Inclusion not recognized");
1154                 if (!goodupdate)
1155                     if (isremoval) {
1156                         /* Removals don't need bindings anymore
1157                            Binding binding=new Binding(vd);
1158                            bindings.add(binding);*/
1159                         goodupdate=true;
1160                     } else if (q instanceof SetQuantifier) {
1161                         /* Create new element to bind to */
1162                         // search if the set 'set' has a size
1163                         Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
1164                         bindings.add(binding);
1165                         goodupdate=true;
1166
1167                     } else
1168                         goodupdate=false;
1169             } else if (q instanceof RelationQuantifier) {
1170                 RelationQuantifier rq=(RelationQuantifier)q;
1171                 for(int k=0;k<2;k++) {
1172                     VarDescriptor vd=(k==0)?rq.x:rq.y;
1173                     TypeDescriptor td=(k==0)?rq.getRelation().getDomain().getType():rq.getRelation().getRange().getType();
1174                     if(inc instanceof SetInclusion) {
1175                         SetInclusion si=(SetInclusion)inc;
1176
1177                         Expr e=si.elementexpr;
1178
1179                         while(e instanceof CastExpr) {
1180                             CastExpr ce=(CastExpr)e;
1181                             if (ce.getType()!=td)
1182                                 return false;
1183                             e=ce.getExpr();
1184                         }
1185
1186                         if ((e instanceof VarExpr)&&
1187                             (((VarExpr)e).getVar()==vd)) {
1188                             /* Can solve for v */
1189                             Binding binding=new Binding(vd,0);
1190
1191                             if (!si.getSet().getType().isSubtypeOf(td))
1192                                 return false;
1193                             bindings.add(binding);
1194                         } else
1195                             goodupdate=false;
1196                     } else if (inc instanceof RelationInclusion) {
1197                         RelationInclusion ri=(RelationInclusion)inc;
1198                         boolean f1=true;
1199                         boolean f2=true;
1200
1201
1202                         Expr e=ri.getLeftExpr();
1203
1204                         while(e instanceof CastExpr) {
1205                             CastExpr ce=(CastExpr)e;
1206                             if (ce.getType()!=ri.getRelation().getDomain().getType())
1207                                 return false;
1208                             e=ce.getExpr();
1209                         }
1210                         if ((ri.getLeftExpr() instanceof VarExpr)&&
1211                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
1212                             /* Can solve for v */
1213                             Binding binding=new Binding(vd,0);
1214                             if (!ri.getRelation().getDomain().getType().isSubtypeOf(td))
1215                                 return false;
1216                             if (ar.getDomainSet()!=null)
1217                                 setmapping.put(ri.getLeftExpr(),ar.getDomainSet());
1218                             bindings.add(binding);
1219                         } else f1=false;
1220
1221
1222                         e=ri.getRightExpr();
1223
1224                         while(e instanceof CastExpr) {
1225                             CastExpr ce=(CastExpr)e;
1226                             if (ce.getType()!=ri.getRelation().getRange().getType())
1227                                 return false;
1228                             e=ce.getExpr();
1229                         }
1230                         if ((ri.getRightExpr() instanceof VarExpr)&&
1231                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
1232                             /* Can solve for v */
1233                             Binding binding=new Binding(vd,1);
1234                             if (!ri.getRelation().getRange().getType().isSubtypeOf(td))
1235                                 return false;
1236                             if (ar.getRangeSet()!=null)
1237                                 setmapping.put(ri.getRightExpr(),ar.getRangeSet());
1238                             bindings.add(binding);
1239                         } else f2=false;
1240                         if (!(f1||f2))
1241                             goodupdate=false;
1242                     } else throw new Error("Inclusion not recognized");
1243                     if (!goodupdate)
1244                         if (isremoval) {
1245                             /* Removals don't need bindings anymore
1246                                Binding binding=new Binding(vd);
1247                                bindings.add(binding);*/
1248                             goodupdate=true;
1249                         } else
1250                             break;
1251                 }
1252                 if (!goodupdate)
1253                     break;
1254             } else throw new Error("Quantifier not recognized");
1255         }
1256         return goodupdate;
1257     }
1258
1259     /** Adds updates that add an item to the appropriate set or
1260      * relation quantified over by the model definition rule.. */
1261
1262     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r,Hashtable setmapping) {
1263         Inclusion inc=r.getInclusion();
1264         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1265             Quantifier q=(Quantifier)iterator.next();
1266             /* Add quantifier */
1267             if (q instanceof RelationQuantifier) {
1268                 RelationQuantifier rq=(RelationQuantifier)q;
1269                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
1270                 toe.td=ReservedTypeDescriptor.INT;
1271                 Updates u=new Updates(toe,false);
1272                 un.addUpdate(u);
1273                 if (abstractadd.containsKey(rq.relation)) {
1274                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
1275                     GraphNode.Edge e=new GraphNode.Edge("requiresadd5",agn);
1276                     gn.addEdge(e);
1277                 } else {
1278                     return false;
1279                 }
1280             } else if (q instanceof SetQuantifier) {
1281                 SetQuantifier sq=(SetQuantifier)q;
1282                 if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
1283                     Binding b=un.getBinding(sq.var);
1284                     Constraint reqc=exactsize.getConstraint(b.getSet());
1285                     constraintdependence.requiresConstraint(gn,reqc);
1286                     continue; /* Don't need to ensure addition for search */
1287                 }
1288                 VarExpr ve=new VarExpr(sq.var);
1289                 SetDescriptor sd=findExpr(setmapping, ve);
1290                 if (sd!=null&&sd.isSubset(sq.set))
1291                     continue; /* this update is trivially true */
1292
1293                 ElementOfExpr eoe=new ElementOfExpr(ve,sq.set);
1294                 eoe.td=ReservedTypeDescriptor.INT;
1295                 Updates u=new Updates(eoe,false);
1296                 un.addUpdate(u);
1297                 if (abstractadd.containsKey(sq.set)) {
1298                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
1299                     GraphNode.Edge e=new GraphNode.Edge("requiresadd6",agn);
1300                     gn.addEdge(e);
1301                 } else {
1302                     return false;
1303                 }
1304             } else return false;
1305         }
1306         return true;
1307     }
1308
1309     static SetDescriptor findExpr(Hashtable setmapping, Expr e) {
1310         if (setmapping==null)
1311             return null;
1312         Set kset=setmapping.keySet();
1313         for(Iterator it=kset.iterator();it.hasNext();) {
1314             Expr expr=(Expr)it.next();
1315             if (expr.equals(null,e)) {
1316                 return (SetDescriptor)setmapping.get(expr);
1317             }
1318         }
1319         return null;
1320     }
1321
1322     /** This method generates the necessary updates to satisfy the
1323      * conjunction ruleconj. */
1324
1325     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj,Hashtable setmapping) {
1326         boolean okay=true;
1327         for(int k=0;k<ruleconj.size();k++) {
1328             DNFExpr de=ruleconj.get(k);
1329             Expr e=de.getExpr();
1330             if (e instanceof OpExpr) {
1331                 OpExpr ex=(OpExpr)de.getExpr();
1332                 Opcode op=ex.getOpcode();
1333                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
1334                 un.addUpdate(up);
1335             } else if (e instanceof ElementOfExpr) {
1336                 SetDescriptor sd=findExpr(setmapping, ((ElementOfExpr)e).element);
1337                 if (sd!=null&&sd.isSubset(((ElementOfExpr)e).set))
1338                     continue; /* this update is trivially true */
1339                 Updates up=new Updates(e,de.getNegation());
1340                 un.addUpdate(up);
1341             } else if (e instanceof TupleOfExpr) {
1342                 Updates up=new Updates(e,de.getNegation());
1343                 un.addUpdate(up);
1344             } else if (e instanceof BooleanLiteralExpr) {
1345                 boolean truth=((BooleanLiteralExpr)e).getValue();
1346                 if (de.getNegation())
1347                     truth=!truth;
1348                 if (!truth) {
1349                     okay=false;
1350                     break;
1351                 }
1352             } else {
1353                 System.out.println(e.getClass().getName());
1354                 throw new Error("Unrecognized Expr");
1355             }
1356         }
1357         return okay;
1358     }
1359
1360     /** This method sees if when the quantifiers listed in set are
1361      *  fixed, whether there can be more than one unique binding for
1362      *  the constraint or model definition rule qs.*/
1363     public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
1364         for(int i=0;i<qs.numQuantifiers();i++) {
1365             Quantifier q=qs.getQuantifier(i);
1366             if (set.contains(q))
1367                 continue;
1368             if (q instanceof SetQuantifier) {
1369                 SetDescriptor sd=((SetQuantifier)q).getSet();
1370                 if (maxsize.getsize(sd)<=1&&
1371                     maxsize.getsize(sd)>=0)
1372                     continue;
1373             } else if (q instanceof RelationQuantifier) {
1374                 RelationDescriptor rd=((RelationQuantifier)q).getRelation();
1375                 if (maxsize.getsize(rd)<=1&&
1376                     maxsize.getsize(rd)>=0)
1377                     continue;
1378             }
1379             return false;
1380         }
1381         return true;
1382     }
1383
1384     public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1385         if (mutualexclusive(sd1,sd2)||
1386             mutualexclusive(sd2,sd1))
1387             return true;
1388         else
1389             return false;
1390     }
1391
1392     private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1393         Vector rules=state.vRules;
1394         for(int i=0;i<rules.size();i++) {
1395             Rule r=(Rule)rules.get(i);
1396             if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
1397                 /* Rule may add items to sd1 */
1398                 SetInclusion si=(SetInclusion)r.getInclusion();
1399                 Expr ve=si.getExpr();
1400                 DNFRule drule=r.getDNFGuardExpr();
1401                 for(int j=0;j<drule.size();j++) {
1402                     RuleConjunction rconj=drule.get(j);
1403                     boolean containsexclusion=false;
1404                     for (int k=0;k<rconj.size();k++) {
1405                         DNFExpr dexpr=rconj.get(k);
1406                         if (dexpr.getNegation()&&
1407                             dexpr.getExpr() instanceof ElementOfExpr&&
1408                             ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
1409                             SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
1410                             if (sd.isSubset(sd2))
1411                                 containsexclusion=true;
1412                         }
1413                     }
1414                     if (!containsexclusion)
1415                         return false;
1416                 }
1417             }
1418         }
1419         return true;
1420     }
1421
1422     boolean equivalent(SetExpr se, RelationExpr re) {
1423         if (!(se instanceof ImageSetExpr))
1424             return false;
1425         ImageSetExpr ise=(ImageSetExpr)se;
1426         while(re!=null&&ise!=null) {
1427             if (re.getRelation()!=ise.getRelation())
1428                 return false;
1429             if (re.inverted()!=ise.inverted())
1430                 return false;
1431             if (ise.isimageset) {
1432                 ise=ise.getImageSetExpr();
1433                 if (!(re.getExpr() instanceof RelationExpr))
1434                     return false;
1435                 re=(RelationExpr)re.getExpr();
1436             } else {
1437                 if (!(re.getExpr() instanceof VarExpr))
1438                     return false;
1439                 if (((VarExpr)re.getExpr()).getVar()==ise.getVar())
1440                     return true; //everything matches
1441                 return false;
1442             }
1443         }
1444         return false;
1445     }
1446 }