4 class AbstractInterferes {
5 static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
7 boolean mayremove=false;
8 switch (ar.getType()) {
9 case AbstractRepair.ADDTOSET:
10 case AbstractRepair.ADDTORELATION:
11 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
15 case AbstractRepair.REMOVEFROMSET:
16 case AbstractRepair.REMOVEFROMRELATION:
17 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
21 case AbstractRepair.MODIFYRELATION:
22 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
24 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
30 throw new Error("Unrecognized Abstract Repair");
34 drule=r.getDNFGuardExpr();
36 drule=r.getDNFNegGuardExpr();
38 for(int i=0;i<drule.size();i++) {
39 RuleConjunction rconj=drule.get(i);
40 for(int j=0;j<rconj.size();j++) {
41 DNFExpr dexpr=rconj.get(j);
42 Expr expr=dexpr.getExpr();
43 if (expr.usesDescriptor(ar.getDescriptor())) {
45 if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
54 static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
55 if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
56 ((ar.getDescriptor() instanceof SetDescriptor)||
57 !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
60 /* This if handles all the c comparisons in the paper */
61 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
62 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
63 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
64 (dp.getPredicate() instanceof ExprPredicate)&&
65 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
66 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
67 boolean neg1=ar.getPredicate().isNegated();
68 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
69 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
70 boolean neg2=dp.isNegated();
71 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
72 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
73 if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
74 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
77 if((op1==Opcode.EQ)||(op1==Opcode.GE))
79 if((op1==Opcode.GT)||(op1==Opcode.NE))
83 if((op1==Opcode.EQ)||(op1==Opcode.LE))
85 if((op1==Opcode.LT)||(op1==Opcode.NE))
88 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
89 (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
90 (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
91 (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
92 (!neg2&&(op2==Opcode.GE))||
93 (!neg2&&(op2==Opcode.GT))||
94 (neg2&&(op2==Opcode.LE))||
95 (neg2&&(op2==Opcode.LT))||
96 (neg2&&(op2==Opcode.GE)&&(size1a<size2))||
97 (neg2&&(op2==Opcode.GT)&&(size1a<=size2))||
98 (!neg2&&(op2==Opcode.LE)&&(size1a<=size2))||
99 (!neg2&&(op2==Opcode.LT)&&(size1a<size2)))
104 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
105 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
106 (dp.getPredicate() instanceof ExprPredicate)&&
107 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
108 boolean neg2=dp.isNegated();
109 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
110 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
111 if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
112 (neg2&&(op2==Opcode.NE)&&(size2==0))||
113 (!neg2&&(op2==Opcode.GE))||
114 (!neg2&&(op2==Opcode.GT))||
115 (neg2&&(op2==Opcode.LE))||
116 (neg2&&(op2==Opcode.LT)))
120 /* This handles all the c comparisons in the paper */
121 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
122 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
123 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
124 (dp.getPredicate() instanceof ExprPredicate)&&
125 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
126 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
127 boolean neg1=ar.getPredicate().isNegated();
128 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
129 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
130 boolean neg2=dp.isNegated();
131 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
132 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
133 if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
134 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
137 if((op1==Opcode.EQ)||(op1==Opcode.GE))
139 if((op1==Opcode.GT)||(op1==Opcode.NE))
143 if((op1==Opcode.EQ)||(op1==Opcode.LE))
145 if((op1==Opcode.LT)||(op1==Opcode.NE))
148 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
149 (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
150 (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
151 (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
152 (neg2&&(op2==Opcode.GE))||
153 (neg2&&(op2==Opcode.GT))||
154 (!neg2&&(op2==Opcode.LE))||
155 (!neg2&&(op2==Opcode.LT))||
156 (!neg2&&(op2==Opcode.GE)&&(size1a>=size2))||
157 (!neg2&&(op2==Opcode.GT)&&(size1a>size2))||
158 (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
159 (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
164 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
165 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
166 (dp.getPredicate() instanceof ExprPredicate)&&
167 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
168 boolean neg2=dp.isNegated();
169 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
170 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
171 if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
172 (neg2&&(op2==Opcode.NE)&&(size2==0))||
173 (neg2&&(op2==Opcode.GE))||
174 (neg2&&(op2==Opcode.GT))||
175 (!neg2&&(op2==Opcode.LE))||
176 (!neg2&&(op2==Opcode.LT)))
180 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
181 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
182 (dp.getPredicate() instanceof InclusionPredicate)&&
183 (dp.isNegated()==false))
184 return false; /* Could only satisfy this predicate */
186 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
187 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
188 (dp.getPredicate() instanceof InclusionPredicate)&&
189 (dp.isNegated()==true))
190 return false; /* Could only satisfy this predicate */
195 static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
196 if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
198 Set target=r.getInclusion().getTargetDescriptors();
200 for(int i=0;i<r.numQuantifiers();i++) {
201 Quantifier q=r.getQuantifier(i);
202 if (q instanceof SetQuantifier) {
203 SetQuantifier sq=(SetQuantifier) q;
204 if (target.contains(sq.getSet())) {
211 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
212 (dp.getPredicate() instanceof ExprPredicate)&&
213 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
214 boolean neg=dp.isNegated();
215 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
216 int size=((ExprPredicate)dp.getPredicate()).leftsize();
218 /* remove negation through opcode translation */
221 else if (op==Opcode.GE)
223 else if (op==Opcode.EQ)
225 else if (op==Opcode.NE)
227 else if (op==Opcode.LT)
229 else if (op==Opcode.LE)
232 if ((op==Opcode.GE)&&
233 ((size==0)||(size==1)))
235 if ((op==Opcode.GT)&&
240 return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
243 static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
244 if ((des!=dp.getPredicate().getDescriptor()) &&
245 ((des instanceof SetDescriptor)||
246 !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
249 /* This if handles all the c comparisons in the paper */
250 if (des==dp.getPredicate().getDescriptor()&&
252 (dp.getPredicate() instanceof ExprPredicate)&&
253 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
254 boolean neg2=dp.isNegated();
255 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
256 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
258 if ((!neg2&&(op2==Opcode.GE))||
259 (!neg2&&(op2==Opcode.GT))||
260 (neg2&&(op2==Opcode.EQ)&&(size2==0))||
261 (!neg2&&(op2==Opcode.NE)&&(size2==0))||
262 (neg2&&(op2==Opcode.LE))||
263 (neg2&&(op2==Opcode.LT)))
267 /* This if handles all the c comparisons in the paper */
268 if (des==dp.getPredicate().getDescriptor()&&
270 (dp.getPredicate() instanceof ExprPredicate)&&
271 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
272 boolean neg2=dp.isNegated();
273 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
274 int size2=((ExprPredicate)dp.getPredicate()).leftsize();
276 if ((neg2&&(op2==Opcode.GE))||
277 (neg2&&(op2==Opcode.GT))||
278 (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
279 (neg2&&(op2==Opcode.NE)&&(size2==0))||
280 (!neg2&&(op2==Opcode.LE))||
281 (!neg2&&(op2==Opcode.LT)))
285 if ((des==dp.getPredicate().getDescriptor())&&
287 (dp.getPredicate() instanceof InclusionPredicate)&&
288 (dp.isNegated()==false))
289 return false; /* Could only satisfy this predicate */
291 if ((des==dp.getPredicate().getDescriptor())&&
293 (dp.getPredicate() instanceof InclusionPredicate)&&
294 (dp.isNegated()==true))
295 return false; /* Could only satisfy this predicate */
300 static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
301 for(int i=0;i<r.numQuantifiers();i++) {
302 Quantifier q=r.getQuantifier(i);
303 if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
304 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
306 } else if (q instanceof ForQuantifier) {
307 if (q.getRequiredDescriptors().contains(des))
309 } else throw new Error("Unrecognized Quantifier");
314 static public boolean interferes(AbstractRepair ar, Quantifiers q) {
315 if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
316 return interferesquantifier(ar.getDescriptor(),true,q,true);
320 static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
321 return interferesquantifier(des, satisfy, q,true);
324 static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
325 if (interferesquantifier(des,satisfy,r,satisfyrule))
328 DNFRule drule=r.getDNFGuardExpr();
329 for(int i=0;i<drule.size();i++) {
330 RuleConjunction rconj=drule.get(i);
331 for(int j=0;j<rconj.size();j++) {
332 DNFExpr dexpr=rconj.get(j);
333 Expr expr=dexpr.getExpr();
334 boolean negated=dexpr.getNegation();
342 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
343 if (satisfiesrule==satisfyrule) {
344 /* Effect is the one being tested for */
345 /* Only expr's to be concerned with are TupleOfExpr and
347 if (expr.getRequiredDescriptors().contains(des)) {
348 if (((expr instanceof ElementOfExpr)||
349 (expr instanceof TupleOfExpr))&&
350 (expr.getRequiredDescriptors().size()==1))
353 throw new Error("Unrecognized EXPR");