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