7 public class ImplicitSchema {
9 SetAnalysis setanalysis;
10 public ImplicitSchema(State state) {
12 this.setanalysis=new SetAnalysis(state);
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)
32 for(int i=0;i<rules.size();i++) {
33 Rule r=(Rule)rules.get(i);
34 if ((r.numQuantifiers()==1)&&
35 (r.getQuantifier(0) instanceof RelationQuantifier)&&
36 (((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
37 r.getInclusion().getTargetDescriptors().contains(sd)) {
38 SetInclusion rinc=(SetInclusion)r.getInclusion();
39 RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
40 VarDescriptor vd=isdomain?rq.x:rq.y;
41 if ((rinc.getExpr() instanceof VarExpr)&&
42 (((VarExpr)rinc.getExpr()).getVar()==vd)&&
43 (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
44 (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
50 for(int i=0;i<rules.size();i++) {
51 Rule r=(Rule)rules.get(i);
52 Inclusion inc=r.getInclusion();
53 if (inc.getTargetDescriptors().contains(rd)) {
54 /* Need to check this rule */
56 RelationInclusion rinc=(RelationInclusion)inc;
57 Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
58 if (expr instanceof VarExpr) {
59 VarDescriptor vd=((VarExpr)expr).getVar();
61 for (int j=0;j<r.numQuantifiers();j++) {
62 Quantifier q=r.getQuantifier(j);
63 if ((q instanceof SetQuantifier)&&
64 (((SetQuantifier)q).getVar()==vd)&&
65 (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
69 if ((q instanceof RelationQuantifier)&&
71 ((((RelationQuantifier)q).x==vd)&&
72 (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
74 ((((RelationQuantifier)q).y==vd)&&
75 (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
83 continue; /* Proved for this case */
85 for(int j=0;j<rules.size();j++) {
86 Rule r2=(Rule)rules.get(j);
87 Inclusion inc2=r2.getInclusion();
89 if (checkimplication(r,r2,isdomain)) {
97 return true; /* Couldn't prove we didn't need */
103 boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
104 /* r1 is the relation */
105 /* See if this rule guarantees relation */
107 1. match up quantifiers
108 2. check inclusion condition
109 3. see if guard expr of set rule is more general */
110 RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
111 RelationDescriptor rd=inc1.getRelation();
112 SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
113 Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
115 Inclusion inc2=r2.getInclusion();
116 if (!(inc2 instanceof SetInclusion))
118 SetInclusion sinc2=(SetInclusion)inc2;
119 if (sinc2.getSet()!=sd)
122 /* Construct a mapping between quantifiers */
123 int[] mapping=new int[r2.numQuantifiers()];
124 HashMap map=new HashMap();
125 for(int i=0;i<r1.numQuantifiers();i++) {
126 Quantifier q1=r1.getQuantifier(i);
127 for (int j=0;j<r2.numQuantifiers();j++) {
129 continue; /* Its already used */
130 Quantifier q2=r2.getQuantifier(j);
131 if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
132 ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
134 map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
137 if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
138 ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
140 map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
141 map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
144 if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
145 ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
146 ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
148 map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
153 /* Make sure all bindings in the set rule are bound */
154 for (int i=0;i<r2.numQuantifiers();i++) {
160 Expr sexpr=sinc2.getExpr();
161 if (!expr.equals(map,sexpr))
162 return false; /* This rule doesn't add the right thing */
164 DNFRule drule1=r1.getDNFGuardExpr();
165 DNFRule drule2=r2.getDNFGuardExpr();
166 for (int i=0;i<drule1.size();i++) {
167 RuleConjunction rconj1=drule1.get(i);
168 boolean foundmatch=false;
169 for (int j=0;j<drule2.size();j++) {
170 RuleConjunction rconj2=drule2.get(j);
171 /* Need to show than rconj2 is true if rconj1 is true */
172 if (implication(map,rconj1,rconj2,sinc2)) {
183 boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
184 for(int i=0;i<rc2.size();i++) {
185 /* Check that rc1 has all predicates that rc2 has */
186 DNFExpr de2=rc2.get(i);
187 /* Predicates for objects that aren't in set */
188 if (de2.getNegation()&&
189 (de2.getExpr() instanceof ElementOfExpr)) {
190 ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
191 if (si.getSet().isSubset(eoe.set)&&
192 si.getExpr().equals(null,eoe.element))
193 continue; /* This predicate isn't a problem */
195 boolean havematch=false;
196 for(int j=0;j<rc1.size();j++) {
197 DNFExpr de1=rc1.get(i);
198 if (de1.getNegation()!=de2.getNegation())
200 if (de1.getExpr().equals(map,de2.getExpr())) {
211 boolean needRange(RelationDescriptor rd) {
212 return needDR(rd, false);
215 void updaterelationconstraints() {
216 Vector reldescriptors=state.stRelations.getAllDescriptors();
217 for(int i=0;i<reldescriptors.size();i++) {
218 RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
219 if (needDomain(rd)||needRange(rd)) {
221 Constraint c=new Constraint();
222 /* Construct quantifier */
223 LogicStatement ls=null;
225 RelationQuantifier rq=new RelationQuantifier();
226 String varname1=new String("relationvar1");
227 VarDescriptor var1=new VarDescriptor(varname1);
228 String varname2=new String("relationvar2");
229 VarDescriptor var2=new VarDescriptor(varname2);
230 rq.setTuple(var1,var2);
233 c.getSymbolTable().add(var1);
234 c.getSymbolTable().add(var2);
235 var1.setType(rd.getDomain().getType());
236 var2.setType(rd.getRange().getType());
238 if (needDomain(rd)) {
239 VarExpr ve1=new VarExpr(var1);
240 SetExpr se1=new SetExpr(rd.getDomain());
241 se1.td=rd.getDomain().getType();
242 ls=new InclusionPredicate(ve1,se1);
247 VarExpr ve2=new VarExpr(var2);
248 SetExpr se2=new SetExpr(rd.getRange());
249 se2.td=rd.getRange().getType();
250 LogicStatement incpred2=new InclusionPredicate(ve2,se2);
251 if (ls==null) ls=incpred2;
252 else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
254 rd.addUsage(RelationDescriptor.IMAGE);
256 c.setLogicStatement(ls);
257 state.vConstraints.add(c);
262 void updateconstraints() {
263 Vector setdescriptors=state.stSets.getAllDescriptors();
264 for(int i=0;i<setdescriptors.size();i++) {
265 SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
266 if(sd.isPartition()) {
267 Constraint c=new Constraint();
268 /* Construct quantifier */
269 SetQuantifier sq=new SetQuantifier();
270 String varname=new String("partitionvar");
271 VarDescriptor var=new VarDescriptor(varname);
272 c.getSymbolTable().add(var);
273 var.setType(sd.getType());
278 /*Construct logic statement*/
279 LogicStatement ls=null;
280 for(int j=0;j<sd.getSubsets().size();j++) {
281 LogicStatement conj=null;
282 for(int k=0;k<sd.getSubsets().size();k++) {
283 VarExpr ve=new VarExpr(var);
284 SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
286 LogicStatement incpred=new InclusionPredicate(ve,se);
288 incpred=new LogicStatement(LogicStatement.NOT ,incpred);
293 conj=new LogicStatement(LogicStatement.AND, conj, incpred);
298 ls=new LogicStatement(LogicStatement.OR, ls, conj);
300 c.setLogicStatement(ls);
301 state.vConstraints.add(c);
307 Vector oldrules=state.vRules;
308 Vector newrules=new Vector();
309 for(int i=0;i<oldrules.size();i++) {
310 Rule r=(Rule)oldrules.get(i);
311 if (r.inclusion instanceof SetInclusion) {
312 SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
313 Set supersets=setanalysis.getSuperset(sd);
315 for(Iterator superit=supersets.iterator();superit.hasNext();) {
316 SetDescriptor sd1=(SetDescriptor)superit.next();
318 nr.setGuardExpr(r.getGuardExpr());
319 nr.quantifiers=r.quantifiers;
320 nr.isstatic=r.isstatic;
321 nr.isdelay=r.isdelay;
322 nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
327 state.implicitrule.put(nr,r);
328 if (!state.implicitruleinv.containsKey(r))
329 state.implicitruleinv.put(r,new HashSet());
330 ((Set)state.implicitruleinv.get(r)).add(nr);
334 oldrules.addAll(newrules);