package MCC.IR;
import MCC.State;
+import MCC.Compiler;
+
import java.util.*;
public class ImplicitSchema {
SetAnalysis setanalysis;
public ImplicitSchema(State state) {
this.state=state;
- this.setanalysis=new SetAnalysis(state);
+ this.setanalysis=state.setanalysis;
}
public void update() {
- updaterules();
+ if (Compiler.REPAIR) {
+ updaterules();
+ }
updateconstraints();
updaterelationconstraints();
}
boolean needDR(RelationDescriptor rd,boolean isdomain) {
Vector rules=state.vRules;
SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+ if (sd instanceof ReservedSetDescriptor)
+ return false;
+
+ /* See if there is a rule that adds the corresponding range or domain
+ of the relation to the correct set */
for(int i=0;i<rules.size();i++) {
Rule r=(Rule)rules.get(i);
if ((r.numQuantifiers()==1)&&
return false;
}
}
-
-
for(int i=0;i<rules.size();i++) {
Rule r=(Rule)rules.get(i);
Inclusion inc=r.getInclusion();
boolean good=false;
RelationInclusion rinc=(RelationInclusion)inc;
Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+ /* Check for varexpr's and quantification over */
if (expr instanceof VarExpr) {
VarDescriptor vd=((VarExpr)expr).getVar();
assert vd!=null;
+ /* See if the var is from an appropriate quantifier */
for (int j=0;j<r.numQuantifiers();j++) {
Quantifier q=r.getQuantifier(j);
if ((q instanceof SetQuantifier)&&
good=true;
break;
}
-
}
if (good)
- continue; /* Proved for this case */
+ continue; /* Checked for this case */
}
+ if (checkguard(r,isdomain))
+ continue;
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 true; /* Couldn't verify we didn't need */
}
}
return false;
}
+ boolean checkguard(Rule r,boolean isdomain) {
+ RelationInclusion inc=(RelationInclusion) r.getInclusion();
+ RelationDescriptor rd=inc.getRelation();
+ SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+ Expr expr=isdomain?inc.getLeftExpr():inc.getRightExpr();
+ DNFRule dnfGuard=r.getDNFGuardExpr();
+ for(int i=0;i<dnfGuard.size();i++) {
+ RuleConjunction rconj=dnfGuard.get(i);
+ boolean foundcheck=false;
+ for(int j=0;j<rconj.size();j++) {
+ DNFExpr dexpr=rconj.get(j);
+ if (!dexpr.getNegation()&&
+ dexpr.getExpr() instanceof ElementOfExpr) {
+ ElementOfExpr eoe=(ElementOfExpr)dexpr.getExpr();
+
+ if (eoe.set==sd&&
+ eoe.element.equals(null,expr)) {
+ foundcheck=true;
+ break;
+ }
+ }
+ }
+ if (!foundcheck) {
+ return false;
+ }
+ }
+ return true;
+ }
+
boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
/* r1 is the relation */
/* See if this rule guarantees relation */
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 */
((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 &&
mapping[j]=1;
map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
- foundmapping=true;
break;
}
+ if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
+ ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
+ ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
+ mapping[j]=1;
+ map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
+ }
}
- if (!foundmapping)
+ }
+
+ /* Make sure all bindings in the set rule are bound */
+ for (int i=0;i<r2.numQuantifiers();i++) {
+ if (mapping[i]!=1)
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++) {
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)) {
+ if (implication(map,rconj1,rconj2,sinc2)) {
foundmatch=true;
break;
}
return true;
}
- boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+ boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
for(int i=0;i<rc2.size();i++) {
/* Check that rc1 has all predicates that rc2 has */
DNFExpr de2=rc2.get(i);
+ /* Predicates for objects that aren't in set */
+ if (de2.getNegation()&&
+ (de2.getExpr() instanceof ElementOfExpr)) {
+ ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
+ if (si.getSet().isSubset(eoe.set)&&
+ si.getExpr().equals(null,eoe.element))
+ continue; /* This predicate isn't a problem */
+ }
boolean havematch=false;
for(int j=0;j<rc1.size();j++) {
DNFExpr de1=rc1.get(i);
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) {
if (supersets!=null)
for(Iterator superit=supersets.iterator();superit.hasNext();) {
SetDescriptor sd1=(SetDescriptor)superit.next();
+ Expr e=((SetInclusion)r.inclusion).getExpr();
+ while(e instanceof CastExpr) {
+ e=((CastExpr)e).getExpr();
+ }
+ if (e instanceof VarExpr) {
+ VarDescriptor vde=((VarExpr)e).getVar();
+ boolean ok=false;
+ for (int j=0;j<r.numQuantifiers();j++) {
+ Quantifier tmp=r.getQuantifier(j);
+ if (tmp instanceof SetQuantifier&&
+ ((SetQuantifier)tmp).getVar()==vde)
+ ok=true; /* Need to make sure we don't have a relation quantifier. */
+ }
+
+ SetDescriptor currentset=e.getSet();
+ if (ok&¤tset!=null&¤tset.isSubset(sd1))
+ continue; /* This rule doesn't add item to
+ 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.isdelay=r.isdelay;
nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
nr.st=r.st;
+ 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());
+ ((Set)state.implicitruleinv.get(r)).add(nr);
}
}
}
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 / blobdiff