public class ComputeMaxSize {
State state;
Hashtable sizemap; /* -1 means infinity */
-
+ static int KBOUND=100;
public ComputeMaxSize(State state) {
this.state=state;
sizemap=new Hashtable();
computesizes();
+ postprocess();
+ printsizes();
}
/** This method compute relation and set maximum sizes */
Descriptor d=(Descriptor)dit.next();
if (d instanceof ReservedSetDescriptor)
continue;
- int totalsize=0;
+ int totalstarts=0;
+ int totalchains=0;
+ Rule chainrule=null;
for(int i=0;i<rules.size();i++) {
Rule r=(Rule)rules.get(i);
if (r.getInclusion().getTargetDescriptors().contains(d)) {
/* This rule may add items to this set or relation */
int rulesize=1;
+ boolean start=true;
for(int j=0;j<r.numQuantifiers();j++) {
Quantifier q=r.getQuantifier(j);
int size=0;
if (q instanceof RelationQuantifier) {
Descriptor d2=((RelationQuantifier)q).getRelation();
if (sizemap.containsKey(d2)) {
- size=((Integer)sizemap.get(d2)).intValue();
+ size=getsize(d2);
+ }
+ if (d==d2) {
+ if (!start)
+ size=-1;
+ else
+ size=1;
+ start=false;
}
- if ((size!=0)&&(d==d2))
- size=-1;
} else if (q instanceof SetQuantifier) {
Descriptor d2=((SetQuantifier)q).getSet();
if (sizemap.containsKey(d2)) {
- size=((Integer)sizemap.get(d2)).intValue();
+ size=getsize(d2);
+ }
+ if (d==d2) {
+ if (!start)
+ size=-1;
+ else
+ size=1;
+ start=false;
}
- if ((size!=0)&&(d==d2))
- size=-1;
} else if (q instanceof ForQuantifier) {
ForQuantifier fq=(ForQuantifier)q;
boolean lowint=OpExpr.isInt(fq.lower);
if (size<=0) /* Catch sneaky bounds */
throw new Error("Funny bounds in: "+fq);
} else size=-1;
- } else {
- size=-1;
- }
+ } else
+ throw new Error("Unrecognized Quantifier");
+
if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
rulesize=-1;
else
rulesize=rulesize*size;
}
- if ((rulesize==-1)||(totalsize==-1))
- totalsize=-1;
- else
- totalsize+=rulesize;
+ if (start) {
+ if ((rulesize==-1)||(totalstarts==-1))
+ totalstarts=-1;
+ else
+ totalstarts+=rulesize;
+ } else {
+ if (totalchains==0)
+ chainrule=r;
+ else
+ chainrule=null;
+ if ((rulesize==-1)||(totalchains==-1))
+ totalchains=-1;
+ else
+ totalchains+=rulesize;
+ }
}
}
- if (!sizemap.containsKey(d)||((Integer)sizemap.get(d)).intValue()!=totalsize) {
+ if (totalstarts>=KBOUND)
+ totalstarts=-1;
+ if (totalchains>=KBOUND)
+ totalchains=-1;
+
+ if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
change=true;
- sizemap.put(d,new Integer(totalsize));
+ MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+ sizemap.put(d,so);
}
}
}
}
+
+ void printsizes() {
+ Set descriptorset=new HashSet();
+ descriptorset.addAll(state.stSets.getAllDescriptors());
+ descriptorset.addAll(state.stRelations.getAllDescriptors());
+ for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+ Descriptor d=(Descriptor)dit.next();
+ if (d instanceof ReservedSetDescriptor)
+ continue;
+ System.out.println("size("+d+")="+getsize(d));
+ }
+ }
+
+ private void postprocess() {
+ Vector rules=state.vRules;
+ boolean change=true;
+ Set descriptorset=new HashSet();
+ descriptorset.addAll(state.stSets.getAllDescriptors());
+ descriptorset.addAll(state.stRelations.getAllDescriptors());
+ while(change) {
+ change=false;
+ for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+ Descriptor d=(Descriptor)dit.next();
+ if (d instanceof ReservedSetDescriptor)
+ continue;
+ int totalstarts=0;
+ int totalchains=0;
+ Rule chainrule=null;
+ for(int i=0;i<rules.size();i++) {
+ Rule r=(Rule)rules.get(i);
+ if (r.getInclusion().getTargetDescriptors().contains(d)) {
+ /* This rule may add items to this set or relation */
+ int rulesize=1;
+ boolean start=true;
+ for(int j=0;j<r.numQuantifiers();j++) {
+ Quantifier q=r.getQuantifier(j);
+ int size=0;
+ if (q instanceof RelationQuantifier) {
+ Descriptor d2=((RelationQuantifier)q).getRelation();
+ if (sizemap.containsKey(d2)) {
+ size=getsize(d2);
+ }
+ if (d==d2) {
+ if (!start)
+ size=-1;
+ else
+ size=1;
+ start=false;
+ } else {
+ if (getchainrule(d2)!=null) {
+ if (isMutuallyExclusive(r, getchainrule(d2)))
+ size=getstarts(d2);
+ }
+ }
+ } else if (q instanceof SetQuantifier) {
+ Descriptor d2=((SetQuantifier)q).getSet();
+ if (sizemap.containsKey(d2)) {
+ size=getsize(d2);
+ }
+ if (d==d2) {
+ if (!start)
+ size=-1;
+ else
+ size=1;
+ start=false;
+ } else {
+ if (getchainrule(d2)!=null) {
+ if (isMutuallyExclusive(r, getchainrule(d2)))
+ size=getstarts(d2);
+ }
+ }
+ } else if (q instanceof ForQuantifier) {
+ ForQuantifier fq=(ForQuantifier)q;
+ boolean lowint=OpExpr.isInt(fq.lower);
+ boolean highint=OpExpr.isInt(fq.upper);
+ if (lowint&&highint) {
+ size=1+OpExpr.getInt(fq.upper)-OpExpr.getInt(fq.lower);
+ if (size<=0) /* Catch sneaky bounds */
+ throw new Error("Funny bounds in: "+fq);
+ } else size=-1;
+ } else
+ throw new Error("Unrecognized Quantifier");
+
+ if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
+ rulesize=-1;
+ else
+ rulesize=rulesize*size;
+ }
+
+ if (start) {
+ if ((rulesize==-1)||(totalstarts==-1))
+ totalstarts=-1;
+ else
+ totalstarts+=rulesize;
+ } else {
+ if (totalchains==0)
+ chainrule=r;
+ else
+ chainrule=null;
+ if ((rulesize==-1)||(totalchains==-1))
+ totalchains=-1;
+ else
+ totalchains+=rulesize;
+ }
+ }
+ }
+ if (totalstarts>=KBOUND)
+ totalstarts=-1;
+ if (totalchains>=KBOUND)
+ totalchains=-1;
+
+ if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
+ change=true;
+ MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+ sizemap.put(d,so);
+ }
+ }
+ }
+
+ }
+
+ int getstarts(Descriptor d) {
+ MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+ return so.maxstarts;
+ }
+ int getchains(Descriptor d) {
+ MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+ return so.numberchains;
+ }
int getsize(Descriptor d) {
- return ((Integer)sizemap.get(d)).intValue();
+ MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+ if (so.maxstarts==0)
+ return 0;
+ if (so.numberchains!=0)
+ return -1;
+ return so.maxstarts;
}
-}
+ private Rule getchainrule(Descriptor d) {
+ MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+ return so.chainrule;
+ }
+
+ public static boolean isMutuallyExclusive(Rule r1,Rule r2) {
+ // Building a map between quantifier variables
+ if (r1.numQuantifiers()!=r2.numQuantifiers())
+ return false;
+ Set usedDescriptors=new HashSet();
+ Hashtable varmap=new Hashtable();
+
+ outerloop:
+ for(int i=0;i<r1.numQuantifiers();i++) {
+ Quantifier q1=r1.getQuantifier(i);
+ if (!(q1 instanceof SetQuantifier))
+ return false;
+ if (usedDescriptors.contains(((SetQuantifier)q1).getSet()))
+ return false;
+ usedDescriptors.add(((SetQuantifier)q1).getSet());
+ for(int j=0;j<r2.numQuantifiers();j++) {
+ Quantifier q2=r2.getQuantifier(j);
+ if (!(q2 instanceof SetQuantifier))
+ return false;
+ if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
+ varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+ continue outerloop;
+ }
+ }
+ return false;
+ }
+ DNFRule dr1=r1.getDNFGuardExpr();
+ DNFRule dr2=r2.getDNFGuardExpr();
+ for(int i=0;i<dr1.size();i++) {
+ for(int j=0;j<dr2.size();j++) {
+ RuleConjunction rc1=dr1.get(i);
+ RuleConjunction rc2=dr2.get(j);
+ if (!exclusive(varmap,rc1,rc2))
+ return false;
+ }
+ }
+ return true;
+ }
+
+ private static boolean exclusive(Hashtable varmap, RuleConjunction rc1, RuleConjunction rc2) {
+ for (int i=0;i<rc1.size();i++) {
+ for (int j=0;j<rc2.size();j++) {
+ DNFExpr de1=rc1.get(i);
+ DNFExpr de2=rc2.get(j);
+ if ((de1.getNegation()!=de2.getNegation())&&
+ (de1.getExpr().equals(varmap,de2.getExpr())))
+ return true;
+ }
+ }
+ return false;
+ }
+}
+class MaxSizeObject {
+ int maxstarts;
+ int numberchains;
+ Rule chainrule;
+
+ public MaxSizeObject(int start,int chain, Rule r) {
+ maxstarts=start;
+ numberchains=chain;
+ chainrule=r;
+ }
+}
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) {
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;
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());
}
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;
+ }
+
}
projects / repair.git / commitdiff