Adding changes to cvs...
[repair.git] / Repair / RepairCompiler / MCC / IR / Termination.java
index bfbe8db..271d9f2 100755 (executable)
@@ -15,6 +15,8 @@ public class Termination {
     Hashtable scopesatisfy;
     Hashtable scopefalsify;
     Hashtable consequence;
+    Hashtable abstractadd;
+    Hashtable abstractremove;
 
     State state;
 
@@ -29,11 +31,15 @@ public class Termination {
        consequence=new Hashtable();
        updatenodes=new HashSet();
        consequencenodes=new HashSet();
+       abstractadd=new Hashtable();
+       abstractremove=new Hashtable();
+
 
        generateconjunctionnodes();
        generatescopenodes();
        generaterepairnodes();
        generatedatastructureupdatenodes();
+       generatecompensationnodes();
 
        generateabstractedges();
        generatescopeedges();
@@ -42,9 +48,10 @@ public class Termination {
        HashSet superset=new HashSet();
        superset.addAll(conjunctions);
        superset.addAll(abstractrepair);
-       superset.addAll(updatenodes);
-       superset.addAll(scopenodes);
-       superset.addAll(consequencenodes);
+       //superset.addAll(updatenodes);
+       //superset.addAll(scopenodes);
+       //superset.addAll(consequencenodes);
+       //GraphNode.computeclosure(superset);
        try {
            GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
        } catch (Exception e) {
@@ -60,7 +67,9 @@ public class Termination {
            DNFConstraint dnf=c.dnfconstraint;
            for(int j=0;j<dnf.size();j++) {
                TermNode tn=new TermNode(c,dnf.get(j));
-               GraphNode gn=new GraphNode("Conjunction"+i+"B"+j,tn);
+               GraphNode gn=new GraphNode("Conj"+i+"A"+j,
+                                          "Conj ("+i+","+j+") "+dnf.get(j).name()
+                                          ,tn);
                conjunctions.add(gn);
                conjunctionmap.put(c,gn);
            }
@@ -78,14 +87,12 @@ public class Termination {
                if (ConcreteInterferes.interferes(mun,r,true)) {
                    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
-                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
-                   gnconseq.addEdge(e);
+                   gn.addEdge(e);
                }
                if (ConcreteInterferes.interferes(mun,r,false)) {
                    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
-                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
-                   gnconseq.addEdge(e);
+                   gn.addEdge(e);
                }
            }
        }
@@ -101,9 +108,12 @@ public class Termination {
                GraphNode gn2=(GraphNode)conjiterator.next();
                TermNode tn2=(TermNode)gn2.getOwner();
                Conjunction conj=tn2.getConjunction();
+               Constraint cons=tn2.getConstraint();
+
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (AbstractInterferes.interferes(ar,dp)) {
+                   if (AbstractInterferes.interferes(ar,cons)||
+                       AbstractInterferes.interferes(ar,dp)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        gn.addEdge(e);
                        break;
@@ -124,9 +134,11 @@ public class Termination {
                GraphNode gn2=(GraphNode)conjiterator.next();
                TermNode tn2=(TermNode)gn2.getOwner();
                Conjunction conj=tn2.getConjunction();
+               Constraint constr=tn2.getConstraint();
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
+                   if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
+                       AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        GraphNode gnconseq=(GraphNode)consequence.get(sn);
                        gnconseq.addEdge(e);
@@ -154,8 +166,9 @@ public class Termination {
        }
     }
 
-
+    /* Generates the abstract repair nodes */
     void generaterepairnodes() {
+       /* Generate repairs of conjunctions */
        for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
            GraphNode gn=(GraphNode)conjiterator.next();
            TermNode tn=(TermNode)gn.getOwner();
@@ -167,13 +180,129 @@ public class Termination {
                for(int j=0;j<array.length;j++) {
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d);
                    TermNode tn2=new TermNode(ar);
-                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+j,tn2);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
                    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
                    abstractrepair.add(gn2);
                }
            }
        }
+       /* Generate additional abstract repairs */
+       Vector setdescriptors=state.stSets.getAllDescriptors();
+       for(int i=0;i<setdescriptors.size();i++) {
+           SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
+
+           /* XXXXXXX: Not sure what to do here */
+           VarExpr ve=new VarExpr("DUMMY");
+           InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
+           
+           DNFPredicate tp=new DNFPredicate(false,ip);
+           AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
+           TermNode tn=new TermNode(ar);
+           GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+           abstractrepair.add(gn);
+           abstractadd.put(sd,gn);
+           
+           DNFPredicate tp2=new DNFPredicate(true,ip);
+           AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
+           TermNode tn2=new TermNode(ar2);
+           GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+           abstractrepair.add(gn2);
+           abstractremove.put(sd,gn2);
+       }
+
+       Vector relationdescriptors=state.stRelations.getAllDescriptors();
+       for(int i=0;i<relationdescriptors.size();i++) {
+           RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
+
+           /* XXXXXXX: Not sure what to do here */
+           VarDescriptor vd1=new VarDescriptor("DUMMY1");
+           VarExpr ve2=new VarExpr("DUMMY2");
+
+           InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
+           
+           DNFPredicate tp=new DNFPredicate(false,ip);
+           AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
+           TermNode tn=new TermNode(ar);
+           GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+           abstractrepair.add(gn);
+           abstractadd.put(rd,gn);
+           
+           DNFPredicate tp2=new DNFPredicate(true,ip);
+           AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
+           TermNode tn2=new TermNode(ar2);
+           GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+           abstractrepair.add(gn2);
+           abstractremove.put(rd,gn2);
+       }
+       
+    }
+
+    int compensationcount=0;
+    void generatecompensationnodes() {
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           Vector possiblerules=new Vector();
+           /* Construct bindings */
+           Vector bindings=new Vector();
+           constructbindings(bindings, r,true);
+           
+           for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
+               GraphNode gn=(GraphNode)scopesatisfy.get(r);
+               TermNode tn=(TermNode) gn.getOwner();
+               ScopeNode sn=tn.getScope();
+               MultUpdateNode mun=new MultUpdateNode(sn);
+               TermNode tn2=new TermNode(mun);
+               GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
+               UpdateNode un=new UpdateNode();
+               un.addBindings(bindings);
+               if (j<r.numQuantifiers()) {
+                   /* Remove quantifier */
+                   Quantifier q=r.getQuantifier(j);
+                   if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier)q;
+                       TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+                       toe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(toe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(rq.relation)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           continue; /* Abstract repair doesn't exist */
+                       }
+                   } else if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier)q;
+                       ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+                       eoe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(eoe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(sq.set)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           continue; /* Abstract repair doesn't exist */
+                       }
+                   } else {
+                       continue;
+                   }
+               } else {
+                   int c=j-r.numQuantifiers();
+                   if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
+                       continue;
+                   }
+               }
+
+               mun.addUpdate(un);
+
+               GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
+               compensationcount++;
+               gn.addEdge(e);
+               updatenodes.add(gn2);
+           }
+       }
     }
 
     void generatedatastructureupdatenodes() {
@@ -182,34 +311,94 @@ public class Termination {
            TermNode tn=(TermNode) gn.getOwner();
            AbstractRepair ar=tn.getAbstract();
            if (ar.getType()==AbstractRepair.ADDTOSET) {
-               generateaddtoset(gn,ar);
+               generateaddtosetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
-               generateremovefromset(gn,ar);
+               generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
-               generateaddtorelation(gn,ar);
+               generateaddtosetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
-               generateremovefromrelation(gn,ar);
+               generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+               /* Generate remove/add pairs */
+               generateremovefromsetrelation(gn,ar);
+               generateaddtosetrelation(gn,ar);
+               /* Generate atomic modify */
                generatemodifyrelation(gn,ar);
            }
        }
     }
 
