X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FImplicitSchema.java;h=f229334e87696c791017656abd7e88e21d4ff65a;hp=85bd076dab1e383bbd69bea470bd85af407abfbb;hb=95271a46ce6573ff5532fda46561d2936cb25393;hpb=816cfe472bc29b4a950e96e5ab8cddb4e24c1556

diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 85bd076..f229334 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -338,6 +338,8 @@ public class ImplicitSchema {
     void updaterules() {
 	Vector oldrules=state.vRules;
 	Vector newrules=new Vector();
+	Vector allrules=new Vector();
+	allrules.addAll(oldrules);
 	for(int i=0;i<oldrules.size();i++) {
 	    Rule r=(Rule)oldrules.get(i);
 	    if (r.inclusion instanceof SetInclusion) {
@@ -366,7 +368,9 @@ public class ImplicitSchema {
 					     this set, as item is already
 					     in this set. */
 			}
-			
+			if (isRedundant(allrules,r,sd1))
+			    continue;
+
 			Rule nr=new Rule();
 			nr.setGuardExpr(r.getGuardExpr());
 			nr.quantifiers=r.quantifiers;
@@ -377,6 +381,7 @@ public class ImplicitSchema {
 			nr.setnogenerate();
 			nr.num=r.num;
 			newrules.add(nr);
+			allrules.add(nr);
 			state.implicitrule.put(nr,r);
 			if (!state.implicitruleinv.containsKey(r))
 			    state.implicitruleinv.put(r,new HashSet());
@@ -386,4 +391,98 @@ public class ImplicitSchema {
 	}
 	oldrules.addAll(newrules);
     }
+
+    private boolean isRedundant(Vector allrules,Rule r,SetDescriptor sd) {
+    outerloop:
+	for(int i=0;i<allrules.size();i++) {
+	    Rule r2=(Rule)allrules.get(i);
+	    if (!(r2.getInclusion() instanceof SetInclusion))
+		continue;
+	    //old rule to the same set as the new rule's inclusion condition
+	    if (sd!=((SetInclusion)r2.getInclusion()).getSet())
+		continue;
+	    //old rule quantifiers over superset of new rule's quantification
+	    Hashtable varmap=buildvarmap(state,r2,r,true);
+	    if (varmap==null)
+		continue;
+	    Expr ei1=((SetInclusion)r.getInclusion()).getExpr();
+	    Expr ei2=((SetInclusion)r2.getInclusion()).getExpr();
+	    if (!ei2.stripCastExpr().equals(varmap,ei1.stripCastExpr())) //adds same expression
+		continue;
+	    DNFRule dr1=r.getDNFGuardExpr();
+	    DNFRule dr2=r2.getDNFGuardExpr();
+
+	    //need to show that whenever the guard in r is satisfied, some guard in r2 is satisfied
+	innerloop1:
+	    for(int j=0;j<dr1.size();j++) {
+		RuleConjunction rc1=dr1.get(j);
+	    innerloop2:
+		for(int k=0;k<dr2.size();k++) {
+		    RuleConjunction rc2=dr2.get(k);
+		    //if rc1 being true implies rc2 being true continue to innerloop1
+		innerloop3:
+		    for(int l=0;l<rc2.size();l++) {
+			DNFExpr de2=rc2.get(l);
+			for(int m=0;m<rc1.size();m++) {
+			    DNFExpr de1=rc1.get(m);
+			    if (de1.getNegation()==de2.getNegation()&&
+				de2.getExpr().equals(varmap,de1.getExpr()))
+				continue innerloop3;
+			}
+			continue innerloop2; //see if we can satisfy some other conjunction
+		    }
+		    continue innerloop1; //all of the expr's in this conjunction are satisfied
+		}
+		continue outerloop;
+	    }
+	    return true;
+	}
+	return false;
+    }
+
+    public static Hashtable buildvarmap(State state,Rule r1,Rule r2,boolean subsetting) {
+	// Building a map between quantifier variables
+	Hashtable varmap=new Hashtable();
+	if (r1.numQuantifiers()!=r2.numQuantifiers())
+	    return null;
+	Set usedQuantifiers=new HashSet();
+    outerloop:
+	for(int i=0;i<r1.numQuantifiers();i++) {
+	    Quantifier q1=r1.getQuantifier(i);
+
+	    if (q1 instanceof SetQuantifier) {
+		for(int j=0;j<r2.numQuantifiers();j++) {
+		    Quantifier q2=r2.getQuantifier(j);
+		    if (!(q2 instanceof SetQuantifier))
+			continue;;
+		    if (usedQuantifiers.contains(q2))
+			continue;
+		    if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()||
+			(subsetting&&((SetQuantifier)q1).getSet().isSubset(((SetQuantifier)q2).getSet()))) {
+			varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+			usedQuantifiers.add(q2);
+			continue outerloop;
+		    }
+		}
+		return null;
+	    } else if (q1 instanceof RelationQuantifier) {
+		for(int j=0;j<r2.numQuantifiers();j++) {
+		    Quantifier q2=r2.getQuantifier(j);
+		    if (!(q2 instanceof RelationQuantifier))
+			continue;
+		    if (usedQuantifiers.contains(q2))
+			continue;
+		    if (((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+			varmap.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+			varmap.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+			usedQuantifiers.add(q2);
+			continue outerloop;
+		    }
+		}
+		return null;
+	    }
+	}
+	return varmap;
+    }
+
 }