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 /** This method checks whether a modify relation abstract repair
103 * to satisfy ar may violate dp. It returns true if there is no
106 private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
107 boolean neg1=ar.isNegated();
108 Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
109 Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;
110 Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
111 RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
113 boolean neg2=dp.isNegated();
114 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
115 Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
116 Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
118 /* Translate the opcodes */
119 op1=Opcode.translateOpcode(neg1,op1);
120 op2=Opcode.translateOpcode(neg2,op2);
122 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
123 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
124 !rexpr2.usesDescriptor(updated_des)) {
125 Hashtable varmap=new Hashtable();
129 boolean initialrelation=true;
130 boolean onetoone=true;
132 if ((l1 instanceof VarExpr)&&
133 (l2 instanceof VarExpr)) {
134 VarDescriptor vd1=((VarExpr)l1).getVar();
135 VarDescriptor vd2=((VarExpr)l2).getVar();
138 } else if ((l1 instanceof RelationExpr)&&
139 (l2 instanceof RelationExpr)) {
140 RelationExpr re1=(RelationExpr)l1;
141 RelationExpr re2=(RelationExpr)l2;
142 if (re1.getRelation()!=re2.getRelation()||
143 re1.inverted()!=re2.inverted())
146 if (!initialrelation) {
148 ConstraintDependence.rulesensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)||
149 ConstraintDependence.constraintsensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)))
151 //need check one-to-one property here
152 } else initialrelation=false;
155 } else return false; // bad match
157 Set freevars=rexpr1.freeVars();
158 for(Iterator it=freevars.iterator();it.hasNext();) {
159 VarDescriptor vd=(VarDescriptor)it.next();
161 continue; //globals are fine
162 else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
164 else if (termination.maxsize.getsize(vd.getSet())==1)
168 return rexpr1.equals(varmap,rexpr2);
173 /** Does performing the AbstractRepair ar falsify the predicate dp */
175 public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
176 if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
177 // ((ar.getDescriptor() instanceof SetDescriptor)||
178 // If the second predicate uses the size of the set, modifying the set size could falsify it...
179 !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
184 // If the update changes something in the middle of a size
185 // expression, it interferes with it.
186 if ((dp.getPredicate() instanceof ExprPredicate)&&
187 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
188 (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
189 ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
190 ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
194 // If the update changes something in the middle of a
195 // comparison expression, it interferes with it.
196 if ((dp.getPredicate() instanceof ExprPredicate)&&
197 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
198 (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
202 /* This if handles all the c comparisons in the paper */
203 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
204 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
205 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
206 (dp.getPredicate() instanceof ExprPredicate)&&
207 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
208 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
209 boolean neg1=ar.getPredicate().isNegated();
210 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
211 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
212 boolean neg2=dp.isNegated();
213 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
214 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
215 op1=Opcode.translateOpcode(neg1,op1);
216 op2=Opcode.translateOpcode(neg2,op2);
218 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
220 if((op1==Opcode.EQ)||(op1==Opcode.GE))
222 if((op1==Opcode.GT)||(op1==Opcode.NE))
225 if (((op2==Opcode.EQ)&&(size1a==size2))||
226 ((op2==Opcode.NE)&&(size1a!=size2))||
229 ((op2==Opcode.LE)&&(size1a<=size2))||
230 ((op2==Opcode.LT)&&(size1a<size2)))
235 /* This if handles all the c comparisons in the paper */
236 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
237 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
238 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
239 (dp.getPredicate() instanceof ExprPredicate)&&
240 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
241 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
242 boolean neg1=ar.getPredicate().isNegated();
243 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
244 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
246 op1=Opcode.translateOpcode(neg1,op1);
248 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
250 if((op1==Opcode.EQ)||(op1==Opcode.GE))
252 if((op1==Opcode.GT)||(op1==Opcode.NE))
259 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
260 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
261 (dp.getPredicate() instanceof ExprPredicate)&&
262 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
263 (((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();
270 op2=Opcode.translateOpcode(neg2,op2);
272 if (((op2==Opcode.EQ)&&(size1==size2))||
273 ((op2==Opcode.NE)&&(size1!=size2))||
274 ((op2==Opcode.GE)&&(size1>=size2))||
275 ((op2==Opcode.GT)&&(size1>size2))||
276 ((op2==Opcode.LE)&&(size1<=size2))||
277 ((op2==Opcode.LT)&&(size1<size2)))
281 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
282 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
283 (dp.getPredicate() instanceof ExprPredicate)&&
284 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
285 boolean neg2=dp.isNegated();
286 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
287 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
289 op2=Opcode.translateOpcode(neg2,op2);
291 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
294 ((op2==Opcode.LT&&size2>maxsize)||
295 (op2==Opcode.LE&&size2>=maxsize)||
296 (op2==Opcode.EQ&&size2>=maxsize)))
299 if (((op2==Opcode.NE)&&(size2==0))||
306 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
307 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
308 (dp.getPredicate() instanceof ExprPredicate)&&
309 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
310 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
312 boolean neg1=ar.getPredicate().isNegated();
313 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
314 boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
315 int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
316 Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
319 boolean neg2=dp.isNegated();
320 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
321 boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
322 int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
323 Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
326 /* If the left sides of the comparisons are both from
327 different sets, the update is orthogonal to the expr dp */
329 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
330 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
331 SetDescriptor sd1=lexpr1.getSet();
332 SetDescriptor sd2=lexpr2.getSet();
333 if (termination.mutuallyexclusive(sd1,sd2))
337 /* Translate the opcodes */
338 op1=Opcode.translateOpcode(neg1,op1);
339 op2=Opcode.translateOpcode(neg2,op2);
341 /* Obvious cases which can't interfere */
342 if (((op1==Opcode.GT)||
347 if (((op1==Opcode.LT)||
353 if (interferemodifies(ar.getPredicate(),dp))
356 if (isInt1&&isInt2) {
357 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
358 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
368 size1a++; /*FLAGNE this is current behavior for NE repairs */
374 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
375 ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
378 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
379 ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
382 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
385 if ((op1==Opcode.EQ)&&
386 ((op2==Opcode.LE)||(op2==Opcode.LT))&&
389 if ((op1==Opcode.EQ)&&
390 ((op2==Opcode.GE)||(op2==Opcode.GT))&&
393 if (op2==Opcode.NE) /*FLAGNE this is current behavior for NE repairs */
396 if ((op1==Opcode.NE)&&
400 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
401 ((op2==Opcode.GT)||(op2==Opcode.GE))&&
404 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
405 ((op2==Opcode.LT)||(op2==Opcode.LE))&&
410 /* This handles all the c comparisons in the paper */
411 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
412 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
413 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
414 (dp.getPredicate() instanceof ExprPredicate)&&
415 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
416 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
417 boolean neg1=ar.getPredicate().isNegated();
418 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
419 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
420 boolean neg2=dp.isNegated();
421 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
422 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
423 /* Translate the opcodes */
424 op1=Opcode.translateOpcode(neg1,op1);
425 op2=Opcode.translateOpcode(neg2,op2);
427 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
430 if((op1==Opcode.EQ)||(op1==Opcode.LE))
432 if((op1==Opcode.LT)||(op1==Opcode.NE))
435 if (((op2==Opcode.EQ)&&(size1a==size2))||
436 ((op2==Opcode.NE)&&(size1a!=size2))||
439 ((op2==Opcode.GE)&&(size1a>=size2))||
440 ((op2==Opcode.GT)&&(size1a>size2)))
445 /* This handles all the c comparisons in the paper */
446 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
447 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
448 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
449 (dp.getPredicate() instanceof ExprPredicate)&&
450 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
451 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
452 boolean neg1=ar.getPredicate().isNegated();
453 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
454 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
456 /* Translate the opcodes */
457 op1=Opcode.translateOpcode(neg1,op1);
459 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
462 if((op1==Opcode.EQ)||(op1==Opcode.LE))
464 if((op1==Opcode.LT)||(op1==Opcode.NE))
472 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
473 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
474 (dp.getPredicate() instanceof ExprPredicate)&&
475 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
476 boolean neg2=dp.isNegated();
477 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
478 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
479 op2=Opcode.translateOpcode(neg2,op2);
481 if (((op2==Opcode.EQ)&&(size2==0))||
486 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
487 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
488 (dp.getPredicate() instanceof InclusionPredicate)&&
489 (dp.isNegated()==false))
490 return false; /* Could only satisfy this predicate */
492 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
493 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
494 (dp.getPredicate() instanceof InclusionPredicate)&&
495 (dp.isNegated()==true))
496 return false; /* Could only satisfy this predicate */
500 /** Does the increase (or decrease) in scope of a model defintion
501 * rule represented by sn falsify the predicate dp. */
503 public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
504 if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
506 Set target=r.getInclusion().getTargetDescriptors();
508 for(int i=0;i<r.numQuantifiers();i++) {
509 Quantifier q=r.getQuantifier(i);
510 if (q instanceof SetQuantifier) {
511 SetQuantifier sq=(SetQuantifier) q;
512 if (target.contains(sq.getSet())) {
519 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
520 (dp.getPredicate() instanceof ExprPredicate)&&
521 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
522 boolean neg=dp.isNegated();
523 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
524 int size=((ExprPredicate)dp.getPredicate()).rightSize();
525 op=Opcode.translateOpcode(neg,op);
527 if ((op==Opcode.GE)&&
528 ((size==0)||(size==1)))
530 if ((op==Opcode.GT)&&
535 return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
538 /** Does increasing (or decreasing if satisfy=false) the size of
539 * the set or relation des falsify the predicate dp. */
541 private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
542 if ((des!=dp.getPredicate().getDescriptor()) &&
543 //((des instanceof SetDescriptor)||
544 !dp.getPredicate().usesDescriptor(des))//)
547 /* This if handles all the c comparisons in the paper */
548 if (des==dp.getPredicate().getDescriptor()&&
550 (dp.getPredicate() instanceof ExprPredicate)&&
551 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
552 boolean neg2=dp.isNegated();
553 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
554 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
555 op2=Opcode.translateOpcode(neg2,op2);
558 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
561 ((op2==Opcode.LT&&size2>maxsize)||
562 (op2==Opcode.LE&&size2>=maxsize)||
563 (op2==Opcode.EQ&&size2>=maxsize)))
566 if ((op2==Opcode.GE)||
568 (op2==Opcode.NE)&&(size2==0))
572 /* This if handles all the c comparisons in the paper */
573 if (des==dp.getPredicate().getDescriptor()&&
575 (dp.getPredicate() instanceof ExprPredicate)&&
576 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
577 boolean neg2=dp.isNegated();
578 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
579 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
580 op2=Opcode.translateOpcode(neg2,op2);
582 if (((op2==Opcode.EQ)&&(size2==0))||
588 if ((des==dp.getPredicate().getDescriptor())&&
590 (dp.getPredicate() instanceof InclusionPredicate)&&
591 (dp.isNegated()==false))
592 return false; /* Could only satisfy this predicate */
594 if ((des==dp.getPredicate().getDescriptor())&&
596 (dp.getPredicate() instanceof InclusionPredicate)&&
597 (dp.isNegated()==true))
598 return false; /* Could only satisfy this predicate */
603 /** This method test whether satisfying (or falsifying depending
604 * on the flag satisfy) a rule that adds an object(or tuple) to
605 * the set(or relation) descriptor may increase (or decrease
606 * depending on the flag satisfyrule) the scope of a constraint or
607 * model defintion rule r. */
609 static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
610 for(int i=0;i<r.numQuantifiers();i++) {
611 Quantifier q=r.getQuantifier(i);
612 if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
613 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
615 } else if (q instanceof ForQuantifier) {
616 if (q.getRequiredDescriptors().contains(des))
618 } else throw new Error("Unrecognized Quantifier");
623 static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
624 if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
625 return interferesquantifier(ar.getDescriptor(),true,q,true);
629 static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
630 return interferesquantifier(des, satisfy, q,true);
633 static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
634 if (interferesquantifier(des,satisfy,r,satisfyrule))
637 DNFRule drule=r.getDNFGuardExpr();
638 for(int i=0;i<drule.size();i++) {
639 RuleConjunction rconj=drule.get(i);
640 for(int j=0;j<rconj.size();j++) {
641 DNFExpr dexpr=rconj.get(j);
642 Expr expr=dexpr.getExpr();
643 boolean negated=dexpr.getNegation();
651 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
652 if (satisfiesrule==satisfyrule) {
653 /* Effect is the one being tested for */
654 /* Only expr's to be concerned with are TupleOfExpr and
656 if (expr.getRequiredDescriptors().contains(des)) {
657 if (((expr instanceof ElementOfExpr)||
658 (expr instanceof TupleOfExpr))&&
659 (expr.getRequiredDescriptors().size()==1))
662 throw new Error("Unrecognized EXPR");