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);
 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);
 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);
 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);
 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);
 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))) {
 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))) {
 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))) {
 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             /* See if this is a good rule*/
 765             if ((r.getInclusion() instanceof SetInclusion&&
 766                  ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 767                 (r.getInclusion() instanceof RelationInclusion&&
 768                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 769
 770                 /* First solve for quantifiers */
 771                 Vector bindings=new Vector();
 772                 /* Construct bindings */
 773                 if (!constructbindings(bindings,r,false))
 774                     continue;
 775                 //Generate add instruction
 776                 DNFRule dnfrule=r.getDNFGuardExpr();
 777                 for(int j=0;j<dnfrule.size();j++) {
 778                     Inclusion inc=r.getInclusion();
 779                     UpdateNode un=new UpdateNode(r);
 780                     un.addBindings(bindings);
 781                     /* Now build update for tuple/set inclusion condition */
 782                     if(inc instanceof SetInclusion) {
 783                         SetInclusion si=(SetInclusion)inc;
 784                         if (!(si.elementexpr instanceof VarExpr)) {
 785                             if (si.elementexpr.isValue(si.getSet().getType())) {
 786                                 Updates up=new Updates(si.elementexpr,0,si.getSet().getType());
 787                                 un.addUpdate(up);
 788                             } else {
 789                                 /* We're an add to set*/
 790                                 System.out.println("Rule: "+r);
 791                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,si.elementexpr);
 792                                 System.out.println("Attempting perform array add");
 793                                 SetDescriptor set=sources.setSource(si.getSet())?
 794                                     sources.getSourceSet(si.getSet()):null;
 795                                 if (set==null)
 796                                     continue;
 797                                 System.out.println("Non-null source set");
 798                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 799                                 if (rap==ArrayAnalysis.AccessPath.NONE)
 800                                     continue;
 801                                 System.out.println("A");
 802                                 if (!rap.equal(ap))
 803                                     continue;
 804                                 System.out.println("B");
 805                                 if (!constructarrayupdate(un, si.elementexpr, rap, 0))
 806                                     continue;
 807                                 System.out.println("C");
 808                             }
 809                         } else {
 810                             VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 811                             if (vd.isGlobal()) {
 812                                 Updates up=new Updates(si.elementexpr,0,null);
 813                                 un.addUpdate(up);
 814                             }
 815                         }
 816                     } else if (inc instanceof RelationInclusion) {
 817                         RelationInclusion ri=(RelationInclusion)inc;
 818                         if (!(ri.getLeftExpr() instanceof VarExpr)) {
 819                             if (ri.getLeftExpr().isValue(ri.getRelation().getDomain().getType())) {
 820                                 Updates up=new Updates(ri.getLeftExpr(),0,ri.getRelation().getDomain().getType());
 821                                 un.addUpdate(up);
 822                             } else {
 823                                 /* We don't handly relation modifies */
 824                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
 825                                     continue;
 826                                 /* We're an add to relation*/
 827                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getLeftExpr());
 828                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),true /* Domain*/)?
 829                                     sources.relgetSourceSet(ri.getRelation(),true):null;
 830                                 if (set==null)
 831                                     continue;
 832                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 833
 834                                 if (rap==ArrayAnalysis.AccessPath.NONE||
 835                                     !rap.equal(ap)||
 836                                     !constructarrayupdate(un, ri.getLeftExpr(), rap, 0))
 837                                     continue;
 838                             }
 839                         } else {
 840                             VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 841                             if (vd.isGlobal()) {
 842                                 Updates up=new Updates(ri.getLeftExpr(),0,null);
 843                                 un.addUpdate(up);
 844                             }
 845                         }
 846                         if (!(ri.getRightExpr() instanceof VarExpr)) {
 847                             if (ri.getRightExpr().isValue(ri.getRelation().getRange().getType())) {
 848                                 Updates up=new Updates(ri.getRightExpr(),1,ri.getRelation().getRange().getType());
 849                                 un.addUpdate(up);
 850                             } else {
 851                                 /* We don't handly relation modifies */
 852                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
 853                                     continue;
 854                                 /* We're an add to relation*/
 855                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getRightExpr());
 856                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),false /* Range*/)?
 857                                     sources.relgetSourceSet(ri.getRelation(),false):null;
 858                                 if (set==null)
 859                                     continue;
 860                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 861
 862                                 if (rap==ArrayAnalysis.AccessPath.NONE||
 863                                     !rap.equal(ap)||
 864                                     !constructarrayupdate(un, ri.getRightExpr(), rap, 1))
 865                                     continue;
 866                             }
 867                         } else {
 868                             VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 869                             if (vd.isGlobal()) {
 870                                 Updates up=new Updates(ri.getRightExpr(),1,null);
 871                                 un.addUpdate(up);
 872                             }
 873                         }
 874                     }
 875                     //Finally build necessary updates to satisfy conjunction
 876                     RuleConjunction ruleconj=dnfrule.get(j);
 877
 878                     /* Add in updates for quantifiers */
 879                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
 880                     TermNode tn=new TermNode(mun);
 881                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 882
 883                     if (processquantifiers(gn2,un, r)&&
 884                         processconjunction(un,ruleconj)&&
 885                         un.checkupdates()) {
 886                         mun.addUpdate(un);
 887                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 888                         addtocount++;
 889                         gn.addEdge(e);
 890                         updatenodes.add(gn2);
 891                     }
 892                 }
 893             }
 894         }
 895     }
 896
 897     boolean constructarrayupdate(UpdateNode un, Expr lexpr, ArrayAnalysis.AccessPath ap, int slotnumber) {
 898         System.out.println("Constructing array update");
 899         Expr e=null;
 900         for (int i=ap.numFields()-1;i>=0;i--) {
 901             if (e==null)
 902                 e=lexpr;
 903             else
 904                 e=((DotExpr)e).getExpr();
 905
 906             while (e instanceof CastExpr)
 907                 e=((CastExpr)e).getExpr();
 908
 909             DotExpr de=(DotExpr)e;
 910             FieldDescriptor fd=ap.getField(i);
 911             if (fd instanceof ArrayDescriptor) {
 912                 // We have an ArrayDescriptor!
 913                 Expr index=de.getIndex();
 914                 if (!index.isValue(null)) {/* Not assignable */
 915                     System.out.println("ERROR:Index isn't assignable");
 916                     return false;
 917                 }
 918                 Updates updates=new Updates(index,i,ap,lexpr,slotnumber);
 919                 un.addUpdate(updates);
 920             }
 921         }
 922         return true;
 923     }
 924
 925     /** This method constructs bindings for an update using rule
 926      * r. The boolean flag isremoval indicates that the update
 927      * performs a removal.  The function returns true if it is able to
 928      * generate a valid set of bindings and false otherwise. */
 929
 930     boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
 931         boolean goodupdate=true;
 932         Inclusion inc=r.getInclusion();
 933         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 934             Quantifier q=(Quantifier)iterator.next();
 935             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 936                 VarDescriptor vd=null;
 937                 SetDescriptor set=null;
 938                 if (q instanceof SetQuantifier) {
 939                     vd=((SetQuantifier)q).getVar();
 940                     set=((SetQuantifier)q).getSet();
 941                 } else {
 942                     vd=((ForQuantifier)q).getVar();
 943                 }
 944                 if(inc instanceof SetInclusion) {
 945                     SetInclusion si=(SetInclusion)inc;
 946                     if ((si.elementexpr instanceof VarExpr)&&
 947                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 948                         /* Can solve for v */
 949                         Binding binding=new Binding(vd,0);
 950                         bindings.add(binding);
 951                     } else {
 952                         goodupdate=false;
 953                     }
 954                 } else if (inc instanceof RelationInclusion) {
 955                     RelationInclusion ri=(RelationInclusion)inc;
 956                     boolean f1=true;
 957                     boolean f2=true;
 958                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 959                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 960                                 /* Can solve for v */
 961                         Binding binding=new Binding(vd,0);
 962                         bindings.add(binding);
 963                     } else f1=false;
 964                     if ((ri.getRightExpr() instanceof VarExpr)&&
 965                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 966                                 /* Can solve for v */
 967                         Binding binding=new Binding(vd,0);
 968                         bindings.add(binding);
 969                     } else f2=false;
 970                     if (!(f1||f2))
 971                         goodupdate=false;
 972                 } else throw new Error("Inclusion not recognized");
 973                 if (!goodupdate)
 974                     if (isremoval) {
 975                         /* Removals don't need bindings anymore
 976                            Binding binding=new Binding(vd);
 977                            bindings.add(binding);*/
 978                         goodupdate=true;
 979                     } else if (q instanceof SetQuantifier) {
 980                         /* Create new element to bind to */
 981                         // search if the set 'set' has a size
 982                         Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
 983                         bindings.add(binding);
 984                         goodupdate=true;
 985
 986                     } else
 987                         goodupdate=false;
 988             } else if (q instanceof RelationQuantifier) {
 989                 RelationQuantifier rq=(RelationQuantifier)q;
 990                 for(int k=0;k<2;k++) {
 991                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 992                     if(inc instanceof SetInclusion) {
 993                         SetInclusion si=(SetInclusion)inc;
 994                         if ((si.elementexpr instanceof VarExpr)&&
 995                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 996                             /* Can solve for v */
 997                             Binding binding=new Binding(vd,0);
 998                             bindings.add(binding);
 999                         } else
1000                             goodupdate=false;
1001                     } else if (inc instanceof RelationInclusion) {
1002                         RelationInclusion ri=(RelationInclusion)inc;
1003                         boolean f1=true;
1004                         boolean f2=true;
1005                         if ((ri.getLeftExpr() instanceof VarExpr)&&
1006                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
1007                             /* Can solve for v */
1008                             Binding binding=new Binding(vd,0);
1009                             bindings.add(binding);
1010                         } else f1=false;
1011                         if ((ri.getRightExpr() instanceof VarExpr)&&
1012                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
1013                             /* Can solve for v */
1014                             Binding binding=new Binding(vd,0);
1015                             bindings.add(binding);
1016                         } else f2=false;
1017                         if (!(f1||f2))
1018                             goodupdate=false;
1019                     } else throw new Error("Inclusion not recognized");
1020                     if (!goodupdate)
1021                         if (isremoval) {
1022                             /* Removals don't need bindings anymore
1023                                Binding binding=new Binding(vd);
1024                                bindings.add(binding);*/
1025                             goodupdate=true;
1026                         } else
1027                             break;
1028                 }
1029                 if (!goodupdate)
1030                     break;
1031             } else throw new Error("Quantifier not recognized");
1032         }
1033         return goodupdate;
1034     }
1035
1036     /** Adds updates that add an item to the appropriate set or
1037      * relation quantified over by the model definition rule.. */
1038
1039     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) {
1040         Inclusion inc=r.getInclusion();
1041         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1042             Quantifier q=(Quantifier)iterator.next();
1043             /* Add quantifier */
1044             /* FIXME: Analysis to determine when this update is necessary */
1045             if (q instanceof RelationQuantifier) {
1046                 RelationQuantifier rq=(RelationQuantifier)q;
1047                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
1048                 toe.td=ReservedTypeDescriptor.INT;
1049                 Updates u=new Updates(toe,false);
1050                 un.addUpdate(u);
1051                 if (abstractadd.containsKey(rq.relation)) {
1052                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
1053                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
1054                     gn.addEdge(e);
1055                 } else {
1056                     return false;
1057                 }
1058
1059             } else if (q instanceof SetQuantifier) {
1060                 SetQuantifier sq=(SetQuantifier)q;
1061                 if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
1062                     Binding b=un.getBinding(sq.var);
1063                     Constraint reqc=exactsize.getConstraint(b.getSet());
1064                     constraintdependence.requiresConstraint(gn,reqc);
1065                     continue; /* Don't need to ensure addition for search */
1066                 }
1067
1068                 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
1069                 eoe.td=ReservedTypeDescriptor.INT;
1070                 Updates u=new Updates(eoe,false);
1071                 un.addUpdate(u);
1072                 if (abstractadd.containsKey(sq.set)) {
1073                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
1074                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
1075                     gn.addEdge(e);
1076                 } else {
1077                     return false;
1078                 }
1079             } else return false;
1080         }
1081         return true;
1082     }
1083
1084     /** This method generates the necessary updates to satisfy the
1085      * conjunction ruleconj. */
1086
1087     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
1088         boolean okay=true;
1089         for(int k=0;k<ruleconj.size();k++) {
1090             DNFExpr de=ruleconj.get(k);
1091             Expr e=de.getExpr();
1092             if (e instanceof OpExpr) {
1093                 OpExpr ex=(OpExpr)de.getExpr();
1094                 Opcode op=ex.getOpcode();
1095                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
1096                 un.addUpdate(up);
1097             } else if (e instanceof ElementOfExpr) {
1098                 Updates up=new Updates(e,de.getNegation());
1099                 un.addUpdate(up);
1100             } else if (e instanceof TupleOfExpr) {
1101                 Updates up=new Updates(e,de.getNegation());
1102                 un.addUpdate(up);
1103             } else if (e instanceof BooleanLiteralExpr) {
1104                 boolean truth=((BooleanLiteralExpr)e).getValue();
1105                 if (de.getNegation())
1106                     truth=!truth;
1107                 if (!truth) {
1108                     okay=false;
1109                     break;
1110                 }
1111             } else {
1112                 System.out.println(e.getClass().getName());
1113                 throw new Error("Unrecognized Expr");
1114             }
1115         }
1116         return okay;
1117     }
1118
1119     public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
1120         for(int i=0;i<qs.numQuantifiers();i++) {
1121             Quantifier q=qs.getQuantifier(i);
1122             if (set.contains(q))
1123                 continue;
1124             if (q instanceof SetQuantifier) {
1125                 SetDescriptor sd=((SetQuantifier)q).getSet();
1126                 if (maxsize.getsize(sd)<=1&&
1127                     maxsize.getsize(sd)>=0)
1128                     continue;
1129             } else if (q instanceof RelationQuantifier) {
1130                 RelationDescriptor rd=((RelationQuantifier)q).getRelation();
1131                 if (maxsize.getsize(rd)<=1&&
1132                     maxsize.getsize(rd)>=0)
1133                     continue;
1134             }
1135             return false;
1136         }
1137         return true;
1138     }
1139
1140     public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1141         if (mutualexclusive(sd1,sd2)||
1142             mutualexclusive(sd2,sd1))
1143             return true;
1144         else
1145             return false;
1146     }
1147
1148     private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1149         Vector rules=state.vRules;
1150         for(int i=0;i<rules.size();i++) {
1151             Rule r=(Rule)rules.get(i);
1152             if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
1153                 /* Rule may add items to sd1 */
1154                 SetInclusion si=(SetInclusion)r.getInclusion();
1155                 Expr ve=si.getExpr();
1156                 DNFRule drule=r.getDNFGuardExpr();
1157                 for(int j=0;j<drule.size();j++) {
1158                     RuleConjunction rconj=drule.get(j);
1159                     boolean containsexclusion=false;
1160                     for (int k=0;k<rconj.size();k++) {
1161                         DNFExpr dexpr=rconj.get(k);
1162                         if (dexpr.getNegation()&&
1163                             dexpr.getExpr() instanceof ElementOfExpr&&
1164                             ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
1165                             SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
1166                             if (sd.isSubset(sd2))
1167                                 containsexclusion=true;
1168                         }
1169                     }
1170                     if (!containsexclusion)
1171                         return false;
1172                 }
1173             }
1174         }
1175         return true;
1176     }
1177 }