Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

   1 package MCC.IR;
   2 import java.util.*;
   3
   4 class AbstractInterferes {
   5     Termination termination;
   6
   7     public AbstractInterferes(Termination t) {
   8         termination=t;
   9     }
  10
  11     /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
  12      * Rule r. */
  13
  14     static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
  15         boolean mayadd=false;
  16         boolean mayremove=false;
  17         switch (ar.getType()) {
  18         case AbstractRepair.ADDTOSET:
  19         case AbstractRepair.ADDTORELATION:
  20             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  21                 return true;
  22             mayadd=true;
  23             break;
  24         case AbstractRepair.REMOVEFROMSET:
  25         case AbstractRepair.REMOVEFROMRELATION:
  26             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  27                 return true;
  28             mayremove=true;
  29             break;
  30         case AbstractRepair.MODIFYRELATION:
  31             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  32                 return true;
  33             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  34                 return true;
  35             mayadd=true;
  36             mayremove=true;
  37         break;
  38         default:
  39             throw new Error("Unrecognized Abstract Repair");
  40         }
  41         DNFRule drule=null;
  42         if (satisfy)
  43             drule=r.getDNFGuardExpr();
  44         else
  45             drule=r.getDNFNegGuardExpr();
  46
  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())) {
  53                     /* Need to check */
  54                     if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
  55                         return true;
  56                 }
  57             }
  58         }
  59         return false;
  60     }
  61
  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;
  73             conjloop:
  74                 for(int i=0;i<dconst.size();i++) {
  75                     Conjunction conj=dconst.get(i);
  76                 predloop:
  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);
  88                                     if (td.isSubset(s))
  89                                         continue predloop;
  90                                 }
  91                             }
  92                         }
  93                         continue conjloop;
  94                     }
  95                     return true;
  96                 }
  97             }
  98         }
  99         return false;
 100     }
 101
 102     /** This method checks whether a modify relation abstract repair
 103      * to satisfy ar may violate dp.  It returns true if there is no
 104      * interference. */
 105
 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();
 112
 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;
 117
 118         /* Translate the opcodes */
 119         op1=Opcode.translateOpcode(neg1,op1);
 120         op2=Opcode.translateOpcode(neg2,op2);
 121
 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();
 126             Expr l1=lexpr1;
 127             Expr l2=lexpr2;
 128
 129             boolean initialrelation=true;
 130             boolean onetoone=true;
 131             while(true) {
 132                 if ((l1 instanceof VarExpr)&&
 133                     (l2 instanceof VarExpr)) {
 134                     VarDescriptor vd1=((VarExpr)l1).getVar();
 135                     VarDescriptor vd2=((VarExpr)l2).getVar();
 136                     varmap.put(vd1,vd2);
 137                     break;
 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())
 144                         return false;
 145
 146                     if (!initialrelation) {
 147                         if (!(
 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)))
 150                             onetoone=false;
 151                         //need check one-to-one property here
 152                     } else initialrelation=false;
 153                     l1=re1.getExpr();
 154                     l2=re2.getExpr();
 155                 } else return false; // bad match
 156             }
 157             Set freevars=rexpr1.freeVars();
 158             for(Iterator it=freevars.iterator();it.hasNext();) {
 159                 VarDescriptor vd=(VarDescriptor)it.next();
 160                 if (vd.isGlobal())
 161                     continue; //globals are fine
 162                 else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
 163                     continue;
 164                 else if (termination.maxsize.getsize(vd.getSet())==1)
 165                     continue;
 166                 return false;
 167             }
 168             return rexpr1.equals(varmap,rexpr2);
 169         }
 170         return false;
 171     }
 172
 173     /** Does performing the AbstractRepair ar falsify the predicate dp */
 174
 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()))
 180             //)
 181             return false;
 182
 183
 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())) {
 191             return true;
 192         }
 193
 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()))) {
 199             return true;
 200         }
 201
 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);
 217
 218             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 219                 int size1a=0;
 220                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 221                     size1a=size1;
 222                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 223                     size1a=size1+1;
 224
 225                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 226                     ((op2==Opcode.NE)&&(size1a!=size2))||
 227                     (op2==Opcode.GE)||
 228                     (op2==Opcode.GT)||
 229                     ((op2==Opcode.LE)&&(size1a<=size2))||
 230                     ((op2==Opcode.LT)&&(size1a<size2)))
 231                     return false;
 232             }
 233         }
 234
 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();
 245             int size2=1;
 246             op1=Opcode.translateOpcode(neg1,op1);
 247
 248             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 249                 int size1a=0;
 250                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 251                     size1a=size1;
 252                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 253                     size1a=size1+1;
 254                 if (size1a==size2)
 255                     return false;
 256             }
 257         }
 258
 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)) {
 264             int size1=1;
 265
 266             boolean neg2=dp.isNegated();
 267             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 268             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 269
 270             op2=Opcode.translateOpcode(neg2,op2);
 271
 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)))
 278                 return false;
 279         }
 280
 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();
 288
 289             op2=Opcode.translateOpcode(neg2,op2);
 290
 291             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 292
 293             if ((maxsize!=-1)&&
 294                 ((op2==Opcode.LT&&size2>maxsize)||
 295                  (op2==Opcode.LE&&size2>=maxsize)||
 296                  (op2==Opcode.EQ&&size2>=maxsize)))
 297                 return false;
 298
 299             if (((op2==Opcode.NE)&&(size2==0))||
 300                 (op2==Opcode.GE)||
 301                 (op2==Opcode.GT))
 302                 return false;
 303         }
 304
 305
 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)) {
 311
 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;
 317
 318
 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;
 324
 325
 326             /* If the left sides of the comparisons are both from
 327                different sets, the update is orthogonal to the expr dp */
 328             {
 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))
 334                     return false;
 335             }
 336
 337             /* Translate the opcodes */
 338             op1=Opcode.translateOpcode(neg1,op1);
 339             op2=Opcode.translateOpcode(neg2,op2);
 340
 341             /* Obvious cases which can't interfere */
 342             if (((op1==Opcode.GT)||
 343                 (op1==Opcode.GE))&&
 344                 ((op2==Opcode.GT)||
 345                  (op2==Opcode.GE)))
 346                 return false;
 347             if (((op1==Opcode.LT)||
 348                 (op1==Opcode.LE))&&
 349                 ((op2==Opcode.LT)||
 350                  (op2==Opcode.LE)))
 351                 return false;
 352
 353             if (interferemodifies(ar.getPredicate(),dp))
 354                 return false;
 355
 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))&&
 359                     size1==size2)
 360                     return false;
 361                 int size1a=size1;
 362                 int size2a=size2;
 363                 if (op1==Opcode.GT)
 364                     size1a++;
 365                 if (op1==Opcode.LT)
 366                     size1a--;
 367                 if (op1==Opcode.NE)
 368                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 369
 370                 if (op2==Opcode.GT)
 371                     size2a++;
 372                 if (op2==Opcode.LT)
 373                     size2a--;
 374                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 375                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 376                     (size1a<=size2a))
 377                     return false;
 378                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 379                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 380                     (size1a>=size2a))
 381                     return false;
 382                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 383                     (size1a==size2a))
 384                     return false;
 385                 if ((op1==Opcode.EQ)&&
 386                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 387                     (size1a<=size2a))
 388                     return false;
 389                 if ((op1==Opcode.EQ)&&
 390                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 391                     (size1a>=size2a))
 392                     return false;
 393                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 394                     if (size1a!=size2)
 395                         return false;
 396                 if ((op1==Opcode.NE)&&
 397                     (op2==Opcode.EQ)&&
 398                     (size1!=size2))
 399                     return false;
 400                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 401                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 402                     (size1!=size2a))
 403                     return false;
 404                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 405                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 406                     (size1!=size2a))
 407                     return false;
 408             }
 409         }
 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);
 426
 427             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 428                 int size1a=0;
 429
 430                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 431                     size1a=size1;
 432                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 433                     size1a=size1-1;
 434
 435                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 436                     ((op2==Opcode.NE)&&(size1a!=size2))||
 437                     (op2==Opcode.LE)||
 438                     (op2==Opcode.LT)||
 439                     ((op2==Opcode.GE)&&(size1a>=size2))||
 440                     ((op2==Opcode.GT)&&(size1a>size2)))
 441                     return false;
 442             }
 443         }
 444
 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();
 455             int size2=1;
 456             /* Translate the opcodes */
 457             op1=Opcode.translateOpcode(neg1,op1);
 458
 459             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 460                 int size1a=0;
 461
 462                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 463                     size1a=size1;
 464                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 465                     size1a=size1-1;
 466
 467                 if (size1a==size2)
 468                     return false;
 469             }
 470         }
 471
 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);
 480
 481             if (((op2==Opcode.EQ)&&(size2==0))||
 482                 (op2==Opcode.LE)||
 483                 (op2==Opcode.LT))
 484                 return false;
 485         }
 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 */
 491
 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 */
 497         return true;
 498     }
 499
 500     /** Does the increase (or decrease) in scope of a model defintion
 501      * rule represented by sn falsify the predicate dp. */
 502
 503     public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
 504         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 505             Rule r=sn.getRule();
 506             Set target=r.getInclusion().getTargetDescriptors();
 507             boolean match=false;
 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())) {
 513                         match=true;
 514                         break;
 515                     }
 516                 }
 517             }
 518             if (match&&
 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);
 526
 527                 if ((op==Opcode.GE)&&
 528                     ((size==0)||(size==1)))
 529                     return false;
 530                 if ((op==Opcode.GT)&&
 531                     (size==0))
 532                     return false;
 533             }
 534         }
 535         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 536     }
 537
 538     /** Does increasing (or decreasing if satisfy=false) the size of
 539      * the set or relation des falsify the predicate dp. */
 540
 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))//)
 545             return false;
 546
 547         /* This if handles all the c comparisons in the paper */
 548         if (des==dp.getPredicate().getDescriptor()&&
 549             (satisfy)&&
 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);
 556
 557
 558             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 559             {
 560                 if ((maxsize!=-1)&&
 561                     ((op2==Opcode.LT&&size2>maxsize)||
 562                      (op2==Opcode.LE&&size2>=maxsize)||
 563                      (op2==Opcode.EQ&&size2>=maxsize)))
 564                     return false;
 565
 566                 if ((op2==Opcode.GE)||
 567                     (op2==Opcode.GT)||
 568                     (op2==Opcode.NE)&&(size2==0))
 569                     return false;
 570             }
 571         }
 572         /* This if handles all the c comparisons in the paper */
 573         if (des==dp.getPredicate().getDescriptor()&&
 574             (!satisfy)&&
 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);
 581             {
 582                 if (((op2==Opcode.EQ)&&(size2==0))||
 583                     (op2==Opcode.LE)||
 584                     (op2==Opcode.LT))
 585                     return false;
 586             }
 587         }
 588         if ((des==dp.getPredicate().getDescriptor())&&
 589             satisfy&&
 590             (dp.getPredicate() instanceof InclusionPredicate)&&
 591             (dp.isNegated()==false))
 592             return false; /* Could only satisfy this predicate */
 593
 594         if ((des==dp.getPredicate().getDescriptor())&&
 595             (!satisfy)&&
 596             (dp.getPredicate() instanceof InclusionPredicate)&&
 597             (dp.isNegated()==true))
 598             return false; /* Could only satisfy this predicate */
 599
 600         return true;
 601     }
 602
 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.  */
 608
 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))
 614                     return true;
 615             } else if (q instanceof ForQuantifier) {
 616                 if (q.getRequiredDescriptors().contains(des))
 617                     return true;
 618             } else throw new Error("Unrecognized Quantifier");
 619         }
 620         return false;
 621     }
 622
 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);
 626         return false;
 627     }
 628
 629     static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
 630         return interferesquantifier(des, satisfy, q,true);
 631     }
 632
 633     static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 634         if (interferesquantifier(des,satisfy,r,satisfyrule))
 635             return true;
 636         /* Scan DNF form */
 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();
 644                 /*
 645                   satisfy  negated
 646                   Yes      No             Yes
 647                   Yes      Yes            No
 648                   No       No             No
 649                   No       Yes            Yes
 650                 */
 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
 655                        ElementOfExpr */
 656                     if (expr.getRequiredDescriptors().contains(des)) {
 657                         if (((expr instanceof ElementOfExpr)||
 658                             (expr instanceof TupleOfExpr))&&
 659                             (expr.getRequiredDescriptors().size()==1))
 660                             return true;
 661                         else
 662                             throw new Error("Unrecognized EXPR");
 663                     }
 664                 }
 665             }
 666         }
 667         return false;
 668     }
 669 }