From: bdemsky <bdemsky>
Date: Fri, 23 Jan 2004 03:58:49 +0000 (+0000)
Subject: Fix some of Dan's bugs (code generation for relation quantifiers misstyped), didn... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0ddd66cf596f161886dc67214f3fb2e19f6f7168;p=repair.git

Fix some of Dan's bugs (code generation for relation quantifiers misstyped), didn't allow for relation quantifier in constraints, and my bugs.
---

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index df39d0f..ad98137 100755
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -17,7 +17,7 @@ import MCC.IR.*;
  */
 
 public class Compiler {
-    public static boolean REPAIR=true;
+    public static boolean REPAIR=false;
     
     public static void main(String[] args) {
         State state = null;
@@ -54,11 +54,13 @@ public class Compiler {
 	    success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
 	    success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
 
+	    /* Check partition constraints */
+	    (new ImplicitSchema(state)).update();
+
 	    if (REPAIR) {
-		(new ImplicitSchema(state)).update();
 		Termination t=new Termination(state);
 	    }
-            
+            state.printall();
             (new DependencyBuilder(state)).calculate();
             
             try {
diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 569485c..4217361 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -50,7 +50,24 @@ class AbstractInterferes {
 		    return false;
 	    } 
 	}
-	/* This if handles all the c comparisons in the paper */
+
+	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		(neg2&&(op2==Opcode.NE)&&(size2==0))||
+		(!neg2&&(op2==Opcode.GE))||
+		(!neg2&&(op2==Opcode.GT))||
+		(neg2&&(op2==Opcode.LE))||
+		(neg2&&(op2==Opcode.LT)))
+		return false;
+	}
+
+	/* This handles all the c comparisons in the paper */
 	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 	    (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
@@ -63,8 +80,8 @@ class AbstractInterferes {
 	    boolean neg2=dp.isNegated();
 	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
-	    if ((neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
-		(!neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+	    if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
+		(neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
 		int size1a=0;
 		if (neg1) {
 		    if((op1==Opcode.EQ)||(op1==Opcode.GE))
@@ -91,8 +108,37 @@ class AbstractInterferes {
 		    (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
 		    (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
 		    return false;
-	    } 
+	    }
+	}
+
+	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		(neg2&&(op2==Opcode.NE)&&(size2==0))||
+		(neg2&&(op2==Opcode.GE))||
+		(neg2&&(op2==Opcode.GT))||
+		(!neg2&&(op2==Opcode.LE))||
+		(!neg2&&(op2==Opcode.LT)))
+		return false;
+	    
 	}
+	if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==false))
+	    return false; /* Could only satisfy this predicate */
+
+	if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==true))
+	    return false; /* Could only satisfy this predicate */
+	  
 	return true;
     }
 
@@ -113,6 +159,8 @@ class AbstractInterferes {
 	    {
 		if ((!neg2&&(op2==Opcode.GE))||
 		    (!neg2&&(op2==Opcode.GT))||
+		    (neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		    (!neg2&&(op2==Opcode.NE)&&(size2==0))||
 		    (neg2&&(op2==Opcode.LE))||
 		    (neg2&&(op2==Opcode.LT)))
 		    return false;
@@ -129,15 +177,29 @@ class AbstractInterferes {
 	    {
 		if ((neg2&&(op2==Opcode.GE))||
 		    (neg2&&(op2==Opcode.GT))||
+		    (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		    (neg2&&(op2==Opcode.NE)&&(size2==0))||
 		    (!neg2&&(op2==Opcode.LE))||
 		    (!neg2&&(op2==Opcode.LT)))
 		    return false;
 	    } 
 	}
+	if ((des==dp.getPredicate().getDescriptor())&&
+	    satisfy&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==false))
+	    return false; /* Could only satisfy this predicate */
+
+	if ((des==dp.getPredicate().getDescriptor())&&
+	    (!satisfy)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==true))
+	    return false; /* Could only satisfy this predicate */
+
 	return true;
     }
 
-    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+    static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 	for(int i=0;i<r.numQuantifiers();i++) {
 	    Quantifier q=r.getQuantifier(i);
 	    if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
@@ -148,6 +210,22 @@ class AbstractInterferes {
 		    return true;
 	    } else throw new Error("Unrecognized Quantifier");
 	}
+	return false;
+    }
+
+    static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+	if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
+	    return interferesquantifier(ar.getDescriptor(),true,q,true);
+	return false;
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+	return interferesquantifier(des, satisfy, q,true);
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+	if (interferesquantifier(des,satisfy,r,satisfyrule))
+	    return true;
 	/* Scan DNF form */
 	DNFRule drule=r.getDNFGuardExpr();
 	for(int i=0;i<drule.size();i++) {
diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 5b12c6d..4ccc637 100755
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -12,6 +12,12 @@ public class CastExpr extends Expr {
         this.expr = expr;
     }
 
+    public String name() {
+	String str="";
+	str="(("+type.toString()+")"+expr.name()+")";
+	return str;
+    }
+
     public boolean equals(Map remap, Expr e) {
 	if (e==null)
 	    return false;
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index aeaf4c9..9419563 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -21,7 +21,7 @@ class ConcreteInterferes {
 			RuleConjunction rconj=drule.get(k);
 			for(int l=0;l<rconj.size();l++) {
 			    DNFExpr dexpr=rconj.get(l);
-			    /* See if update interfers w/ dexpr */
+			    /* See if update interferes w/ dexpr */
 			    
 			    if (!dexpr.getExpr().usesDescriptor(updated_des))
 				continue; /* No use of the descriptor */
diff --git a/Repair/RepairCompiler/MCC/IR/Constraint.java b/Repair/RepairCompiler/MCC/IR/Constraint.java
index 97a2c24..f3fdcec 100755
--- a/Repair/RepairCompiler/MCC/IR/Constraint.java
+++ b/Repair/RepairCompiler/MCC/IR/Constraint.java
@@ -2,7 +2,7 @@ package MCC.IR;
 
 import java.util.*;
 
-public class Constraint {
+public class Constraint implements Quantifiers {
     
     private static int count = 1;
 
@@ -19,10 +19,27 @@ public class Constraint {
         label = new String("c" + count++);
     }
 
+    public String toString() {
+	String name="";
+	for(int i=0;i<numQuantifiers();i++) {
+	    name+=getQuantifier(i).toString()+",";
+	}
+	name+=logicstatement.name();
+	return name;
+    }
+
     public int getNum() {
         return num;
     }
 
+    public int numQuantifiers() {
+	return quantifiers.size();
+    }
+
+    public Quantifier getQuantifier(int i) {
+	return (Quantifier) quantifiers.get(i);
+    }
+
     public String getLabel() {
         return label;
     }
@@ -59,7 +76,7 @@ public class Constraint {
 
         for (int i = 0; i < quantifiers.size(); i++) {            
             Quantifier q = (Quantifier) quantifiers.elementAt(i);
-            topdescriptors.addAll(q.getRequiredDescriptors());                
+            topdescriptors.addAll(q.getRequiredDescriptors());
         }
 
         return SetDescriptor.expand(topdescriptors);
diff --git a/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java b/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
index c913a26..9ad6460 100755
--- a/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
+++ b/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
@@ -14,8 +14,7 @@ public class DependencyBuilder {
     }
 
     public void calculate() {
-                     
-        /* reinitialize (clear) nodes */
+	/* reinitialize (clear) nodes */
         constraintnodes = new Hashtable();
         rulenodes = new Hashtable();
 
@@ -109,8 +108,8 @@ public class DependencyBuilder {
                         edge.setDotNodeParameters("style=dotted");
                         otherrulenode.addEdge(edge);
                     }
-                }               
-            }           
+                }
+            }
         }
 
         /* store results in state */
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 4e9d283..6be665b 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -20,6 +20,7 @@ public abstract class Expr {
     }
 
     public String name() {
+	System.out.println(this.getClass().getName());
 	return "?";
     }
 
diff --git a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
index 5739d63..86cf50a 100755
--- a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
@@ -32,7 +32,7 @@ public class ForQuantifier extends Quantifier {
     }
 
     public String toString() {
-        return "for quantifier " + var.getSymbol() + " = " + lower + " to " + upper;
+        return "for quantifier " + var.getSymbol() + " = " + lower.name() + " to " + upper.name();
     }
 
     public void generate_open(CodeWriter writer) {
diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index fde26ad..da50a5a 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -83,6 +83,22 @@ public class GraphNode {
         return owner;
     }
 
+    public static void computeclosure(Set nodes) {
+	Stack tovisit=new Stack();
+	tovisit.addAll(nodes);
+	while(!tovisit.isEmpty()) {
+	    GraphNode gn=(GraphNode)tovisit.pop();
+	    for(Iterator it=gn.edges();it.hasNext();) {
+		Edge edge=(Edge)it.next();
+		GraphNode target=edge.getTarget();
+		if (!nodes.contains(target)) {
+		    nodes.add(target);
+		    tovisit.push(target);
+		}
+	    }
+	}
+    }
+
     public void setDotNodeParameters(String param) {
         if (param == null) {
             throw new NullPointerException();
@@ -195,8 +211,10 @@ public class GraphNode {
                 while (edges.hasNext()) {
                     Edge edge = (Edge) edges.next();
                     GraphNode node = edge.getTarget();
-                    String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
-                    output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+		    if (nodes.contains(node)) {
+			String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
+			output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+		    }
                 }
             }
         }
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 8d61947..1be0068 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -11,38 +11,230 @@ public class ImplicitSchema {
     }
 
     public void update() {
-	updaterules();
+	//	updaterules();
 	updateconstraints();
 	updaterelationconstraints();
     }
 
+    boolean needDomain(RelationDescriptor rd) {
+	return needDR(rd, true);
+    }
+
+    boolean needDR(RelationDescriptor rd,boolean isdomain) {
+	Vector rules=state.vRules;
+	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	for(int i=0;i<rules.size();i++) {
+	    Rule r=(Rule)rules.get(i);
+	    if ((r.numQuantifiers()==1)&&
+		(r.getQuantifier(0) instanceof RelationQuantifier)&&
+		(((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
+		r.getInclusion().getTargetDescriptors().contains(sd)) {
+		SetInclusion rinc=(SetInclusion)r.getInclusion();
+		RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
+		VarDescriptor vd=isdomain?rq.x:rq.y;
+		if ((rinc.getExpr() instanceof VarExpr)&&
+		    (((VarExpr)rinc.getExpr()).getVar()==vd)&&
+		    (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+		    (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
+		    return false;
+	    }
+	}
+
+
+	for(int i=0;i<rules.size();i++) {
+	    Rule r=(Rule)rules.get(i);
+	    Inclusion inc=r.getInclusion();
+	    if (inc.getTargetDescriptors().contains(rd)) {
+		/* Need to check this rule */
+		boolean good=false;
+		RelationInclusion rinc=(RelationInclusion)inc;
+		Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+		if (expr instanceof VarExpr) {
+		    VarDescriptor vd=((VarExpr)expr).getVar();
+		    assert vd!=null;
+		    for (int j=0;j<r.numQuantifiers();j++) {
+			Quantifier q=r.getQuantifier(j);
+			if ((q instanceof SetQuantifier)&&
+			    (((SetQuantifier)q).getVar()==vd)&&
+			    (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
+			    good=true;
+			    break;
+			}
+			if ((q instanceof RelationQuantifier)&&
+			    (
+			    ((((RelationQuantifier)q).x==vd)&&
+			    (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
+			    ||
+			    ((((RelationQuantifier)q).y==vd)&&
+			    (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
+			    )) {
+			    good=true;
+			    break;
+			}
+			
+		    }
+		    if (good)
+			continue; /* Proved for this case */
+		}
+		for(int j=0;j<rules.size();j++) {
+		    Rule r2=(Rule)rules.get(j);
+		    Inclusion inc2=r2.getInclusion();
+		    
+		    if (checkimplication(r,r2,isdomain)) {
+			good=true;
+			break;
+		    }
+		}
+		if (good)
+		    continue;
+
+		return true; /* Couldn't prove we didn't need */
+	    }
+	}
+	return false;
+    }
+
+    boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
+	/* r1 is the relation */
+	/* See if this rule guarantees relation */
+	/* Steps:
+	   1. match up quantifiers
+	   2. check inclusion condition
+	   3. see if guard expr of set rule is more general */
+
+	RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
+	RelationDescriptor rd=inc1.getRelation();
+	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
+
+	Inclusion inc2=r2.getInclusion();
+	if (!(inc2 instanceof SetInclusion))
+	    return false;
+	SetInclusion sinc2=(SetInclusion)inc2;
+	if (sinc2.getSet()!=sd)
+	    return false;
+	if (r1.numQuantifiers()!=r2.numQuantifiers())
+	    return false; 
+	/* Construct a mapping between quantifiers */
+	int[] mapping=new int[r2.numQuantifiers()];
+	HashMap map=new HashMap();
+	for(int i=0;i<r1.numQuantifiers();i++) {
+	    Quantifier q1=r1.getQuantifier(i);
+	    boolean foundmapping=false;
+	    for (int j=0;j<r2.numQuantifiers();j++) {
+		if (mapping[j]==1)
+		    continue; /* Its already used */
+		Quantifier q2=r2.getQuantifier(j);
+		if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
+		    ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
+		    mapping[j]=1;
+		    map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+		    foundmapping=true;
+		    break;
+		}
+		if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
+		    ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+		    mapping[j]=1;
+		    map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+		    map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+		    foundmapping=true;
+		    break;
+		}
+	    }
+	    if (!foundmapping)
+		return false;
+	}
+	/* Built mapping */
+	Expr sexpr=sinc2.getExpr();
+	if (!expr.equals(map,sexpr))
+	    return false;  /* This rule doesn't add the right thing */
+	DNFRule drule1=r1.getDNFGuardExpr();
+	DNFRule drule2=r2.getDNFGuardExpr();
+	for (int i=0;i<drule1.size();i++) {
+	    RuleConjunction rconj1=drule1.get(i);
+	    boolean foundmatch=false;
+	    for (int j=0;j<drule2.size();j++) {
+		RuleConjunction rconj2=drule2.get(j);
+		/* Need to show than rconj2 is true if rconj1 is true */
+		if (implication(map,rconj1,rconj2)) {
+		    foundmatch=true;
+		    break;
+		}
+	    }
+	    if (!foundmatch)
+		return false;
+	}
+	return true;
+    }
+
+    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+	for(int i=0;i<rc2.size();i++) {
+	    /* Check that rc1 has all predicates that rc2 has */
+	    DNFExpr de2=rc2.get(i);
+	    boolean havematch=false;
+	    for(int j=0;j<rc1.size();j++) {
+		DNFExpr de1=rc1.get(i);
+		if (de1.getNegation()!=de2.getNegation())
+		    continue;
+		if (de1.getExpr().equals(map,de2.getExpr())) {
+		    havematch=true;
+		    break;
+		}
+	    }
+	    if (!havematch)
+		return false;
+	}
+	return true;
+    }
+
+    boolean needRange(RelationDescriptor rd) {
+	return needDR(rd, false);
+    }
+
     void updaterelationconstraints() {
 	Vector reldescriptors=state.stRelations.getAllDescriptors();
 	for(int i=0;i<reldescriptors.size();i++) {
 	    RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
-	    Constraint c=new Constraint();
-	    
-	    /* Construct quantifier */
-	    RelationQuantifier rq=new RelationQuantifier();
-	    String varname1=new String("relationvar1");
-	    String varname2=new String("relationvar2");
-	    VarDescriptor var1=new VarDescriptor(varname1);
-	    VarDescriptor var2=new VarDescriptor(varname2);
-	    c.getSymbolTable().add(var1);
-	    c.getSymbolTable().add(var2);
-	    var1.setType(rd.getDomain().getType());
-	    var2.setType(rd.getRange().getType());
-	    rq.setTuple(var1,var2);
-	    rq.setRelation(rd);
-	    c.addQuantifier(rq);
-	    VarExpr ve1=new VarExpr(varname1);
-	    SetExpr se1=new SetExpr(rd.getDomain());
-	    LogicStatement incpred1=new InclusionPredicate(ve1,se1);
-	    VarExpr ve2=new VarExpr(varname2);
-	    SetExpr se2=new SetExpr(rd.getRange());
-	    LogicStatement incpred2=new InclusionPredicate(ve2,se2);
-	    c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
-	    state.vConstraints.add(c);
+	    if (needDomain(rd)||needRange(rd)) {
+		
+		Constraint c=new Constraint();
+		/* Construct quantifier */
+		LogicStatement ls=null;
+
+		RelationQuantifier rq=new RelationQuantifier();
+		String varname1=new String("relationvar1");
+		VarDescriptor var1=new VarDescriptor(varname1);
+		String varname2=new String("relationvar2");
+		VarDescriptor var2=new VarDescriptor(varname2);
+		rq.setTuple(var1,var2);
+		rq.setRelation(rd);
+		c.addQuantifier(rq);
+		c.getSymbolTable().add(var1);
+		c.getSymbolTable().add(var2);
+		var1.setType(rd.getDomain().getType());
+		var2.setType(rd.getRange().getType());
+
+		if (needDomain(rd)) {
+		    VarExpr ve1=new VarExpr(var1);
+		    SetExpr se1=new SetExpr(rd.getDomain());
+		    se1.td=rd.getDomain().getType();
+		    ls=new InclusionPredicate(ve1,se1);
+		}
+
+
+		if (needRange(rd)) {
+		    VarExpr ve2=new VarExpr(var2);
+		    SetExpr se2=new SetExpr(rd.getRange());
+		    se2.td=rd.getRange().getType();
+		    LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+		    if (ls==null) ls=incpred2;
+		    else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
+		}
+		rd.addUsage(RelationDescriptor.IMAGE);
+
+		c.setLogicStatement(ls);
+		state.vConstraints.add(c);
+	    }
 	}
     }
 
@@ -67,8 +259,9 @@ public class ImplicitSchema {
 		for(int j=0;j<sd.getSubsets().size();j++) {
 		    LogicStatement conj=null;
 		    for(int k=0;k<sd.getSubsets().size();k++) {
-			VarExpr ve=new VarExpr(varname);
+			VarExpr ve=new VarExpr(var);
 			SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+			se.td=sd.getType();
 			LogicStatement incpred=new InclusionPredicate(ve,se);
 			if (j!=k) {
 			    incpred=new LogicStatement(LogicStatement.NOT ,incpred);
diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index aa093b4..5871004 100755
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -9,8 +9,10 @@ public class LogicStatement {
     public static final Operation NOT = new Operation("NOT");
 
     public String name() {
+	if (op==NOT)
+	    return "!"+left.name();
 	String name=left.name();
-	name+=op.toString();
+	name+=" "+op.toString()+" ";
 	if (right!=null)
 	    name+=right.name();
 	return name;
diff --git a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
index fdddbeb..033c8d6 100755
--- a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
@@ -4,9 +4,21 @@ import java.util.*;
 class MultUpdateNode {
     Vector updates;
     AbstractRepair abstractrepair;
-    public MultUpdateNode(AbstractRepair ar) {
+    ScopeNode scopenode;
+    int op;
+    static public final int ADD=0;
+    static public final int REMOVE=1;
+    static public final int MODIFY=2;
+
+    public MultUpdateNode(AbstractRepair ar, int op) {
 	updates=new Vector();
 	abstractrepair=ar;
+	this.op=op;
+    }
+
+    public MultUpdateNode(ScopeNode sn) {
+	updates=new Vector();
+	scopenode=sn;
     }
     void addUpdate(UpdateNode un) {
 	updates.add(un);
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index f903a33..8f6aa59 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -29,6 +29,9 @@ public class OpExpr extends Expr {
 	return opcode;
     }
 
+
+
+
     public boolean equals(Map remap, Expr e) {
 	if (e==null||!(e instanceof OpExpr))
 	    return false;
@@ -61,11 +64,13 @@ public class OpExpr extends Expr {
     public boolean usesDescriptor(Descriptor d) {
 	if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
 	    opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
-	    return right.usesDescriptor(d);
+	    return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
+	    //	    return right.usesDescriptor(d);
 	else
 	    return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
     
+
     public int[] getRepairs(boolean negated) {
 	if (left instanceof RelationExpr)
 	    return new int[] {AbstractRepair.MODIFYRELATION};
@@ -73,21 +78,33 @@ public class OpExpr extends Expr {
 	    boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
 	    if (isRelation) {
 		if (opcode==Opcode.EQ)
-		    return new int[] {AbstractRepair.ADDTORELATION,
-					  AbstractRepair.REMOVEFROMRELATION};
+		    if (((IntegerLiteralExpr)right).getValue()==0)
+			return new int[] {AbstractRepair.REMOVEFROMRELATION};
+		    else
+			return new int[] {AbstractRepair.ADDTORELATION,
+					      AbstractRepair.REMOVEFROMRELATION};
 		if (((opcode==Opcode.GE)&&!negated)||
-		    ((opcode==Opcode.LE)&&negated))
-		    return new int[]{AbstractRepair.ADDTORELATION};
+		    ((opcode==Opcode.LE)&&negated)) {
+		    if (((IntegerLiteralExpr)right).getValue()==0)
+			return new int[0];
+		    else
+			return new int[]{AbstractRepair.ADDTORELATION}; }
 		else
 		    return new int[]{AbstractRepair.REMOVEFROMRELATION};
 	    } else {
 		if (opcode==Opcode.EQ)
-		    return new int[] {AbstractRepair.ADDTOSET,
-					  AbstractRepair.REMOVEFROMSET};
+		    if (((IntegerLiteralExpr)right).getValue()==0)
+			return new int[] {AbstractRepair.REMOVEFROMSET};			
+		    else
+			return new int[] {AbstractRepair.ADDTOSET,
+					      AbstractRepair.REMOVEFROMSET};
 		
 		if (((opcode==Opcode.GE)&&!negated)||
-		    ((opcode==Opcode.LE)&&negated))
-		    return new int[] {AbstractRepair.ADDTOSET};
+		    ((opcode==Opcode.LE)&&negated)) {
+		    if (((IntegerLiteralExpr)right).getValue()==0)
+			return new int[0];
+		    else
+			return new int[] {AbstractRepair.ADDTOSET}; }
 		else
 		    return new int[] {AbstractRepair.REMOVEFROMSET};
 	    }
diff --git a/Repair/RepairCompiler/MCC/IR/Quantifier.java b/Repair/RepairCompiler/MCC/IR/Quantifier.java
index 2f5c170..4b50b30 100755
--- a/Repair/RepairCompiler/MCC/IR/Quantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/Quantifier.java
@@ -9,5 +9,4 @@ public abstract class Quantifier {
 
     public abstract int generate_worklistload(CodeWriter writer, int offset);
     public abstract int generate_workliststore(CodeWriter writer, int offset);
-
 }
diff --git a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
index a2b40bc..d1b3a02 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
@@ -17,6 +17,11 @@ public class RelationInclusion extends Inclusion {
         this.relation = relation;
     }
 
+    public String toString() {
+	String str="<"+leftelementexpr.name()+","+rightelementexpr.name()+"> in "+relation.toString();
+	return str;
+    }
+
     public boolean usesDescriptor(Descriptor d) {
 	if (d==relation)
 	    return true;
diff --git a/Repair/RepairCompiler/MCC/IR/RelationQuantifier.java b/Repair/RepairCompiler/MCC/IR/RelationQuantifier.java
index 7281d2e..193e02c 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationQuantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationQuantifier.java
@@ -13,6 +13,10 @@ public class RelationQuantifier extends Quantifier {
         relation = rd; 
     }
 
+    public RelationDescriptor getRelation() {
+	return relation;
+    }
+
     public void setTuple(VarDescriptor x, VarDescriptor y) {
         this.x = x;
         this.y = y;
@@ -31,9 +35,9 @@ public class RelationQuantifier extends Quantifier {
     public void generate_open(CodeWriter writer) {
         writer.outputline("for (SimpleIterator* " + x.getSafeSymbol() + "_iterator = " + relation.getSafeSymbol() + "_hash->iterator(); " + x.getSafeSymbol() + "_iterator->hasNext(); )");
         writer.startblock();
-        writer.outputline(y.getType().getSafeSymbol() + " " + y.getSafeSymbol() + " = (" + y.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->next();");        
+        writer.outputline(y.getType().getGenerateType() + " " + y.getSafeSymbol() + " = (" + y.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->next();");        
         // #ATTN#: key is called second because next() forwards ptr and key does not! 
-        writer.outputline(x.getType().getSafeSymbol() + " " + x.getSafeSymbol() + " = (" + x.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->key();");
+        writer.outputline(x.getType().getGenerateType() + " " + x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->key();");
     }
 
     public int generate_worklistload(CodeWriter writer, int offset) {        
diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java
index 12650d9..017e788 100755
--- a/Repair/RepairCompiler/MCC/IR/Rule.java
+++ b/Repair/RepairCompiler/MCC/IR/Rule.java
@@ -2,7 +2,7 @@ package MCC.IR;
 
 import java.util.*;
 
-public class Rule {
+public class Rule implements Quantifiers {
     
     static int count = 1;
 
@@ -23,6 +23,15 @@ public class Rule {
         label = new String("rule" + count++);
     }
     
+    public String toString() {
+	String name="";
+	for(int i=0;i<numQuantifiers();i++) {
+	    name+=getQuantifier(i).toString()+",";
+	}
+	name+=guard.name()+"=>"+inclusion.toString();
+	return name;
+    }
+
     public int numQuantifiers() {
 	return quantifiers.size();
     }
diff --git a/Repair/RepairCompiler/MCC/IR/SetDescriptor.java b/Repair/RepairCompiler/MCC/IR/SetDescriptor.java
index 6bd62ed..2b42ac2 100755
--- a/Repair/RepairCompiler/MCC/IR/SetDescriptor.java
+++ b/Repair/RepairCompiler/MCC/IR/SetDescriptor.java
@@ -28,7 +28,8 @@ public class SetDescriptor extends Descriptor {
             
             if (descriptor instanceof SetDescriptor) {
                 expanded.addAll(((SetDescriptor) descriptor).allSubsets());
-            }
+            } else
+		expanded.add(descriptor); /* Still need the descriptor */
         }
 
         expanded.addAll(descriptors);
diff --git a/Repair/RepairCompiler/MCC/IR/SetInclusion.java b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
index cdf67b2..9d37572 100755
--- a/Repair/RepairCompiler/MCC/IR/SetInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
@@ -13,6 +13,12 @@ public class SetInclusion extends Inclusion {
     static boolean worklist = false;
     public boolean dostore = true;
 
+    public String toString() {
+	String str="";
+	str+=elementexpr.name()+" in "+set;
+	return str;
+    }
+
     public SetInclusion(Expr elementexpr, SetDescriptor set) {
         this.elementexpr = elementexpr;
         this.set = set;
@@ -25,6 +31,10 @@ public class SetInclusion extends Inclusion {
 	    return elementexpr.usesDescriptor(d);
     }
 
+    public Expr getExpr() {
+	return elementexpr;
+    }
+
     public SetDescriptor getSet() {
         return set;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/TermNode.java b/Repair/RepairCompiler/MCC/IR/TermNode.java
index 9e3dbe8..7fadf32 100755
--- a/Repair/RepairCompiler/MCC/IR/TermNode.java
+++ b/Repair/RepairCompiler/MCC/IR/TermNode.java
@@ -55,6 +55,13 @@ class TermNode {
 	    return conj;
     }
 
+    public Constraint getConstraint() {
+	if (type!=CONJUNCTION)
+	    throw new Error("Not Conjunction Node!");
+	else
+	    return constr;
+    }
+
     public MultUpdateNode getUpdate() {
 	if (type!=UPDATE)
 	    throw new Error("Not Update Node!");
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 0b01ab9..f9ae3bb 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -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) {
@@ -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();
@@ -174,6 +187,122 @@ public class Termination {
 		}
 	    }
 	}
+	/* 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() {
@@ -190,6 +319,10 @@ public class Termination {
 	    } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 		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);
 	    }
 	}
@@ -207,9 +340,14 @@ public class Termination {
 		(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);
@@ -217,6 +355,7 @@ public class Termination {
 		/* 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]);
@@ -226,12 +365,26 @@ public class Termination {
 			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();
@@ -242,8 +395,6 @@ public class Termination {
 		mun.addUpdate(un);
 	    }
 	    if (goodflag) {
-		TermNode tn=new TermNode(mun);
-		GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 		GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
 		removefromcount++;
 		gn.addEdge(e);
@@ -437,13 +588,14 @@ public class Termination {
 		    RuleConjunction ruleconj=dnfrule.get(j);
 		    /* Add in updates for quantifiers */
 		    System.out.println("Attempting to generate add to set #4");
-		    if (processquantifers(un, r)&&debugdd()&&
+		    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");
-			MultUpdateNode mun=new MultUpdateNode(ar);
 			mun.addUpdate(un);
-			TermNode tn=new TermNode(mun);
-			GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 			GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 			addtocount++;
 			gn.addEdge(e);
@@ -458,8 +610,7 @@ public class Termination {
 	return true;
     }
 
-    boolean processquantifers(UpdateNode un, Rule r) {
-	boolean goodupdate=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();
@@ -471,15 +622,30 @@ public class Termination {
 		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);
-	    } else {goodupdate=false; break;}
+		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 goodupdate;
+	return true;
     }
 
     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
diff --git a/Repair/RepairCompiler/MCC/State.java b/Repair/RepairCompiler/MCC/State.java
index ee1dfa0..9f907a9 100755
--- a/Repair/RepairCompiler/MCC/State.java
+++ b/Repair/RepairCompiler/MCC/State.java
@@ -49,4 +49,15 @@ public class State {
         ptSpace = null;
     }
 
+    void printall() {
+	for(int i=0;i<vRules.size();i++) {
+	    Rule r=(Rule)vRules.get(i);
+	    System.out.println(r.toString());
+	}
+	for(int i=0;i<vConstraints.size();i++) {
+	    Constraint c=(Constraint)vConstraints.get(i);
+	    System.out.println(c.toString());
+	}
+    }
+    
 }
diff --git a/Repair/RepairCompiler/MCC/link.model b/Repair/RepairCompiler/MCC/link.model
index 18c9466..1953ef2 100755
--- a/Repair/RepairCompiler/MCC/link.model
+++ b/Repair/RepairCompiler/MCC/link.model
@@ -1,7 +1,6 @@
 [], literal(true) => head in Nodes;
 [forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes;
 [forall node in Nodes], !(node.next=literal(0)) => <node, node.next> in nextnodes;
-[forall node in Nodes], !(node.prev=literal(0)) => node.prev in Nodes;
 [forall node in Nodes], !(node.prev=literal(0)) => <node, node.prev> in prevnodes;