-    void generateremovefromset(GraphNode gn,AbstractRepair ar) {
+    int removefromcount=0;
+    void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
        Vector possiblerules=new Vector();
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            if ((r.getInclusion() instanceof SetInclusion)&&
                (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
                possiblerules.add(r);
+           if ((r.getInclusion() instanceof RelationInclusion)&&
+               (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
+               possiblerules.add(r);
        }
+       if (possiblerules.size()==0)
+           return;
        int[] count=new int[possiblerules.size()];
        while(remains(count,possiblerules)) {
-           MultUpdateNode mun=new MultUpdateNode(ar);
+           MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
+           TermNode tn=new TermNode(mun);
+           GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
+
+           boolean goodflag=true;
            for(int i=0;i<possiblerules.size();i++) {
+               Rule r=(Rule)possiblerules.get(i);
                UpdateNode un=new UpdateNode();
+               /* Construct bindings */
+               Vector bindings=new Vector();
+               constructbindings(bindings, r,true);
+               un.addBindings(bindings);
+               if (count[i]<r.numQuantifiers()) {
+                   /* Remove quantifier */
+                   Quantifier q=r.getQuantifier(count[i]);
+                   if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier)q;
+                       TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+                       toe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(toe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(rq.relation)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           goodflag=false;break; /* Abstract repair doesn't exist */
+                       }
+                   } else if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier)q;
+                       ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+                       eoe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(eoe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(sq.set)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           goodflag=false;break; /* Abstract repair doesn't exist */
+                       }
+                   } else {goodflag=false;break;}
+               } else {
+                   int c=count[i]-r.numQuantifiers();
+                   if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
+                       goodflag=false;break;
+                   }
+               }
                mun.addUpdate(un);
-               /* CODE HERE*/
+           }
+           if (goodflag) {
+               GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
+               removefromcount++;
+               gn.addEdge(e);
+               updatenodes.add(gn2);
            }
            increment(count,possiblerules);
        }
