4 class AbstractInterferes {
5 Termination termination;
7 public AbstractInterferes(Termination t) {
11 /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
14 static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
16 boolean mayremove=false;
17 switch (ar.getType()) {
18 case AbstractRepair.ADDTOSET:
19 case AbstractRepair.ADDTORELATION:
20 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
24 case AbstractRepair.REMOVEFROMSET:
25 case AbstractRepair.REMOVEFROMRELATION:
26 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
30 case AbstractRepair.MODIFYRELATION:
31 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
33 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
39 throw new Error("Unrecognized Abstract Repair");
43 drule=r.getDNFGuardExpr();
45 drule=r.getDNFNegGuardExpr();
47 for(int i=0;i<drule.size();i++) {
48 RuleConjunction rconj=drule.get(i);
49 for(int j=0;j<rconj.size();j++) {
50 DNFExpr dexpr=rconj.get(j);
51 Expr expr=dexpr.getExpr();
52 if (expr.usesDescriptor(ar.getDescriptor())) {
54 if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
62 /** Does performing the AbstractRepair ar falsify the predicate dp */
64 public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
65 if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
66 ((ar.getDescriptor() instanceof SetDescriptor)||
67 !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
70 /* This if handles all the c comparisons in the paper */
71 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
72 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
73 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
74 (dp.getPredicate() instanceof ExprPredicate)&&
75 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
76 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
77 boolean neg1=ar.getPredicate().isNegated();
78 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
79 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
80 boolean neg2=dp.isNegated();
81 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
82 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
83 op1=Opcode.translateOpcode(neg1,op1);
84 op2=Opcode.translateOpcode(neg2,op2);
86 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
88 if((op1==Opcode.EQ)||(op1==Opcode.GE))
90 if((op1==Opcode.GT)||(op1==Opcode.NE))
93 if (((op2==Opcode.EQ)&&(size1a==size2))||
94 ((op2==Opcode.NE)&&(size1a!=size2))||
97 ((op2==Opcode.LE)&&(size1a<=size2))||
98 ((op2==Opcode.LT)&&(size1a<size2)))
102 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
103 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
104 (dp.getPredicate() instanceof ExprPredicate)&&
105 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
106 boolean neg2=dp.isNegated();
107 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
108 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
110 op2=Opcode.translateOpcode(neg2,op2);
112 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
115 ((op2==Opcode.LT&&size2>maxsize)||
116 (op2==Opcode.LE&&size2>=maxsize)||
117 (op2==Opcode.EQ&&size2>=maxsize)))
120 if (((op2==Opcode.NE)&&(size2==0))||
125 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
126 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
127 (dp.getPredicate() instanceof ExprPredicate)&&
128 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
129 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
131 boolean neg1=ar.getPredicate().isNegated();
132 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
133 boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
134 int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
135 Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
138 boolean neg2=dp.isNegated();
139 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
140 boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
141 int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
142 Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
145 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
146 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
147 SetDescriptor sd1=lexpr1.getSet();
148 SetDescriptor sd2=lexpr2.getSet();
149 if (termination.mutuallyexclusive(sd1,sd2))
153 /* Translate the opcodes */
154 op1=Opcode.translateOpcode(neg1,op1);
155 op2=Opcode.translateOpcode(neg2,op2);
157 /* Obvious cases which can't interfere */
158 if (((op1==Opcode.GT)||
163 if (((op1==Opcode.LT)||
168 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
169 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
170 expr1.equals(null,expr2)) {
173 if (isInt1&&isInt2) {
174 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
175 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
185 size1a++; /*FLAGNE this is current behavior for NE repairs */
191 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
192 ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
195 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
196 ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
199 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
202 if ((op1==Opcode.EQ)&&
203 ((op2==Opcode.LE)||(op2==Opcode.LT))&&
206 if ((op1==Opcode.EQ)&&
207 ((op2==Opcode.GE)||(op2==Opcode.GT))&&
210 if (op2==Opcode.NE) /*FLAGNE this is current behavior for NE repairs */
213 if ((op1==Opcode.NE)&&
217 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
218 ((op2==Opcode.GT)||(op2==Opcode.GE))&&
221 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
222 ((op2==Opcode.LT)||(op2==Opcode.LE))&&
227 /* This handles all the c comparisons in the paper */
228 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
229 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
230 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
231 (dp.getPredicate() instanceof ExprPredicate)&&
232 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
233 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
234 boolean neg1=ar.getPredicate().isNegated();
235 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
236 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
237 boolean neg2=dp.isNegated();
238 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
239 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
240 /* Translate the opcodes */
241 op1=Opcode.translateOpcode(neg1,op1);
242 op2=Opcode.translateOpcode(neg2,op2);
244 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
247 if((op1==Opcode.EQ)||(op1==Opcode.LE))
249 if((op1==Opcode.LT)||(op1==Opcode.NE))
252 if (((op2==Opcode.EQ)&&(size1a==size2))||
253 ((op2==Opcode.NE)&&(size1a!=size2))||
256 ((op2==Opcode.GE)&&(size1a>=size2))||
257 ((op2==Opcode.GT)&&(size1a>size2)))
262 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
263 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
264 (dp.getPredicate() instanceof ExprPredicate)&&
265 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
266 boolean neg2=dp.isNegated();
267 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
268 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
269 op2=Opcode.translateOpcode(neg2,op2);
271 if (((op2==Opcode.EQ)&&(size2==0))||
276 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
277 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
278 (dp.getPredicate() instanceof InclusionPredicate)&&
279 (dp.isNegated()==false))
280 return false; /* Could only satisfy this predicate */
282 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
283 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
284 (dp.getPredicate() instanceof InclusionPredicate)&&
285 (dp.isNegated()==true))
286 return false; /* Could only satisfy this predicate */
290 /** Does the increase (or decrease) in scope of a model defintion
291 * rule represented by sn falsify the predicate dp. */
293 public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
294 if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
296 Set target=r.getInclusion().getTargetDescriptors();
298 for(int i=0;i<r.numQuantifiers();i++) {
299 Quantifier q=r.getQuantifier(i);
300 if (q instanceof SetQuantifier) {
301 SetQuantifier sq=(SetQuantifier) q;
302 if (target.contains(sq.getSet())) {
309 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
310 (dp.getPredicate() instanceof ExprPredicate)&&
311 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
312 boolean neg=dp.isNegated();
313 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
314 int size=((ExprPredicate)dp.getPredicate()).rightSize();
315 op=Opcode.translateOpcode(neg,op);
317 if ((op==Opcode.GE)&&
318 ((size==0)||(size==1)))
320 if ((op==Opcode.GT)&&
325 return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
328 /** Does increasing (or decreasing if satisfy=false) the size of
329 * the set or relation des falsify the predicate dp. */
331 private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
332 if ((des!=dp.getPredicate().getDescriptor()) &&
333 ((des instanceof SetDescriptor)||
334 !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
337 /* This if handles all the c comparisons in the paper */
338 if (des==dp.getPredicate().getDescriptor()&&
340 (dp.getPredicate() instanceof ExprPredicate)&&
341 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
342 boolean neg2=dp.isNegated();
343 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
344 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
345 op2=Opcode.translateOpcode(neg2,op2);
348 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
351 ((op2==Opcode.LT&&size2>maxsize)||
352 (op2==Opcode.LE&&size2>=maxsize)||
353 (op2==Opcode.EQ&&size2>=maxsize)))
356 if ((op2==Opcode.GE)||
358 (op2==Opcode.NE)&&(size2==0))
362 /* This if handles all the c comparisons in the paper */
363 if (des==dp.getPredicate().getDescriptor()&&
365 (dp.getPredicate() instanceof ExprPredicate)&&
366 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
367 boolean neg2=dp.isNegated();
368 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
369 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
370 op2=Opcode.translateOpcode(neg2,op2);
372 if (((op2==Opcode.EQ)&&(size2==0))||
378 if ((des==dp.getPredicate().getDescriptor())&&
380 (dp.getPredicate() instanceof InclusionPredicate)&&
381 (dp.isNegated()==false))
382 return false; /* Could only satisfy this predicate */
384 if ((des==dp.getPredicate().getDescriptor())&&
386 (dp.getPredicate() instanceof InclusionPredicate)&&
387 (dp.isNegated()==true))
388 return false; /* Could only satisfy this predicate */
393 /** This method test whether satisfying (or falsifying depending
394 * on the flag satisfy) a rule that adds an object(or tuple) to
395 * the set(or relation) descriptor may increase (or decrease
396 * depending on the flag satisfyrule) the scope of a constraint or
397 * model defintion rule r. */
399 static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
400 for(int i=0;i<r.numQuantifiers();i++) {
401 Quantifier q=r.getQuantifier(i);
402 if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
403 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
405 } else if (q instanceof ForQuantifier) {
406 if (q.getRequiredDescriptors().contains(des))
408 } else throw new Error("Unrecognized Quantifier");
413 static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
414 if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
415 return interferesquantifier(ar.getDescriptor(),true,q,true);
419 static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
420 return interferesquantifier(des, satisfy, q,true);
423 static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
424 if (interferesquantifier(des,satisfy,r,satisfyrule))
427 DNFRule drule=r.getDNFGuardExpr();
428 for(int i=0;i<drule.size();i++) {
429 RuleConjunction rconj=drule.get(i);
430 for(int j=0;j<rconj.size();j++) {
431 DNFExpr dexpr=rconj.get(j);
432 Expr expr=dexpr.getExpr();
433 boolean negated=dexpr.getNegation();
441 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
442 if (satisfiesrule==satisfyrule) {
443 /* Effect is the one being tested for */
444 /* Only expr's to be concerned with are TupleOfExpr and
446 if (expr.getRequiredDescriptors().contains(des)) {
447 if (((expr instanceof ElementOfExpr)||
448 (expr instanceof TupleOfExpr))&&
449 (expr.getRequiredDescriptors().size()==1))
452 throw new Error("Unrecognized EXPR");