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 public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
63 if (c.numQuantifiers()==1&&
64 (c.getQuantifier(0) instanceof RelationQuantifier)) {
65 RelationQuantifier rq=(RelationQuantifier)c.getQuantifier(0);
66 if (rq.getRelation()==ar.getDescriptor()) {
67 Hashtable ht=new Hashtable();
68 if (ar.getDomainSet()!=null)
69 ht.put(rq.x,ar.getDomainSet());
70 if (ar.getRangeSet()!=null)
71 ht.put(rq.y,ar.getRangeSet());
72 DNFConstraint dconst=c.dnfconstraint;
74 for(int i=0;i<dconst.size();i++) {
75 Conjunction conj=dconst.get(i);
77 for(int j=0;j<conj.size();j++) {
78 DNFPredicate dpred=conj.get(j);
79 Predicate p=dpred.getPredicate();
80 if ((p instanceof InclusionPredicate)&&(!dpred.isNegated())) {
81 InclusionPredicate ip=(InclusionPredicate)p;
82 if (ip.expr instanceof VarExpr&&
83 ip.setexpr.getDescriptor() instanceof SetDescriptor) {
84 VarDescriptor vd=((VarExpr)ip.expr).getVar();
85 if (ht.containsKey(vd)) {
86 SetDescriptor td=(SetDescriptor)ip.setexpr.getDescriptor();
87 SetDescriptor s=(SetDescriptor)ht.get(vd);
102 /** Does performing the AbstractRepair ar falsify the predicate dp */
104 public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
105 if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
106 // ((ar.getDescriptor() instanceof SetDescriptor)||
107 // If the second predicate uses the size of the set, modifying the set size could falsify it...
108 !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
112 /* This if handles all the c comparisons in the paper */
113 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
114 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
115 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
116 (dp.getPredicate() instanceof ExprPredicate)&&
117 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
118 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
119 boolean neg1=ar.getPredicate().isNegated();
120 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
121 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
122 boolean neg2=dp.isNegated();
123 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
124 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
125 op1=Opcode.translateOpcode(neg1,op1);
126 op2=Opcode.translateOpcode(neg2,op2);
128 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
130 if((op1==Opcode.EQ)||(op1==Opcode.GE))
132 if((op1==Opcode.GT)||(op1==Opcode.NE))
135 if (((op2==Opcode.EQ)&&(size1a==size2))||
136 ((op2==Opcode.NE)&&(size1a!=size2))||
139 ((op2==Opcode.LE)&&(size1a<=size2))||
140 ((op2==Opcode.LT)&&(size1a<size2)))
144 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
145 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
146 (dp.getPredicate() instanceof ExprPredicate)&&
147 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
148 boolean neg2=dp.isNegated();
149 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
150 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
152 op2=Opcode.translateOpcode(neg2,op2);
154 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
157 ((op2==Opcode.LT&&size2>maxsize)||
158 (op2==Opcode.LE&&size2>=maxsize)||
159 (op2==Opcode.EQ&&size2>=maxsize)))
162 if (((op2==Opcode.NE)&&(size2==0))||
167 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
168 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
169 (dp.getPredicate() instanceof ExprPredicate)&&
170 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
171 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
173 boolean neg1=ar.getPredicate().isNegated();
174 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
175 boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
176 int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
177 Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
180 boolean neg2=dp.isNegated();
181 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
182 boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
183 int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
184 Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
187 /* If the left sides of the comparisons are both from
188 different sets, the update is orthogonal to the expr dp */
190 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
191 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
192 SetDescriptor sd1=lexpr1.getSet();
193 SetDescriptor sd2=lexpr2.getSet();
194 if (termination.mutuallyexclusive(sd1,sd2))
198 /* Translate the opcodes */
199 op1=Opcode.translateOpcode(neg1,op1);
200 op2=Opcode.translateOpcode(neg2,op2);
202 /* Obvious cases which can't interfere */
203 if (((op1==Opcode.GT)||
208 if (((op1==Opcode.LT)||
214 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
215 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
216 expr1.equals(null,expr2)) {
217 // Need to check free variables...
220 if (isInt1&&isInt2) {
221 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
222 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
232 size1a++; /*FLAGNE this is current behavior for NE repairs */
238 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
239 ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
242 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
243 ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
246 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
249 if ((op1==Opcode.EQ)&&
250 ((op2==Opcode.LE)||(op2==Opcode.LT))&&
253 if ((op1==Opcode.EQ)&&
254 ((op2==Opcode.GE)||(op2==Opcode.GT))&&
257 if (op2==Opcode.NE) /*FLAGNE this is current behavior for NE repairs */
260 if ((op1==Opcode.NE)&&
264 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
265 ((op2==Opcode.GT)||(op2==Opcode.GE))&&
268 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
269 ((op2==Opcode.LT)||(op2==Opcode.LE))&&
274 /* This handles all the c comparisons in the paper */
275 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
276 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
277 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
278 (dp.getPredicate() instanceof ExprPredicate)&&
279 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
280 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
281 boolean neg1=ar.getPredicate().isNegated();
282 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
283 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
284 boolean neg2=dp.isNegated();
285 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
286 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
287 /* Translate the opcodes */
288 op1=Opcode.translateOpcode(neg1,op1);
289 op2=Opcode.translateOpcode(neg2,op2);
291 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
294 if((op1==Opcode.EQ)||(op1==Opcode.LE))
296 if((op1==Opcode.LT)||(op1==Opcode.NE))
299 if (((op2==Opcode.EQ)&&(size1a==size2))||
300 ((op2==Opcode.NE)&&(size1a!=size2))||
303 ((op2==Opcode.GE)&&(size1a>=size2))||
304 ((op2==Opcode.GT)&&(size1a>size2)))
309 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
310 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
311 (dp.getPredicate() instanceof ExprPredicate)&&
312 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
313 boolean neg2=dp.isNegated();
314 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
315 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
316 op2=Opcode.translateOpcode(neg2,op2);
318 if (((op2==Opcode.EQ)&&(size2==0))||
323 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
324 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
325 (dp.getPredicate() instanceof InclusionPredicate)&&
326 (dp.isNegated()==false))
327 return false; /* Could only satisfy this predicate */
329 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
330 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
331 (dp.getPredicate() instanceof InclusionPredicate)&&
332 (dp.isNegated()==true))
333 return false; /* Could only satisfy this predicate */
337 /** Does the increase (or decrease) in scope of a model defintion
338 * rule represented by sn falsify the predicate dp. */
340 public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
341 if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
343 Set target=r.getInclusion().getTargetDescriptors();
345 for(int i=0;i<r.numQuantifiers();i++) {
346 Quantifier q=r.getQuantifier(i);
347 if (q instanceof SetQuantifier) {
348 SetQuantifier sq=(SetQuantifier) q;
349 if (target.contains(sq.getSet())) {
356 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
357 (dp.getPredicate() instanceof ExprPredicate)&&
358 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
359 boolean neg=dp.isNegated();
360 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
361 int size=((ExprPredicate)dp.getPredicate()).rightSize();
362 op=Opcode.translateOpcode(neg,op);
364 if ((op==Opcode.GE)&&
365 ((size==0)||(size==1)))
367 if ((op==Opcode.GT)&&
372 return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
375 /** Does increasing (or decreasing if satisfy=false) the size of
376 * the set or relation des falsify the predicate dp. */
378 private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
379 if ((des!=dp.getPredicate().getDescriptor()) &&
380 //((des instanceof SetDescriptor)||
381 !dp.getPredicate().usesDescriptor(des))//)
384 /* This if handles all the c comparisons in the paper */
385 if (des==dp.getPredicate().getDescriptor()&&
387 (dp.getPredicate() instanceof ExprPredicate)&&
388 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
389 boolean neg2=dp.isNegated();
390 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
391 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
392 op2=Opcode.translateOpcode(neg2,op2);
395 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
398 ((op2==Opcode.LT&&size2>maxsize)||
399 (op2==Opcode.LE&&size2>=maxsize)||
400 (op2==Opcode.EQ&&size2>=maxsize)))
403 if ((op2==Opcode.GE)||
405 (op2==Opcode.NE)&&(size2==0))
409 /* This if handles all the c comparisons in the paper */
410 if (des==dp.getPredicate().getDescriptor()&&
412 (dp.getPredicate() instanceof ExprPredicate)&&
413 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
414 boolean neg2=dp.isNegated();
415 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
416 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
417 op2=Opcode.translateOpcode(neg2,op2);
419 if (((op2==Opcode.EQ)&&(size2==0))||
425 if ((des==dp.getPredicate().getDescriptor())&&
427 (dp.getPredicate() instanceof InclusionPredicate)&&
428 (dp.isNegated()==false))
429 return false; /* Could only satisfy this predicate */
431 if ((des==dp.getPredicate().getDescriptor())&&
433 (dp.getPredicate() instanceof InclusionPredicate)&&
434 (dp.isNegated()==true))
435 return false; /* Could only satisfy this predicate */
440 /** This method test whether satisfying (or falsifying depending
441 * on the flag satisfy) a rule that adds an object(or tuple) to
442 * the set(or relation) descriptor may increase (or decrease
443 * depending on the flag satisfyrule) the scope of a constraint or
444 * model defintion rule r. */
446 static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
447 for(int i=0;i<r.numQuantifiers();i++) {
448 Quantifier q=r.getQuantifier(i);
449 if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
450 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
452 } else if (q instanceof ForQuantifier) {
453 if (q.getRequiredDescriptors().contains(des))
455 } else throw new Error("Unrecognized Quantifier");
460 static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
461 if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
462 return interferesquantifier(ar.getDescriptor(),true,q,true);
466 static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
467 return interferesquantifier(des, satisfy, q,true);
470 static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
471 if (interferesquantifier(des,satisfy,r,satisfyrule))
474 DNFRule drule=r.getDNFGuardExpr();
475 for(int i=0;i<drule.size();i++) {
476 RuleConjunction rconj=drule.get(i);
477 for(int j=0;j<rconj.size();j++) {
478 DNFExpr dexpr=rconj.get(j);
479 Expr expr=dexpr.getExpr();
480 boolean negated=dexpr.getNegation();
488 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
489 if (satisfiesrule==satisfyrule) {
490 /* Effect is the one being tested for */
491 /* Only expr's to be concerned with are TupleOfExpr and
493 if (expr.getRequiredDescriptors().contains(des)) {
494 if (((expr instanceof ElementOfExpr)||
495 (expr instanceof TupleOfExpr))&&
496 (expr.getRequiredDescriptors().size()==1))
499 throw new Error("Unrecognized EXPR");