4 class AbstractInterferes {
5 Termination termination;
7 public AbstractInterferes(Termination t) {
12 /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
15 static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
17 boolean mayremove=false;
18 switch (ar.getType()) {
19 case AbstractRepair.ADDTOSET:
20 case AbstractRepair.ADDTORELATION:
21 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
25 case AbstractRepair.REMOVEFROMSET:
26 case AbstractRepair.REMOVEFROMRELATION:
27 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
31 case AbstractRepair.MODIFYRELATION:
32 if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
34 if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
40 throw new Error("Unrecognized Abstract Repair");
44 drule=r.getDNFGuardExpr();
46 drule=r.getDNFNegGuardExpr();
48 for(int i=0;i<drule.size();i++) {
49 RuleConjunction rconj=drule.get(i);
50 for(int j=0;j<rconj.size();j++) {
51 DNFExpr dexpr=rconj.get(j);
52 Expr expr=dexpr.getExpr();
53 if (expr.usesDescriptor(ar.getDescriptor())) {
55 if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
63 /** This method is designed to check that modifying a relation
64 * doesn't violate a relation well-formedness constraint
65 * (ie. [forall <a,b> in R], a in S1 and b in S2; */
67 public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
68 if (c.numQuantifiers()==1&&
69 (c.getQuantifier(0) instanceof RelationQuantifier)) {
70 RelationQuantifier rq=(RelationQuantifier)c.getQuantifier(0);
71 if (rq.getRelation()==ar.getDescriptor()) {
72 Hashtable ht=new Hashtable();
73 if (ar.getDomainSet()!=null)
74 ht.put(rq.x,ar.getDomainSet());
75 if (ar.getRangeSet()!=null)
76 ht.put(rq.y,ar.getRangeSet());
77 DNFConstraint dconst=c.dnfconstraint;
79 for(int i=0;i<dconst.size();i++) {
80 Conjunction conj=dconst.get(i);
82 for(int j=0;j<conj.size();j++) {
83 DNFPredicate dpred=conj.get(j);
84 Predicate p=dpred.getPredicate();
85 if ((p instanceof InclusionPredicate)&&(!dpred.isNegated())) {
86 InclusionPredicate ip=(InclusionPredicate)p;
87 if (ip.expr instanceof VarExpr&&
88 ip.setexpr.getDescriptor() instanceof SetDescriptor) {
89 VarDescriptor vd=((VarExpr)ip.expr).getVar();
90 if (ht.containsKey(vd)) {
91 SetDescriptor td=(SetDescriptor)ip.setexpr.getDescriptor();
92 SetDescriptor s=(SetDescriptor)ht.get(vd);
108 /** Check to see if performing the repair ar on repair_c does not
109 * inferere with interfere_c. Returns true if there is no
112 public boolean interferemodifies(AbstractRepair ar, Constraint repair_c, DNFPredicate interfere_pred, Constraint interfere_c) {
113 DNFConstraint precondition=repair_c.getDNFConstraint().not();
114 if (repair_c.numQuantifiers()!=1||
115 interfere_c.numQuantifiers()!=1||
116 !(repair_c.getQuantifier(0) instanceof SetQuantifier)||
117 !(interfere_c.getQuantifier(0) instanceof SetQuantifier)||
118 ((SetQuantifier)repair_c.getQuantifier(0)).getSet()!=((SetQuantifier)interfere_c.getQuantifier(0)).getSet())
121 Hashtable mapping=new Hashtable();
122 mapping.put(((SetQuantifier)repair_c.getQuantifier(0)).getVar(),
123 ((SetQuantifier)interfere_c.getQuantifier(0)).getVar());
125 if (ar.getType()!=AbstractRepair.MODIFYRELATION||
126 !(ar.getPredicate().getPredicate() instanceof ExprPredicate)||
127 !(interfere_pred.getPredicate() instanceof ExprPredicate))
129 Expr e=((ExprPredicate)interfere_pred.getPredicate()).expr;
130 Expr leftside=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).left;
131 Set relationset=e.useDescriptor(ar.getDescriptor());
132 for(Iterator relit=relationset.iterator();relit.hasNext();) {
133 Expr e2=(Expr)relit.next();
134 if (!leftside.equals(mapping,e2))
139 /* Prune precondition using any ar's in the same conjunction */
140 adjustcondition(precondition, ar);
141 Conjunction conj=findConjunction(repair_c.getDNFConstraint(),ar.getPredicate());
143 /* We don't interfere with the same constraint, if there
144 aren't any shared state problems between different
145 bindings (which we've already checked for), and its a
146 different conjunction. Because we wouldn't have repair it
147 if it wasn't already broken. Doesn't appear to be needed,
148 the cycle algorithm will just eliminate one of the nodes.
150 if (repair_c==interfere_c) {
151 if (conj!=findConjunction(interfere_c.getDNFConstraint(),interfere_pred))
155 for(int i=0;i<conj.size();i++) {
156 DNFPredicate dp=conj.get(i);
157 Set s=(Set)termination.predtoabstractmap.get(dp);
158 for(Iterator it=s.iterator();it.hasNext();) {
159 GraphNode gn=(GraphNode)it.next();
160 TermNode tn=(TermNode)gn.getOwner();
161 AbstractRepair dp_ar=tn.getAbstract();
162 adjustcondition(precondition, dp_ar);
165 /* We now have precondition after interference */
166 if (precondition.size()==0)
168 DNFConstraint infr_const=interfere_c.getDNFConstraint();
171 for(int i=0;i<infr_const.size();i++) {
172 Conjunction infr_conj=infr_const.get(i);
173 for(int j=0;j<infr_conj.size();j++) {
174 DNFPredicate infr_dp=infr_conj.get(j);
176 for(int i2=0;i2<precondition.size();i2++) {
177 Conjunction pre_conj=precondition.get(i2);
178 for(int j2=0;j2<pre_conj.size();j2++) {
179 DNFPredicate pre_dp=pre_conj.get(j2);
180 if (checkPreEnsures(pre_dp,infr_dp,mapping))
181 continue next_pre_conj;
184 continue next_conj; /* The precondition doesn't ensure this conjunction is true */
187 return true; /*Found a conjunction that must be
188 true...therefore the precondition
189 guarantees that the second constraint is
190 always true after repair*/
195 static private Conjunction findConjunction(DNFConstraint cons, DNFPredicate dp) {
196 for(int i=0;i<cons.size();i++) {
197 Conjunction conj=cons.get(i);
198 for(int j=0;j<conj.size();j++) {
199 DNFPredicate curr_dp=conj.get(j);
204 throw new Error("Not found");
207 /** This method removes predicates that the abstract repair may
210 private void adjustcondition(DNFConstraint precond, AbstractRepair ar) {
211 HashSet conjremove=new HashSet();
212 for(int i=0;i<precond.size();i++) {
213 Conjunction conj=precond.get(i);
214 HashSet toremove=new HashSet();
215 for(int j=0;j<conj.size();j++) {
216 DNFPredicate dp=conj.get(j);
217 if (interfereswithpredicate(ar,dp)) {
218 /* Remove dp from precond */
222 conj.predicates.removeAll(toremove);
224 conjremove.add(conj);
226 precond.conjunctions.removeAll(conjremove);
229 private boolean checkPreEnsures(DNFPredicate pre_dp, DNFPredicate infr_dp, Hashtable mapping) {
230 if (pre_dp.isNegated()==infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
231 (infr_dp.getPredicate() instanceof ExprPredicate)) {
232 if (((ExprPredicate)pre_dp.getPredicate()).expr.equals(mapping, ((ExprPredicate)infr_dp.getPredicate()).expr))
235 if ((!pre_dp.isNegated())&&infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
236 (infr_dp.getPredicate() instanceof ExprPredicate)) {
237 ExprPredicate pre_ep=(ExprPredicate)pre_dp.getPredicate();
238 ExprPredicate infr_ep=(ExprPredicate)infr_dp.getPredicate();
239 if (pre_ep.getType()==ExprPredicate.COMPARISON&&
240 infr_ep.getType()==ExprPredicate.COMPARISON&&
241 pre_ep.isRightInt()&&
242 infr_ep.isRightInt()&&
243 pre_ep.rightSize()!=infr_ep.rightSize()&&
244 pre_ep.getOp()==Opcode.EQ&&
245 infr_ep.getOp()==Opcode.EQ) {
246 if (((OpExpr)pre_ep.expr).left.equals(mapping,((OpExpr)infr_ep.expr).left))
253 /** This method checks whether a modify relation abstract repair
254 * to satisfy ar may violate dp. It returns true if there is no
257 private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
258 boolean neg1=ar.isNegated();
259 Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
260 Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;
261 Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
262 RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
264 boolean neg2=dp.isNegated();
265 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
266 Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
267 Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
269 /* Translate the opcodes */
270 op1=Opcode.translateOpcode(neg1,op1);
271 op2=Opcode.translateOpcode(neg2,op2);
273 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
274 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
275 !rexpr2.usesDescriptor(updated_des)) {
276 Hashtable varmap=new Hashtable();
280 boolean initialrelation=true;
281 boolean onetoone=true;
283 if ((l1 instanceof VarExpr)&&
284 (l2 instanceof VarExpr)) {
285 VarDescriptor vd1=((VarExpr)l1).getVar();
286 VarDescriptor vd2=((VarExpr)l2).getVar();
289 } else if ((l1 instanceof RelationExpr)&&
290 (l2 instanceof RelationExpr)) {
291 RelationExpr re1=(RelationExpr)l1;
292 RelationExpr re2=(RelationExpr)l2;
293 if (re1.getRelation()!=re2.getRelation()||
294 re1.inverted()!=re2.inverted())
297 if (!initialrelation) {
299 ConstraintDependence.rulesensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)||
300 ConstraintDependence.constraintsensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)))
302 //need check one-to-one property here
303 } else initialrelation=false;
306 } else return false; // bad match
308 Set freevars=rexpr1.freeVars();
310 for(Iterator it=freevars.iterator();it.hasNext();) {
311 VarDescriptor vd=(VarDescriptor)it.next();
313 continue; //globals are fine
314 else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
316 else if (termination.maxsize.getsize(vd.getSet())==1)
320 return rexpr1.equals(varmap,rexpr2);
325 /** Returns true if performing the AbstractRepair ar may falsify
328 public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
329 if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
330 // ((ar.getDescriptor() instanceof SetDescriptor)||
331 // If the second predicate uses the size of the set, modifying the set size could falsify it...
332 !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
337 // If the update changes something in the middle of a size
338 // expression, it interferes with it.
339 if ((dp.getPredicate() instanceof ExprPredicate)&&
340 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
341 (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
342 ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
343 ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
347 // If the update changes something in the middle of a
348 // comparison expression, it interferes with it.
349 if ((dp.getPredicate() instanceof ExprPredicate)&&
350 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
351 (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
355 /* This if handles all the c comparisons in the paper */
356 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
357 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
358 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
359 (dp.getPredicate() instanceof ExprPredicate)&&
360 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
361 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
362 boolean neg1=ar.getPredicate().isNegated();
363 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
364 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
365 boolean neg2=dp.isNegated();
366 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
367 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
368 op1=Opcode.translateOpcode(neg1,op1);
369 op2=Opcode.translateOpcode(neg2,op2);
371 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
373 if((op1==Opcode.EQ)||(op1==Opcode.GE))
375 if((op1==Opcode.GT)||(op1==Opcode.NE))
378 if (((op2==Opcode.EQ)&&(size1a==size2))||
379 ((op2==Opcode.NE)&&(size1a!=size2))||
382 ((op2==Opcode.LE)&&(size1a<=size2))||
383 ((op2==Opcode.LT)&&(size1a<size2)))
388 /* This if handles all the c comparisons in the paper */
389 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
390 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
391 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
392 (dp.getPredicate() instanceof ExprPredicate)&&
393 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
394 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
395 boolean neg1=ar.getPredicate().isNegated();
396 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
397 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
399 op1=Opcode.translateOpcode(neg1,op1);
401 if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
403 if((op1==Opcode.EQ)||(op1==Opcode.GE))
405 if((op1==Opcode.GT)||(op1==Opcode.NE))
412 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
413 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
414 (dp.getPredicate() instanceof ExprPredicate)&&
415 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
416 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
419 boolean neg2=dp.isNegated();
420 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
421 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
423 op2=Opcode.translateOpcode(neg2,op2);
425 if (((op2==Opcode.EQ)&&(size1==size2))||
426 ((op2==Opcode.NE)&&(size1!=size2))||
427 ((op2==Opcode.GE)&&(size1>=size2))||
428 ((op2==Opcode.GT)&&(size1>size2))||
429 ((op2==Opcode.LE)&&(size1<=size2))||
430 ((op2==Opcode.LT)&&(size1<size2)))
434 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
435 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
436 (dp.getPredicate() instanceof ExprPredicate)&&
437 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
438 boolean neg2=dp.isNegated();
439 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
440 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
442 op2=Opcode.translateOpcode(neg2,op2);
444 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
447 ((op2==Opcode.LT&&size2>maxsize)||
448 (op2==Opcode.LE&&size2>=maxsize)||
449 (op2==Opcode.EQ&&size2>=maxsize)))
452 if (((op2==Opcode.NE)&&(size2==0))||
459 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
460 (ar.getType()==AbstractRepair.MODIFYRELATION)&&
461 (dp.getPredicate() instanceof ExprPredicate)&&
462 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
463 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
465 boolean neg1=ar.getPredicate().isNegated();
466 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
467 boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
468 int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
469 Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
472 boolean neg2=dp.isNegated();
473 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
474 boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
475 int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
476 Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
479 /* If the left sides of the comparisons are both from
480 different sets, the update is orthogonal to the expr dp */
482 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
483 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
484 SetDescriptor sd1=lexpr1.getSet();
485 SetDescriptor sd2=lexpr2.getSet();
486 if (termination.mutuallyexclusive(sd1,sd2))
490 /* Translate the opcodes */
491 op1=Opcode.translateOpcode(neg1,op1);
492 op2=Opcode.translateOpcode(neg2,op2);
494 /* Obvious cases which can't interfere */
495 if (((op1==Opcode.GT)||
500 if (((op1==Opcode.LT)||
506 if (interferemodifies(ar.getPredicate(),dp))
509 if (isInt1&&isInt2) {
510 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
511 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
521 size1a++; /*FLAGNE this is current behavior for NE repairs */
527 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
528 ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
531 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
532 ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
535 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
538 if ((op1==Opcode.EQ)&&
539 ((op2==Opcode.LE)||(op2==Opcode.LT))&&
542 if ((op1==Opcode.EQ)&&
543 ((op2==Opcode.GE)||(op2==Opcode.GT))&&
546 if (op2==Opcode.NE) /*FLAGNE this is current behavior for NE repairs */
549 if ((op1==Opcode.NE)&&
553 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
554 ((op2==Opcode.GT)||(op2==Opcode.GE))&&
557 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
558 ((op2==Opcode.LT)||(op2==Opcode.LE))&&
563 /* This handles all the c comparisons in the paper */
564 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
565 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
566 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
567 (dp.getPredicate() instanceof ExprPredicate)&&
568 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
569 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
570 boolean neg1=ar.getPredicate().isNegated();
571 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
572 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
573 boolean neg2=dp.isNegated();
574 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
575 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
576 /* Translate the opcodes */
577 op1=Opcode.translateOpcode(neg1,op1);
578 op2=Opcode.translateOpcode(neg2,op2);
580 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
583 if((op1==Opcode.EQ)||(op1==Opcode.LE))
585 if((op1==Opcode.LT)||(op1==Opcode.NE))
588 if (((op2==Opcode.EQ)&&(size1a==size2))||
589 ((op2==Opcode.NE)&&(size1a!=size2))||
592 ((op2==Opcode.GE)&&(size1a>=size2))||
593 ((op2==Opcode.GT)&&(size1a>size2)))
598 /* This handles all the c comparisons in the paper */
599 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
600 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
601 (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
602 (dp.getPredicate() instanceof ExprPredicate)&&
603 (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
604 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
605 boolean neg1=ar.getPredicate().isNegated();
606 Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
607 int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
609 /* Translate the opcodes */
610 op1=Opcode.translateOpcode(neg1,op1);
612 if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
615 if((op1==Opcode.EQ)||(op1==Opcode.LE))
617 if((op1==Opcode.LT)||(op1==Opcode.NE))
625 if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
626 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
627 (dp.getPredicate() instanceof ExprPredicate)&&
628 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
629 boolean neg2=dp.isNegated();
630 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
631 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
632 op2=Opcode.translateOpcode(neg2,op2);
634 if (((op2==Opcode.EQ)&&(size2==0))||
639 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
640 (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
641 (dp.getPredicate() instanceof InclusionPredicate)&&
642 (dp.isNegated()==false))
643 return false; /* Could only satisfy this predicate */
645 if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
646 (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
647 (dp.getPredicate() instanceof InclusionPredicate)&&
648 (dp.isNegated()==true))
649 return false; /* Could only satisfy this predicate */
653 /** Does the increase (or decrease) in scope of a model defintion
654 * rule represented by sn falsify the predicate dp. */
656 public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
657 if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
659 Set target=r.getInclusion().getTargetDescriptors();
661 for(int i=0;i<r.numQuantifiers();i++) {
662 Quantifier q=r.getQuantifier(i);
663 if (q instanceof SetQuantifier) {
664 SetQuantifier sq=(SetQuantifier) q;
665 if (target.contains(sq.getSet())) {
672 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
673 (dp.getPredicate() instanceof ExprPredicate)&&
674 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
675 boolean neg=dp.isNegated();
676 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
677 int size=((ExprPredicate)dp.getPredicate()).rightSize();
678 op=Opcode.translateOpcode(neg,op);
680 if ((op==Opcode.GE)&&
681 ((size==0)||(size==1)))
683 if ((op==Opcode.GT)&&
688 return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
691 /** Does increasing (or decreasing if satisfy=false) the size of
692 * the set or relation des falsify the predicate dp. */
694 private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
695 if ((des!=dp.getPredicate().getDescriptor()) &&
696 //((des instanceof SetDescriptor)||
697 !dp.getPredicate().usesDescriptor(des))//)
700 /* This if handles all the c comparisons in the paper */
701 if (des==dp.getPredicate().getDescriptor()&&
703 (dp.getPredicate() instanceof ExprPredicate)&&
704 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
705 boolean neg2=dp.isNegated();
706 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
707 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
708 op2=Opcode.translateOpcode(neg2,op2);
711 int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
714 ((op2==Opcode.LT&&size2>maxsize)||
715 (op2==Opcode.LE&&size2>=maxsize)||
716 (op2==Opcode.EQ&&size2>=maxsize)))
719 if ((op2==Opcode.GE)||
721 (op2==Opcode.NE)&&(size2==0))
725 /* This if handles all the c comparisons in the paper */
726 if (des==dp.getPredicate().getDescriptor()&&
728 (dp.getPredicate() instanceof ExprPredicate)&&
729 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
730 boolean neg2=dp.isNegated();
731 Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
732 int size2=((ExprPredicate)dp.getPredicate()).rightSize();
733 op2=Opcode.translateOpcode(neg2,op2);
735 if (((op2==Opcode.EQ)&&(size2==0))||
741 if ((des==dp.getPredicate().getDescriptor())&&
743 (dp.getPredicate() instanceof InclusionPredicate)&&
744 (dp.isNegated()==false))
745 return false; /* Could only satisfy this predicate */
747 if ((des==dp.getPredicate().getDescriptor())&&
749 (dp.getPredicate() instanceof InclusionPredicate)&&
750 (dp.isNegated()==true))
751 return false; /* Could only satisfy this predicate */
756 /** This method test whether satisfying (or falsifying depending
757 * on the flag satisfy) a rule that adds an object(or tuple) to
758 * the set(or relation) descriptor may increase (or decrease
759 * depending on the flag satisfyrule) the scope of a constraint or
760 * model defintion rule r. */
762 static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
763 for(int i=0;i<r.numQuantifiers();i++) {
764 Quantifier q=r.getQuantifier(i);
765 if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
766 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
768 } else if (q instanceof ForQuantifier) {
769 if (q.getRequiredDescriptors().contains(des))
771 } else throw new Error("Unrecognized Quantifier");
776 static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
777 if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
778 return interferesquantifier(ar.getDescriptor(),true,q,true);
782 static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
783 return interferesquantifier(des, satisfy, q,true);
786 static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
787 if (interferesquantifier(des,satisfy,r,satisfyrule))
790 DNFRule drule=r.getDNFGuardExpr();
791 for(int i=0;i<drule.size();i++) {
792 RuleConjunction rconj=drule.get(i);
793 for(int j=0;j<rconj.size();j++) {
794 DNFExpr dexpr=rconj.get(j);
795 Expr expr=dexpr.getExpr();
796 boolean negated=dexpr.getNegation();
804 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
805 if (satisfiesrule==satisfyrule) {
806 /* Effect is the one being tested for */
807 /* Only expr's to be concerned with are TupleOfExpr and
809 if (expr.getRequiredDescriptors().contains(des)) {
810 if (((expr instanceof ElementOfExpr)||
811 (expr instanceof TupleOfExpr)))
814 throw new Error("Unrecognized EXPR: "+expr);