7 public class ImplicitSchema {
9 SetAnalysis setanalysis;
10 public ImplicitSchema(State state) {
12 this.setanalysis=state.setanalysis;
15 public void update() {
16 if (Compiler.REPAIR) {
20 updaterelationconstraints();
23 boolean needDomain(RelationDescriptor rd) {
24 return needDR(rd, true);
27 boolean needDR(RelationDescriptor rd,boolean isdomain) {
28 Vector rules=state.vRules;
29 SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
30 if (sd instanceof ReservedSetDescriptor)
33 /* See if there is a rule that adds the corresponding range or domain
34 of the relation to the correct set */
35 for(int i=0;i<rules.size();i++) {
36 Rule r=(Rule)rules.get(i);
37 if ((r.numQuantifiers()==1)&&
38 (r.getQuantifier(0) instanceof RelationQuantifier)&&
39 (((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
40 r.getInclusion().getTargetDescriptors().contains(sd)) {
41 SetInclusion rinc=(SetInclusion)r.getInclusion();
42 RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
43 VarDescriptor vd=isdomain?rq.x:rq.y;
44 if ((rinc.getExpr() instanceof VarExpr)&&
45 (((VarExpr)rinc.getExpr()).getVar()==vd)&&
46 (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
47 (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
51 for(int i=0;i<rules.size();i++) {
52 Rule r=(Rule)rules.get(i);
53 Inclusion inc=r.getInclusion();
54 if (inc.getTargetDescriptors().contains(rd)) {
55 /* Need to check this rule */
57 RelationInclusion rinc=(RelationInclusion)inc;
58 Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
59 /* Check for varexpr's and quantification over */
60 if (expr instanceof VarExpr) {
61 VarDescriptor vd=((VarExpr)expr).getVar();
63 /* See if the var is from an appropriate quantifier */
64 for (int j=0;j<r.numQuantifiers();j++) {
65 Quantifier q=r.getQuantifier(j);
66 if ((q instanceof SetQuantifier)&&
67 (((SetQuantifier)q).getVar()==vd)&&
68 (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
72 if ((q instanceof RelationQuantifier)&&
74 ((((RelationQuantifier)q).x==vd)&&
75 (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
77 ((((RelationQuantifier)q).y==vd)&&
78 (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
85 continue; /* Checked for this case */
87 if (checkguard(r,isdomain))
89 for(int j=0;j<rules.size();j++) {
90 Rule r2=(Rule)rules.get(j);
91 Inclusion inc2=r2.getInclusion();
92 if (checkimplication(r,r2,isdomain)) {
100 return true; /* Couldn't verify we didn't need */
106 boolean checkguard(Rule r,boolean isdomain) {
107 RelationInclusion inc=(RelationInclusion) r.getInclusion();
108 RelationDescriptor rd=inc.getRelation();
109 SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
110 Expr expr=isdomain?inc.getLeftExpr():inc.getRightExpr();
111 DNFRule dnfGuard=r.getDNFGuardExpr();
112 for(int i=0;i<dnfGuard.size();i++) {
113 RuleConjunction rconj=dnfGuard.get(i);
114 boolean foundcheck=false;
115 for(int j=0;j<rconj.size();j++) {
116 DNFExpr dexpr=rconj.get(j);
117 if (!dexpr.getNegation()&&
118 dexpr.getExpr() instanceof ElementOfExpr) {
119 ElementOfExpr eoe=(ElementOfExpr)dexpr.getExpr();
122 eoe.element.equals(null,expr)) {
135 boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
136 /* r1 is the relation */
137 /* See if this rule guarantees relation */
139 1. match up quantifiers
140 2. check inclusion condition
141 3. see if guard expr of set rule is more general */
142 RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
143 RelationDescriptor rd=inc1.getRelation();
144 SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
145 Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
147 Inclusion inc2=r2.getInclusion();
148 if (!(inc2 instanceof SetInclusion))
150 SetInclusion sinc2=(SetInclusion)inc2;
151 if (sinc2.getSet()!=sd)
154 /* Construct a mapping between quantifiers */
155 int[] mapping=new int[r2.numQuantifiers()];
156 HashMap map=new HashMap();
157 for(int i=0;i<r1.numQuantifiers();i++) {
158 Quantifier q1=r1.getQuantifier(i);
159 for (int j=0;j<r2.numQuantifiers();j++) {
161 continue; /* Its already used */
162 Quantifier q2=r2.getQuantifier(j);
163 if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
164 ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
166 map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
169 if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
170 ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
172 map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
173 map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
176 if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
177 ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
178 ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
180 map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
185 /* Make sure all bindings in the set rule are bound */
186 for (int i=0;i<r2.numQuantifiers();i++) {
192 Expr sexpr=sinc2.getExpr();
193 if (!expr.equals(map,sexpr))
194 return false; /* This rule doesn't add the right thing */
196 DNFRule drule1=r1.getDNFGuardExpr();
197 DNFRule drule2=r2.getDNFGuardExpr();
198 for (int i=0;i<drule1.size();i++) {
199 RuleConjunction rconj1=drule1.get(i);
200 boolean foundmatch=false;
201 for (int j=0;j<drule2.size();j++) {
202 RuleConjunction rconj2=drule2.get(j);
203 /* Need to show than rconj2 is true if rconj1 is true */
204 if (implication(map,rconj1,rconj2,sinc2)) {
215 boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
216 for(int i=0;i<rc2.size();i++) {
217 /* Check that rc1 has all predicates that rc2 has */
218 DNFExpr de2=rc2.get(i);
219 /* Predicates for objects that aren't in set */
220 if (de2.getNegation()&&
221 (de2.getExpr() instanceof ElementOfExpr)) {
222 ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
223 if (si.getSet().isSubset(eoe.set)&&
224 si.getExpr().equals(null,eoe.element))
225 continue; /* This predicate isn't a problem */
227 boolean havematch=false;
228 for(int j=0;j<rc1.size();j++) {
229 DNFExpr de1=rc1.get(i);
230 if (de1.getNegation()!=de2.getNegation())
232 if (de1.getExpr().equals(map,de2.getExpr())) {
243 boolean needRange(RelationDescriptor rd) {
244 return needDR(rd, false);
247 void updaterelationconstraints() {
248 Vector reldescriptors=state.stRelations.getAllDescriptors();
249 for(int i=0;i<reldescriptors.size();i++) {
250 RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
251 if (needDomain(rd)||needRange(rd)) {
253 Constraint c=new Constraint();
254 /* Construct quantifier */
255 LogicStatement ls=null;
257 RelationQuantifier rq=new RelationQuantifier();
258 String varname1=new String("relationvar1");
259 VarDescriptor var1=new VarDescriptor(varname1);
260 String varname2=new String("relationvar2");
261 VarDescriptor var2=new VarDescriptor(varname2);
262 rq.setTuple(var1,var2);
265 c.getSymbolTable().add(var1);
266 c.getSymbolTable().add(var2);
267 var1.setType(rd.getDomain().getType());
268 var2.setType(rd.getRange().getType());
270 if (needDomain(rd)) {
271 VarExpr ve1=new VarExpr(var1);
272 SetExpr se1=new SetExpr(rd.getDomain());
273 se1.td=rd.getDomain().getType();
274 ls=new InclusionPredicate(ve1,se1);
279 VarExpr ve2=new VarExpr(var2);
280 SetExpr se2=new SetExpr(rd.getRange());
281 se2.td=rd.getRange().getType();
282 LogicStatement incpred2=new InclusionPredicate(ve2,se2);
283 if (ls==null) ls=incpred2;
284 else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
286 rd.addUsage(RelationDescriptor.IMAGE);
288 c.setLogicStatement(ls);
289 state.vConstraints.add(c);
294 void updateconstraints() {
295 Vector setdescriptors=state.stSets.getAllDescriptors();
296 for(int i=0;i<setdescriptors.size();i++) {
297 SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
298 if(sd.isPartition()) {
299 Constraint c=new Constraint();
300 /* Construct quantifier */
301 SetQuantifier sq=new SetQuantifier();
302 String varname=new String("partitionvar");
303 VarDescriptor var=new VarDescriptor(varname);
304 c.getSymbolTable().add(var);
305 var.setType(sd.getType());
310 /*Construct logic statement*/
311 LogicStatement ls=null;
312 for(int j=0;j<sd.getSubsets().size();j++) {
313 LogicStatement conj=null;
314 for(int k=0;k<sd.getSubsets().size();k++) {
315 VarExpr ve=new VarExpr(var);
316 SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
318 LogicStatement incpred=new InclusionPredicate(ve,se);
320 incpred=new LogicStatement(LogicStatement.NOT ,incpred);
325 conj=new LogicStatement(LogicStatement.AND, conj, incpred);
330 ls=new LogicStatement(LogicStatement.OR, ls, conj);
332 c.setLogicStatement(ls);
333 state.vConstraints.add(c);
339 Vector oldrules=state.vRules;
340 Vector newrules=new Vector();
341 Vector allrules=new Vector();
342 allrules.addAll(oldrules);
343 for(int i=0;i<oldrules.size();i++) {
344 Rule r=(Rule)oldrules.get(i);
345 if (r.inclusion instanceof SetInclusion) {
346 SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
347 Set supersets=setanalysis.getSuperset(sd);
349 for(Iterator superit=supersets.iterator();superit.hasNext();) {
350 SetDescriptor sd1=(SetDescriptor)superit.next();
351 Expr e=((SetInclusion)r.inclusion).getExpr();
352 while(e instanceof CastExpr) {
353 e=((CastExpr)e).getExpr();
355 if (e instanceof VarExpr) {
356 VarDescriptor vde=((VarExpr)e).getVar();
358 for (int j=0;j<r.numQuantifiers();j++) {
359 Quantifier tmp=r.getQuantifier(j);
360 if (tmp instanceof SetQuantifier&&
361 ((SetQuantifier)tmp).getVar()==vde)
362 ok=true; /* Need to make sure we don't have a relation quantifier. */
365 SetDescriptor currentset=e.getSet();
366 if (ok&¤tset!=null&¤tset.isSubset(sd1))
367 continue; /* This rule doesn't add item to
368 this set, as item is already
371 if (isRedundant(allrules,r,sd1))
375 nr.setGuardExpr(r.getGuardExpr());
376 nr.quantifiers=r.quantifiers;
377 nr.isstatic=r.isstatic;
378 nr.isdelay=r.isdelay;
379 nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
385 state.implicitrule.put(nr,r);
386 if (!state.implicitruleinv.containsKey(r))
387 state.implicitruleinv.put(r,new HashSet());
388 ((Set)state.implicitruleinv.get(r)).add(nr);
392 oldrules.addAll(newrules);
395 private boolean isRedundant(Vector allrules,Rule r,SetDescriptor sd) {
397 for(int i=0;i<allrules.size();i++) {
398 Rule r2=(Rule)allrules.get(i);
399 if (!(r2.getInclusion() instanceof SetInclusion))
401 //old rule to the same set as the new rule's inclusion condition
402 if (sd!=((SetInclusion)r2.getInclusion()).getSet())
404 //old rule quantifiers over superset of new rule's quantification
405 Hashtable varmap=buildvarmap(state,r2,r,true);
408 Expr ei1=((SetInclusion)r.getInclusion()).getExpr();
409 Expr ei2=((SetInclusion)r2.getInclusion()).getExpr();
410 if (!ei2.stripCastExpr().equals(varmap,ei1.stripCastExpr())) //adds same expression
412 DNFRule dr1=r.getDNFGuardExpr();
413 DNFRule dr2=r2.getDNFGuardExpr();
415 //need to show that whenever the guard in r is satisfied, some guard in r2 is satisfied
417 for(int j=0;j<dr1.size();j++) {
418 RuleConjunction rc1=dr1.get(j);
420 for(int k=0;k<dr2.size();k++) {
421 RuleConjunction rc2=dr2.get(k);
422 //if rc1 being true implies rc2 being true continue to innerloop1
424 for(int l=0;l<rc2.size();l++) {
425 DNFExpr de2=rc2.get(l);
426 for(int m=0;m<rc1.size();m++) {
427 DNFExpr de1=rc1.get(m);
428 if (de1.getNegation()==de2.getNegation()&&
429 de2.getExpr().equals(varmap,de1.getExpr()))
432 continue innerloop2; //see if we can satisfy some other conjunction
434 continue innerloop1; //all of the expr's in this conjunction are satisfied
443 public static Hashtable buildvarmap(State state,Rule r1,Rule r2,boolean subsetting) {
444 // Building a map between quantifier variables
445 Hashtable varmap=new Hashtable();
446 if (r1.numQuantifiers()!=r2.numQuantifiers())
448 Set usedQuantifiers=new HashSet();
450 for(int i=0;i<r1.numQuantifiers();i++) {
451 Quantifier q1=r1.getQuantifier(i);
453 if (q1 instanceof SetQuantifier) {
454 for(int j=0;j<r2.numQuantifiers();j++) {
455 Quantifier q2=r2.getQuantifier(j);
456 if (!(q2 instanceof SetQuantifier))
458 if (usedQuantifiers.contains(q2))
460 if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()||
461 (subsetting&&((SetQuantifier)q1).getSet().isSubset(((SetQuantifier)q2).getSet()))) {
462 varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
463 usedQuantifiers.add(q2);
468 } else if (q1 instanceof RelationQuantifier) {
469 for(int j=0;j<r2.numQuantifiers();j++) {
470 Quantifier q2=r2.getQuantifier(j);
471 if (!(q2 instanceof RelationQuantifier))
473 if (usedQuantifiers.contains(q2))
475 if (((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
476 varmap.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
477 varmap.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
478 usedQuantifiers.add(q2);