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