X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=5d25732106884d1a26f81fce5a483f974d3559be;hb=726db8dc825fb7f33f64f0aca6a4f63b0ba43313;hp=5b741c1e26a52a1aeae1b24c9e1e256e814cdbf4;hpb=ffbc6aa80c7e3ea6aff0cae778ecdbcdbf49a175;p=repair.git

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 5b741c1..5d25732 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -31,6 +31,12 @@ public class Termination {
     ExactSize exactsize;
     ArrayAnalysis arrayanalysis;
     Sources sources;
+    static String conjoption="style=bold";
+    static String absrepoption="shape=box,color=blue,style=bold";
+    static String updateoption="shape=box,color=red,style=bold";
+    static String scopeoption="color=brown";
+    static String conseqoption="style=bold,color=green";
+    static String compoption="shape=box,color=purple,style=bold";
 
     public Termination(State state) {
 	this.state=state;
@@ -50,7 +56,7 @@ public class Termination {
 	predtoabstractmap=new Hashtable();
 	if (!Compiler.REPAIR)
 	    return;
-	
+
 
 	for(int i=0;i<state.vRules.size();i++)
 	    System.out.println(state.vRules.get(i));
@@ -67,20 +73,27 @@ public class Termination {
 	generateconjunctionnodes();
 	constraintdependence=new ConstraintDependence(state,this);
 
+        debugmsg("Generating scope nodes");
 	generatescopenodes();
+        debugmsg("Generating repair nodes");
 	generaterepairnodes();
+        debugmsg("Generating data structure nodes");
 	generatedatastructureupdatenodes();
-	generatecompensationnodes();
-
+        debugmsg("Generating compensation nodes");
+	if (!Compiler.OMITCOMP)
+	    generatecompensationnodes();
+        debugmsg("Generating abstract edges");
 	generateabstractedges();
+        debugmsg("Generating scope edges");
 	generatescopeedges();
+        debugmsg("Generating update edges");
 	generateupdateedges();
 
 
 	HashSet superset=new HashSet();
 	superset.addAll(conjunctions);
 	HashSet closureset=new HashSet();
-
+        debugmsg("Computing closure");
 	GraphNode.computeclosure(superset,closureset);
 	try {
 	    GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
@@ -129,14 +142,14 @@ public class Termination {
 	    DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
 	    HashSet superset=new HashSet();
 	    Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
-	    
+
 	    if (di.conjunctionnum==-1) {
 		superset.addAll((Set)conjunctionmap.get(constr));
 	    } else {
 		DNFConstraint dnf=constr.dnfconstraint;
 		superset.add(conjtonodemap.get(dnf.get(di.conjunctionnum)));
 	    }
-	    
+
 	    GraphNode.boundedcomputeclosure(superset,null,di.depth);
 	    try {
 		GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+(di.conjunctionnum==-1?"":"-"+di.conjunctionnum)+".dot"),superset);
@@ -164,6 +177,7 @@ public class Termination {
 		GraphNode gn=new GraphNode("Conj"+i+"A"+j,
 					   "Conj ("+i+","+j+") "+dnf.get(j).name()
 					   ,tn);
+		gn.setOption(conjoption);
 		conjunctions.add(gn);
 		if (!conjunctionmap.containsKey(c))
 		    conjunctionmap.put(c,new HashSet());
@@ -184,6 +198,7 @@ public class Termination {
 		    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 					       "Conj ("+i+","+j+") "+dconst.get(0).name()
 					       ,tn);
+		    gn.setOption(conjoption);
 		    conjunctions.add(gn);
 		    if (!conjunctionmap.containsKey(c))
 			conjunctionmap.put(c,new HashSet());
@@ -201,6 +216,7 @@ public class Termination {
 		    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 					       "Conj ("+i+","+j+") "+dconst.get(0).name()
 					       ,tn);
+		    gn.setOption(conjoption);
 		    conjunctions.add(gn);
 		    if (!conjunctionmap.containsKey(c))
 			conjunctionmap.put(c,new HashSet());
@@ -251,7 +267,7 @@ public class Termination {
 	    }
 	    /* Cycle through the rules to look for possible conflicts */
 	    for(int i=0;i<state.vRules.size();i++) {
-		Rule r=(Rule) state.vRules.get(i);  
+		Rule r=(Rule) state.vRules.get(i);
 		if (concreteinterferes.interferes(mun,r,true)) {
 		    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
@@ -271,28 +287,39 @@ public class Termination {
 	    GraphNode gn=(GraphNode)absiterator.next();
 	    TermNode tn=(TermNode)gn.getOwner();
 	    AbstractRepair ar=(AbstractRepair)tn.getAbstract();
-	
+
 	    for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 		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,cons)||
-			abstractinterferes.interferes(ar,dp)) {
-			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
-			gn.addEdge(e);
-			break;
-		    }
-		}
+		/* See if this is a relation wellformedness constraint
+                   that is trivially satisfied. */
+		if (abstractinterferes.checkrelationconstraint(ar, cons))
+		    continue;
+                if (AbstractInterferes.interferesquantifier(ar,cons)) {
+                    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                    gn.addEdge(e);
+                } else {
+                    for(int i=0;i<conj.size();i++) {
+                        DNFPredicate dp=conj.get(i);
+
+                        if (!abstractinterferes.interfereswithpredicate(ar,dp))
+                            continue;
+                        if (getConstraint(gn)==null||
+                            !abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons)) {
+                            GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                            gn.addEdge(e);
+                            break;
+                        }
+                    }
+                }
 	    }
 	    for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 		GraphNode gn2=(GraphNode)scopeiterator.next();
 		TermNode tn2=(TermNode)gn2.getOwner();
 		ScopeNode sn2=tn2.getScope();
-		if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+		if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 		    gn.addEdge(e);
 		}
@@ -300,15 +327,30 @@ public class Termination {
 	}
     }
 
+    Constraint getConstraint(GraphNode gn) {
+        for(Iterator it=gn.inedges();it.hasNext();) {
+            GraphNode.Edge e=(GraphNode.Edge)it.next();
+            GraphNode gnsource=e.getSource();
+            TermNode tnsource=(TermNode)gnsource.getOwner();
+            if (tnsource.getType()==TermNode.CONJUNCTION) {
+                return tnsource.getConstraint();
+            }
+        }
+        return null;
+    }
+
     void generatescopenodes() {
 	for(int i=0;i<state.vRules.size();i++) {
 	    Rule r=(Rule) state.vRules.get(i);
 	    ScopeNode satisfy=new ScopeNode(r,true);
 	    TermNode tnsatisfy=new TermNode(satisfy);
 	    GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
+	    gnsatisfy.setOption(scopeoption);
+	    gnsatisfy.setMerge();
 	    ConsequenceNode cnsatisfy=new ConsequenceNode();
 	    TermNode ctnsatisfy=new TermNode(cnsatisfy);
 	    GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
+	    cgnsatisfy.setOption(conseqoption);
 	    consequence.put(satisfy,cgnsatisfy);
 	    GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 	    gnsatisfy.addEdge(esat);
@@ -319,9 +361,12 @@ public class Termination {
 	    ScopeNode falsify=new ScopeNode(r,false);
 	    TermNode tnfalsify=new TermNode(falsify);
 	    GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
+	    gnfalsify.setOption(scopeoption);
+	    gnfalsify.setMerge();
 	    ConsequenceNode cnfalsify=new ConsequenceNode();
 	    TermNode ctnfalsify=new TermNode(cnfalsify);
 	    GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
+	    cgnfalsify.setOption(conseqoption);
 	    consequence.put(falsify,cgnfalsify);
 	    GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 	    gnfalsify.addEdge(efals);
@@ -330,13 +375,13 @@ public class Termination {
 	    scopenodes.add(gnfalsify);
 	}
     }
-    
+
     void generatescopeedges() {
 	for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 	    GraphNode gn=(GraphNode)scopeiterator.next();
 	    TermNode tn=(TermNode)gn.getOwner();
 	    ScopeNode sn=tn.getScope();
-	    
+
 	    /* Interference edges with conjunctions */
 	    for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 		GraphNode gn2=(GraphNode)conjiterator.next();
@@ -345,8 +390,8 @@ public class Termination {
 		Constraint constr=tn2.getConstraint();
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
-		    if (abstractinterferes.interferes(sn,dp)||
-			AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
+		    if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
+			AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 			GraphNode gnconseq=(GraphNode)consequence.get(sn);
 			gnconseq.addEdge(e);
@@ -358,13 +403,13 @@ public class Termination {
 	    /* Now see if this could effect other model defintion rules */
 	    for(int i=0;i<state.vRules.size();i++) {
 		Rule r=(Rule) state.vRules.get(i);
-		if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
+		if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),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);
 		}
-		if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
+		if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 		    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 		    GraphNode gnconseq=(GraphNode)consequence.get(sn);
@@ -381,14 +426,41 @@ public class Termination {
 	    GraphNode gn=(GraphNode)conjiterator.next();
 	    TermNode tn=(TermNode)gn.getOwner();
 	    Conjunction conj=tn.getConjunction();
+	loop:
 	    for(int i=0;i<conj.size();i++) {
 		DNFPredicate dp=conj.get(i);
 		int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
 		Descriptor d=dp.getPredicate().getDescriptor();
+		if ((dp.getPredicate() instanceof ExprPredicate)&&
+		    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+		    boolean neg=dp.isNegated();
+		    Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
+		    int size=((ExprPredicate)dp.getPredicate()).rightSize();
+		    op=Opcode.translateOpcode(neg,op);
+		    if (((size==1)&&(op==Opcode.EQ))||
+			((size!=1)&&(op==Opcode.NE))||
+			((size<=1)&&(op==Opcode.GE))||
+			((size<1)&&(op==Opcode.GT))||
+			((size>1)&&(op==Opcode.LT))||
+			((size>=1)&&(op==Opcode.LE))) {
+			for(int i2=0;i2<conj.size();i2++) {
+			    DNFPredicate dp2=conj.get(i2);
+			    if ((dp2.getPredicate() instanceof ExprPredicate)&&
+				(((ExprPredicate)dp2.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+				if (equivalent(((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr,
+					       (RelationExpr)((OpExpr)((ExprPredicate)dp2.getPredicate()).expr).left))
+				    continue loop; // comparison predicate ensure that size expr is true - no need to generate abstract repairs...
+			    }
+			}
+		    }
+		}
+
 		for(int j=0;j<array.length;j++) {
 		    AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
 		    TermNode tn2=new TermNode(ar);
-		    GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
+		    //		    GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
+		    GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),dp.name()+" "+ar.type(),tn2);
+		    gn2.setOption(absrepoption);
 		    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 		    gn.addEdge(e);
 		    if (!predtoabstractmap.containsKey(dp))
@@ -409,17 +481,19 @@ public class Termination {
 	    AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd,sources);
 	    TermNode tn=new TermNode(ar);
 	    GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+	    gn.setOption(absrepoption);
 	    if (!predtoabstractmap.containsKey(tp))
 		predtoabstractmap.put(tp,new HashSet());
 	    ((Set)predtoabstractmap.get(tp)).add(gn);
 	    abstractrepair.add(gn);
 	    abstractrepairadd.add(gn);
 	    abstractadd.put(sd,gn);
-	    
+
 	    DNFPredicate tp2=new DNFPredicate(true,ip);
 	    AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd,sources);
 	    TermNode tn2=new TermNode(ar2);
 	    GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+	    gn2.setOption(absrepoption);
 	    if (!predtoabstractmap.containsKey(tp2))
 		predtoabstractmap.put(tp2,new HashSet());
 	    ((Set)predtoabstractmap.get(tp2)).add(gn2);
@@ -435,22 +509,24 @@ public class Termination {
 	    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,sources);
 	    TermNode tn=new TermNode(ar);
 	    GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+	    gn.setOption(absrepoption);
 	    if (!predtoabstractmap.containsKey(tp))
 		predtoabstractmap.put(tp,new HashSet());
 	    ((Set)predtoabstractmap.get(tp)).add(gn);
 	    abstractrepair.add(gn);
 	    abstractrepairadd.add(gn);
 	    abstractadd.put(rd,gn);
-	    
+
 	    DNFPredicate tp2=new DNFPredicate(true,ip);
 	    AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd,sources);
 	    TermNode tn2=new TermNode(ar2);
 	    GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+	    gn2.setOption(absrepoption);
 	    if (!predtoabstractmap.containsKey(tp2))
 		predtoabstractmap.put(tp2,new HashSet());
 	    ((Set)predtoabstractmap.get(tp2)).add(gn2);
@@ -473,6 +549,7 @@ public class Termination {
 		MultUpdateNode mun=new MultUpdateNode(sn);
 		TermNode tn2=new TermNode(mun);
 		GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
+		gn2.setOption(compoption);
 		UpdateNode un=new UpdateNode(r);
 
 		if (j<r.numQuantifiers()) {
@@ -516,7 +593,7 @@ public class Termination {
 		}
 		if (!un.checkupdates()) /* Make sure we have a good update */
 		    continue;
-		
+
 		mun.addUpdate(un);
 		GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
 		compensationcount++;
@@ -542,7 +619,8 @@ public class Termination {
 		generateremovefromsetrelation(gn,ar);
 	    } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 		/* Generate remove/add pairs */
-		generateremovefromsetrelation(gn,ar);
+		if (ar.needsRemoves(state))
+		    generateremovefromsetrelation(gn,ar);
 		generateaddtosetrelation(gn,ar);
 		/* Generate atomic modify */
 		generatemodifyrelation(gn,ar);
@@ -570,13 +648,14 @@ public class Termination {
 	}
 	if (possiblerules.size()==0)
 	    return;
-	
+
 	/* Loop through different ways of falsifying each of these rules */
 	int[] count=new int[possiblerules.size()];
 	while(remains(count,possiblerules,true)) {
 	    MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
 	    TermNode tn=new TermNode(mun);
 	    GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
+	    gn2.setOption(updateoption);
 
 	    boolean goodflag=true;
 	    for(int i=0;i<possiblerules.size();i++) {
@@ -626,8 +705,7 @@ public class Termination {
 		mun.addUpdate(un);
 	    }
 	    if (goodflag) {
-		GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
-		removefromcount++;
+		GraphNode.Edge e=new GraphNode.Edge("abstract"+(removefromcount++),gn2);
 		gn.addEdge(e);
 		updatenodes.add(gn2);
 	    }
@@ -673,7 +751,7 @@ public class Termination {
 	int rightindex=1;
 	if (inverted)
 	    leftindex=2;
-	else 
+	else
 	    rightindex=2;
 
 	// construct set of possible rules
@@ -692,13 +770,14 @@ public class Termination {
 	while(remains(count,possiblerules,false)) {
 	    MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
 	    TermNode tn=new TermNode(mun);
-	    GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
+	    GraphNode gn2=new GraphNode("UpdateMod"+modifycount,tn);
+	    gn2.setOption(updateoption);
 
 	    boolean goodflag=true;
 	    for(int i=0;i<possiblerules.size();i++) {
 		Rule r=(Rule)possiblerules.get(i);
 		UpdateNode un=new UpdateNode(r);
-		
+
 		int c=count[i];
 		if (!processconjunction(un,r.getDNFGuardExpr().get(c),null)) {
 		    goodflag=false;break;
@@ -736,10 +815,10 @@ public class Termination {
 		    if (vd.isGlobal()) {
 			Updates up=new Updates(ri.getRightExpr(),rightindex,null);
 			un.addUpdate(up);
-		    } else if (!inverted) 
+		    } else if (!inverted)
 			goodflag=false;
 		}
-				
+
 		if (!un.checkupdates()) {
 		    goodflag=false;
 		    break;
@@ -770,7 +849,7 @@ public class Termination {
 		 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 */
@@ -792,7 +871,7 @@ public class Termination {
 		    if(inc instanceof SetInclusion) {
 			SetInclusion si=(SetInclusion)inc;
 			Expr e=si.elementexpr;
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=si.getSet().getType())
@@ -830,7 +909,7 @@ public class Termination {
 			RelationInclusion ri=(RelationInclusion)inc;
 
 			Expr e=ri.getLeftExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getDomain().getType())
@@ -871,9 +950,9 @@ public class Termination {
 				un.addUpdate(up);
 			    }
      			}
-			
+
 			e=ri.getRightExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getRange().getType())
@@ -895,7 +974,7 @@ public class Termination {
 				if (set==null)
 				    continue;
 				ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
-				
+
 				if (rap==ArrayAnalysis.AccessPath.NONE||
 				    !rap.equal(ap)||
 				    !constructarrayupdate(un, e, rap, 1))
@@ -921,6 +1000,7 @@ public class Termination {
 		    MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
 		    TermNode tn=new TermNode(mun);
 		    GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
+		    gn2.setOption(updateoption);
 
 		    if (debugmsg("Start processing quantifiers")&&
 			processquantifiers(gn2,un, r,setmapping)&&
@@ -938,7 +1018,6 @@ public class Termination {
 		}
 	    }
 	}
-
     }
 
     boolean debugmsg(String st) {
@@ -952,7 +1031,7 @@ public class Termination {
 	for (int i=ap.numFields()-1;i>=0;i--) {
 	    if (e==null)
 		e=lexpr;
-	    else 
+	    else
 		e=((DotExpr)e).getExpr();
 
 	    while (e instanceof CastExpr)
@@ -1005,11 +1084,11 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 			/* Can solve for v */
-			if (!si.getSet().getType().isSubtypeOf(set.getType()))
+			if (set==null||!si.getSet().getType().isSubtypeOf(set.getType()))
 			    return false;
 			Binding binding=new Binding(vd,0);
 			bindings.add(binding);
@@ -1029,7 +1108,7 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 				/* Can solve for v */
@@ -1050,7 +1129,7 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 				/* Can solve for v */
@@ -1088,7 +1167,7 @@ public class Termination {
 			SetInclusion si=(SetInclusion)inc;
 
 			Expr e=si.elementexpr;
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=td)
@@ -1113,7 +1192,7 @@ public class Termination {
 
 
 			Expr e=ri.getLeftExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getDomain().getType())
@@ -1133,7 +1212,7 @@ public class Termination {
 
 
 			e=ri.getRightExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getRange().getType())
@@ -1168,10 +1247,10 @@ public class Termination {
 	}
 	return goodupdate;
     }
-    
+
     /** Adds updates that add an item to the appropriate set or
      * relation quantified over by the model definition rule.. */
-    
+
     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r,Hashtable setmapping) {
 	Inclusion inc=r.getInclusion();
 	for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
@@ -1190,7 +1269,6 @@ public class Termination {
 		} else {
 		    return false;
 		}
-		
 	    } else if (q instanceof SetQuantifier) {
 		SetQuantifier sq=(SetQuantifier)q;
 		if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
@@ -1255,7 +1333,7 @@ public class Termination {
 	    } else if (e instanceof TupleOfExpr) {
 		Updates up=new Updates(e,de.getNegation());
 		un.addUpdate(up);
-	    } else if (e instanceof BooleanLiteralExpr) { 
+	    } else if (e instanceof BooleanLiteralExpr) {
 		boolean truth=((BooleanLiteralExpr)e).getValue();
 		if (de.getNegation())
 		    truth=!truth;
@@ -1332,4 +1410,29 @@ public class Termination {
 	}
 	return true;
     }
+
+    boolean equivalent(SetExpr se, RelationExpr re) {
+	if (!(se instanceof ImageSetExpr))
+	    return false;
+	ImageSetExpr ise=(ImageSetExpr)se;
+	while(re!=null&&ise!=null) {
+	    if (re.getRelation()!=ise.getRelation())
+		return false;
+	    if (re.inverted()!=ise.inverted())
+		return false;
+	    if (ise.isimageset) {
+		ise=ise.getImageSetExpr();
+		if (!(re.getExpr() instanceof RelationExpr))
+		    return false;
+		re=(RelationExpr)re.getExpr();
+	    } else {
+		if (!(re.getExpr() instanceof VarExpr))
+		    return false;
+		if (((VarExpr)re.getExpr()).getVar()==ise.getVar())
+		    return true; //everything matches
+		return false;
+	    }
+	}
+	return false;
+    }
 }