@@ -234,163 +423,261 @@ public class Termination {
        return true;
     }
 
-    void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {}
-    void generateaddtorelation(GraphNode gn,AbstractRepair ar) {}
-    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {}
+    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
+    }
+
+
+    boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
+       boolean goodupdate=true;
+       Inclusion inc=r.getInclusion();
+       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+           Quantifier q=(Quantifier)iterator.next();
+           if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
+               VarDescriptor vd=null;
+               SetDescriptor set=null;
+               if (q instanceof SetQuantifier) {
+                   vd=((SetQuantifier)q).getVar();
+               } else
+                   vd=((ForQuantifier)q).getVar();
+               if(inc instanceof SetInclusion) {
+                   SetInclusion si=(SetInclusion)inc;
+                   if ((si.elementexpr instanceof VarExpr)&&
+                       (((VarExpr)si.elementexpr).getVar()==vd)) {
+                       /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else
+                       goodupdate=false;
+               } else if (inc instanceof RelationInclusion) {
+                   RelationInclusion ri=(RelationInclusion)inc;
+                   boolean f1=true;
+                   boolean f2=true;
+                   if ((ri.getLeftExpr() instanceof VarExpr)&&
+                       (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                               /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else f1=false;
+                   if ((ri.getRightExpr() instanceof VarExpr)&&
+                       (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                               /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else f2=false;
+                   if (!(f1||f2))
+                       goodupdate=false;
+               } else throw new Error("Inclusion not recognized");
+               if (!goodupdate)
+                   if (isremoval) {
+                       Binding binding=new Binding(vd);
+                       bindings.add(binding);
+                       goodupdate=true;
+                   } else
+                       break;
+           } else if (q instanceof RelationQuantifier) {
+               RelationQuantifier rq=(RelationQuantifier)q;
+               for(int k=0;k<2;k++) {
+                   VarDescriptor vd=(k==0)?rq.x:rq.y;
+                   if(inc instanceof SetInclusion) {
+                       SetInclusion si=(SetInclusion)inc;
+                       if ((si.elementexpr instanceof VarExpr)&&
+                           (((VarExpr)si.elementexpr).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else
+                           goodupdate=false;
+                   } else if (inc instanceof RelationInclusion) {
+                       RelationInclusion ri=(RelationInclusion)inc;
+                       boolean f1=true;
+                       boolean f2=true;
+                       if ((ri.getLeftExpr() instanceof VarExpr)&&
+                           (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else f1=false;
+                       if ((ri.getRightExpr() instanceof VarExpr)&&
+                           (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else f2=false;
+                       if (!(f1||f2))
+                           goodupdate=false;
+                   } else throw new Error("Inclusion not recognized");
+                   if (!goodupdate)
+                       if (isremoval) {
+                           Binding binding=new Binding(vd);
+                           bindings.add(binding);
+                           goodupdate=true;
+                       } else
+                           break;
+               }
+               if (!goodupdate)
+                   break;
+           } else throw new Error("Quantifier not recognized");
+       }
+       return goodupdate;
+    }
 
     static int addtocount=0;
-    void generateaddtoset(GraphNode gn, AbstractRepair ar) {
+    void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
+       //      System.out.println("Attempting to generate add to set");
+       //System.out.println(ar.getPredicate().getPredicate().name());
+       //System.out.println(ar.getPredicate().isNegated());
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
-           if (r.getInclusion() instanceof SetInclusion) {
-               if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
-                   //Generate add instruction
-                   DNFRule dnfrule=r.getDNFGuardExpr();
-                   for(int j=0;j<dnfrule.size();j++) {
-                       Inclusion inc=r.getInclusion();
-                       UpdateNode un=new UpdateNode();
-                       /* First solve for quantifiers */
-                       boolean goodupdate=true;
-                       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
-                           Quantifier q=(Quantifier)iterator.next();
-                           boolean foundall=true;
-                           if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
-                               VarDescriptor vd=null;
-                               if (q instanceof SetQuantifier)
-                                   vd=((SetQuantifier)q).getVar();
-                               else
-                                   vd=((ForQuantifier)q).getVar();
-                               if(inc instanceof SetInclusion) {
-                                   SetInclusion si=(SetInclusion)inc;
-                                   if ((si.elementexpr instanceof VarExpr)&&
-                                       (((VarExpr)si.elementexpr).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else
-                                       foundall=false;
-                               } else if (inc instanceof RelationInclusion) {
-                                   RelationInclusion ri=(RelationInclusion)inc;
-                                   boolean f1=true;
-                                   boolean f2=true;
-                                   if ((ri.getLeftExpr() instanceof VarExpr)&&
-                                       (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else f1=false;
-                                   if ((ri.getRightExpr() instanceof VarExpr)&&
-                                       (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else f2=false;
-                                   if (!(f1||f2))
-                                       foundall=false;
-                               } else throw new Error("Inclusion not recognized");
-                           } else if (q instanceof RelationQuantifier) {
-                               RelationQuantifier rq=(RelationQuantifier)q;
-                               for(int k=0;k<2;k++) {
-                                   VarDescriptor vd=(k==0)?rq.x:rq.y;
-                                   if(inc instanceof SetInclusion) {
-                                       SetInclusion si=(SetInclusion)inc;
-                                       if ((si.elementexpr instanceof VarExpr)&&
-                                           (((VarExpr)si.elementexpr).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else
-                                           foundall=false;
-                                   } else if (inc instanceof RelationInclusion) {
-                                       RelationInclusion ri=(RelationInclusion)inc;
-                                       boolean f1=true;
-                                       boolean f2=true;
-                                       if ((ri.getLeftExpr() instanceof VarExpr)&&
-                                           (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else f1=false;
-                                       if ((ri.getRightExpr() instanceof VarExpr)&&
-                                                  (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else f2=false;
-                                       if (!(f1||f2))
-                                           foundall=false;
-                                   } else throw new Error("Inclusion not recognized");
-                               }
-                           } else throw new Error("Quantifier not recognized");
-                           if (!foundall) {
-                               goodupdate=false;
-                               break;
+           /* See if this is a good rule*/
+           //System.out.println(r.getGuardExpr().name());
+           if ((r.getInclusion() instanceof SetInclusion&&
+               ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
+               (r.getInclusion() instanceof RelationInclusion&&
+                ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
+
+               /* First solve for quantifiers */
+               Vector bindings=new Vector();
+               /* Construct bindings */
+               //System.out.println("Attempting to generate add to set: #2");
+               if (!constructbindings(bindings,r,false))
+                   continue;
+               //System.out.println("Attempting to generate add to set: #3");
+               //Generate add instruction
+               DNFRule dnfrule=r.getDNFGuardExpr();
+               for(int j=0;j<dnfrule.size();j++) {
+                   Inclusion inc=r.getInclusion();
+                   UpdateNode un=new UpdateNode();
+                   un.addBindings(bindings);
+                   /* Now build update for tuple/set inclusion condition */
+                   if(inc instanceof SetInclusion) {
+                       SetInclusion si=(SetInclusion)inc;
+                       if (!(si.elementexpr instanceof VarExpr)) {
+                           Updates up=new Updates(si.elementexpr,0);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(si.elementexpr,0);
+                               un.addUpdate(up);
                            }
-                           /* Now build update for tuple/set inclusion condition */
-                           if(inc instanceof SetInclusion) {
-                               SetInclusion si=(SetInclusion)inc;
-                               if (!(si.elementexpr instanceof VarExpr)) {
-                                   Updates up=new Updates(si.elementexpr,0);
-                                   un.addUpdate(up);
-                               }
-                           } 
-                           if (inc instanceof RelationInclusion) {
-                               RelationInclusion ri=(RelationInclusion)inc;
-                               if (!(ri.getLeftExpr() instanceof VarExpr)) {
-                                   Updates up=new Updates(ri.getLeftExpr(),0);
-                                   un.addUpdate(up);
-                               }
-                               if (!(ri.getRightExpr() instanceof VarExpr)) {
-                                   Updates up=new Updates(ri.getRightExpr(),0);
-                                   un.addUpdate(up);
-                               }
+                       }
+                   } else if (inc instanceof RelationInclusion) {
+                       RelationInclusion ri=(RelationInclusion)inc;
+                       if (!(ri.getLeftExpr() instanceof VarExpr)) {
+                           Updates up=new Updates(ri.getLeftExpr(),0);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(ri.getLeftExpr(),0);
+                               un.addUpdate(up);
                            }
-                           //Finally build necessary updates to satisfy conjunction
-                           RuleConjunction ruleconj=dnfrule.get(j);
-                           for(int k=0;k<ruleconj.size();k++) {
-                               DNFExpr de=ruleconj.get(k);
-                               Expr e=de.getExpr();
-                               if (e instanceof OpExpr) {
-                                   OpExpr ex=(OpExpr)de.getExpr();
-                                   Opcode op=ex.getOpcode();
-                                   if (de.getNegation()) {
-                                       /* remove negation through opcode translation */
-                                       if (op==Opcode.GT)
-                                           op=Opcode.LE;
-                                       else if (op==Opcode.GE)
-                                           op=Opcode.LT;
-                                       else if (op==Opcode.EQ)
-                                           op=Opcode.NE;
-                                       else if (op==Opcode.NE)
-                                           op=Opcode.EQ;
-                                       else if (op==Opcode.LT)
-                                           op=Opcode.GE;
-                                       else if (op==Opcode.LE)
-                                           op=Opcode.GT;
-                                   }
-                                   Updates up=new Updates(ex.left,ex.right,op);
-                                   un.addUpdate(up);
-                               } else if (e instanceof ElementOfExpr) {
-                                   Updates up=new Updates(e,de.getNegation());
-                                   un.addUpdate(up);
-                               } else if (e instanceof TupleOfExpr) {
-                                   Updates up=new Updates(e,de.getNegation());
-                                   un.addUpdate(up);
-                               } else throw new Error("Error #213");
+                       }
+                       if (!(ri.getRightExpr() instanceof VarExpr)) {
+                           Updates up=new Updates(ri.getRightExpr(),1);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(ri.getRightExpr(),1);
+                               un.addUpdate(up);
                            }
                        }
-                       MultUpdateNode mun=new MultUpdateNode(ar);
+                   }
+                   //Finally build necessary updates to satisfy conjunction
+                   RuleConjunction ruleconj=dnfrule.get(j);
+                   /* Add in updates for quantifiers */
+                   //System.out.println("Attempting to generate add to set #4");
+                   MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
+                   TermNode tn=new TermNode(mun);
+                   GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
+
+                   if (processquantifers(gn2,un, r)&&debugdd()&&
+                       processconjunction(un,ruleconj)) {
+                       //System.out.println("Attempting to generate add to set #5");
                        mun.addUpdate(un);
-                       TermNode tn=new TermNode(mun);
-                       GraphNode gn2=new GraphNode("Update"+addtocount,tn);
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
                        addtocount++;
                        gn.addEdge(e);
-                       updatenodes.add(gn2);
-                   }
+                       updatenodes.add(gn2);}
+               }
+           }
+       }
+    }
+
+    boolean debugdd() {
+       //System.out.println("Attempting to generate add to set DD");
+       return true;
+    }
+
+    boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
+       Inclusion inc=r.getInclusion();
+       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+           Quantifier q=(Quantifier)iterator.next();
+           /* Add quantifier */
+           /* FIXME: Analysis to determine when this update is necessary */
+           if (q instanceof RelationQuantifier) {
+               RelationQuantifier rq=(RelationQuantifier)q;
+               TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+               toe.td=ReservedTypeDescriptor.INT;
+               Updates u=new Updates(toe,false);
+               un.addUpdate(u);
+               if (abstractremove.containsKey(rq.relation)) {
+                   GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
+                   GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                   gn.addEdge(e);
+               } else {
+                   return false;
+               }
+
+           } else if (q instanceof SetQuantifier) {
+               SetQuantifier sq=(SetQuantifier)q;
+               ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+               eoe.td=ReservedTypeDescriptor.INT;
+               Updates u=new Updates(eoe,false);
+               un.addUpdate(u);
+               if (abstractremove.containsKey(sq.set)) {
+                   GraphNode agn=(GraphNode)abstractadd.get(sq.set);
+                   GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                   gn.addEdge(e);
+               } else {
+                   return false;
+               }
+           } else return false;
+       }
+       return true;
+    }
+
+    boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
+       boolean okay=true;
+       for(int k=0;k<ruleconj.size();k++) {
+           DNFExpr de=ruleconj.get(k);
+           Expr e=de.getExpr();
+           if (e instanceof OpExpr) {
+               OpExpr ex=(OpExpr)de.getExpr();
+               Opcode op=ex.getOpcode();
+               Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof ElementOfExpr) {
+               Updates up=new Updates(e,de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof TupleOfExpr) {
+               Updates up=new Updates(e,de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof BooleanLiteralExpr) { 
+               boolean truth=((BooleanLiteralExpr)e).getValue();
+               if (de.getNegation())
+                   truth=!truth;
+               if (!truth) {
+                   okay=false;
+                   break;
                }
+           } else {
+               System.out.println(e.getClass().getName());
+               throw new Error("Error #213");
            }
        }
+       return okay;
     }
 
     void generatescopenodes() {