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             if (freevars!=null)
 159                 for(Iterator it=freevars.iterator();it.hasNext();) {
 160                     VarDescriptor vd=(VarDescriptor)it.next();
 161                     if (vd.isGlobal())
 162                         continue; //globals are fine
 163                     else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
 164                         continue;
 165                     else if (termination.maxsize.getsize(vd.getSet())==1)
 166                         continue;
 167                     return false;
 168                 }
 169             return rexpr1.equals(varmap,rexpr2);
 170         }
 171         return false;
 172     }
 173
 174     /** Does performing the AbstractRepair ar falsify the predicate dp */
 175
 176     public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
 177         if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
 178             //      ((ar.getDescriptor() instanceof SetDescriptor)||
 179             // If the second predicate uses the size of the set, modifying the set size could falsify it...
 180             !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
 181             //)
 182             return false;
 183
 184
 185         // If the update changes something in the middle of a size
 186         // expression, it interferes with it.
 187         if ((dp.getPredicate() instanceof ExprPredicate)&&
 188             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
 189             (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
 190             ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
 191             ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
 192             return true;
 193         }
 194
 195         // If the update changes something in the middle of a
 196         // comparison expression, it interferes with it.
 197         if ((dp.getPredicate() instanceof ExprPredicate)&&
 198             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
 199             (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
 200             return true;
 201         }
 202
 203         /* This if handles all the c comparisons in the paper */
 204         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 205             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 206             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 207             (dp.getPredicate() instanceof ExprPredicate)&&
 208             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 209             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 210             boolean neg1=ar.getPredicate().isNegated();
 211             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 212             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 213             boolean neg2=dp.isNegated();
 214             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 215             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 216             op1=Opcode.translateOpcode(neg1,op1);
 217             op2=Opcode.translateOpcode(neg2,op2);
 218
 219             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 220                 int size1a=0;
 221                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 222                     size1a=size1;
 223                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 224                     size1a=size1+1;
 225
 226                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 227                     ((op2==Opcode.NE)&&(size1a!=size2))||
 228                     (op2==Opcode.GE)||
 229                     (op2==Opcode.GT)||
 230                     ((op2==Opcode.LE)&&(size1a<=size2))||
 231                     ((op2==Opcode.LT)&&(size1a<size2)))
 232                     return false;
 233             }
 234         }
 235
 236         /* This if handles all the c comparisons in the paper */
 237         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 238             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 239             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 240             (dp.getPredicate() instanceof ExprPredicate)&&
 241             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 242             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 243             boolean neg1=ar.getPredicate().isNegated();
 244             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 245             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 246             int size2=1;
 247             op1=Opcode.translateOpcode(neg1,op1);
 248
 249             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 250                 int size1a=0;
 251                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 252                     size1a=size1;
 253                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 254                     size1a=size1+1;
 255                 if (size1a==size2)
 256                     return false;
 257             }
 258         }
 259
 260         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 261             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 262             (dp.getPredicate() instanceof ExprPredicate)&&
 263             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 264             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 265             int size1=1;
 266
 267             boolean neg2=dp.isNegated();
 268             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 269             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 270
 271             op2=Opcode.translateOpcode(neg2,op2);
 272
 273             if (((op2==Opcode.EQ)&&(size1==size2))||
 274                 ((op2==Opcode.NE)&&(size1!=size2))||
 275                 ((op2==Opcode.GE)&&(size1>=size2))||
 276                 ((op2==Opcode.GT)&&(size1>size2))||
 277                 ((op2==Opcode.LE)&&(size1<=size2))||
 278                 ((op2==Opcode.LT)&&(size1<size2)))
 279                 return false;
 280         }
 281
 282         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 283             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 284             (dp.getPredicate() instanceof ExprPredicate)&&
 285             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 286             boolean neg2=dp.isNegated();
 287             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 288             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 289
 290             op2=Opcode.translateOpcode(neg2,op2);
 291
 292             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 293
 294             if ((maxsize!=-1)&&
 295                 ((op2==Opcode.LT&&size2>maxsize)||
 296                  (op2==Opcode.LE&&size2>=maxsize)||
 297                  (op2==Opcode.EQ&&size2>=maxsize)))
 298                 return false;
 299
 300             if (((op2==Opcode.NE)&&(size2==0))||
 301                 (op2==Opcode.GE)||
 302                 (op2==Opcode.GT))
 303                 return false;
 304         }
 305
 306
 307         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 308             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 309             (dp.getPredicate() instanceof ExprPredicate)&&
 310             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 311             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 312
 313             boolean neg1=ar.getPredicate().isNegated();
 314             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 315             boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
 316             int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
 317             Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 318
 319
 320             boolean neg2=dp.isNegated();
 321             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 322             boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 323             int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 324             Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 325
 326
 327             /* If the left sides of the comparisons are both from
 328                different sets, the update is orthogonal to the expr dp */
 329             {
 330                 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
 331                 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
 332                 SetDescriptor sd1=lexpr1.getSet();
 333                 SetDescriptor sd2=lexpr2.getSet();
 334                 if (termination.mutuallyexclusive(sd1,sd2))
 335                     return false;
 336             }
 337
 338             /* Translate the opcodes */
 339             op1=Opcode.translateOpcode(neg1,op1);
 340             op2=Opcode.translateOpcode(neg2,op2);
 341
 342             /* Obvious cases which can't interfere */
 343             if (((op1==Opcode.GT)||
 344                 (op1==Opcode.GE))&&
 345                 ((op2==Opcode.GT)||
 346                  (op2==Opcode.GE)))
 347                 return false;
 348             if (((op1==Opcode.LT)||
 349                 (op1==Opcode.LE))&&
 350                 ((op2==Opcode.LT)||
 351                  (op2==Opcode.LE)))
 352                 return false;
 353
 354             if (interferemodifies(ar.getPredicate(),dp))
 355                 return false;
 356
 357             if (isInt1&&isInt2) {
 358                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 359                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 360                     size1==size2)
 361                     return false;
 362                 int size1a=size1;
 363                 int size2a=size2;
 364                 if (op1==Opcode.GT)
 365                     size1a++;
 366                 if (op1==Opcode.LT)
 367                     size1a--;
 368                 if (op1==Opcode.NE)
 369                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 370
 371                 if (op2==Opcode.GT)
 372                     size2a++;
 373                 if (op2==Opcode.LT)
 374                     size2a--;
 375                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 376                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 377                     (size1a<=size2a))
 378                     return false;
 379                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 380                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 381                     (size1a>=size2a))
 382                     return false;
 383                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 384                     (size1a==size2a))
 385                     return false;
 386                 if ((op1==Opcode.EQ)&&
 387                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 388                     (size1a<=size2a))
 389                     return false;
 390                 if ((op1==Opcode.EQ)&&
 391                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 392                     (size1a>=size2a))
 393                     return false;
 394                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 395                     if (size1a!=size2)
 396                         return false;
 397                 if ((op1==Opcode.NE)&&
 398                     (op2==Opcode.EQ)&&
 399                     (size1!=size2))
 400                     return false;
 401                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 402                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 403                     (size1!=size2a))
 404                     return false;
 405                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 406                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 407                     (size1!=size2a))
 408                     return false;
 409             }
 410         }
 411         /* This handles all the c comparisons in the paper */
 412         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 413             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 414             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 415             (dp.getPredicate() instanceof ExprPredicate)&&
 416             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 417             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 418             boolean neg1=ar.getPredicate().isNegated();
 419             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 420             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 421             boolean neg2=dp.isNegated();
 422             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 423             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 424             /* Translate the opcodes */
 425             op1=Opcode.translateOpcode(neg1,op1);
 426             op2=Opcode.translateOpcode(neg2,op2);
 427
 428             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 429                 int size1a=0;
 430
 431                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 432                     size1a=size1;
 433                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 434                     size1a=size1-1;
 435
 436                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 437                     ((op2==Opcode.NE)&&(size1a!=size2))||
 438                     (op2==Opcode.LE)||
 439                     (op2==Opcode.LT)||
 440                     ((op2==Opcode.GE)&&(size1a>=size2))||
 441                     ((op2==Opcode.GT)&&(size1a>size2)))
 442                     return false;
 443             }
 444         }
 445
 446         /* This handles all the c comparisons in the paper */
 447         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 448             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 449             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 450             (dp.getPredicate() instanceof ExprPredicate)&&
 451             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 452             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 453             boolean neg1=ar.getPredicate().isNegated();
 454             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 455             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 456             int size2=1;
 457             /* Translate the opcodes */
 458             op1=Opcode.translateOpcode(neg1,op1);
 459
 460             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 461                 int size1a=0;
 462
 463                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 464                     size1a=size1;
 465                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 466                     size1a=size1-1;
 467
 468                 if (size1a==size2)
 469                     return false;
 470             }
 471         }
 472
 473         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 474             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 475             (dp.getPredicate() instanceof ExprPredicate)&&
 476             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 477             boolean neg2=dp.isNegated();
 478             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 479             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 480             op2=Opcode.translateOpcode(neg2,op2);
 481
 482             if (((op2==Opcode.EQ)&&(size2==0))||
 483                 (op2==Opcode.LE)||
 484                 (op2==Opcode.LT))
 485                 return false;
 486         }
 487         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 488             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 489             (dp.getPredicate() instanceof InclusionPredicate)&&
 490             (dp.isNegated()==false))
 491             return false; /* Could only satisfy this predicate */
 492
 493         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 494             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 495             (dp.getPredicate() instanceof InclusionPredicate)&&
 496             (dp.isNegated()==true))
 497             return false; /* Could only satisfy this predicate */
 498         return true;
 499     }
 500
 501     /** Does the increase (or decrease) in scope of a model defintion
 502      * rule represented by sn falsify the predicate dp. */
 503
 504     public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
 505         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 506             Rule r=sn.getRule();
 507             Set target=r.getInclusion().getTargetDescriptors();
 508             boolean match=false;
 509             for(int i=0;i<r.numQuantifiers();i++) {
 510                 Quantifier q=r.getQuantifier(i);
 511                 if (q instanceof SetQuantifier) {
 512                     SetQuantifier sq=(SetQuantifier) q;
 513                     if (target.contains(sq.getSet())) {
 514                         match=true;
 515                         break;
 516                     }
 517                 }
 518             }
 519             if (match&&
 520                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
 521                 (dp.getPredicate() instanceof ExprPredicate)&&
 522                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 523                 boolean neg=dp.isNegated();
 524                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 525                 int size=((ExprPredicate)dp.getPredicate()).rightSize();
 526                 op=Opcode.translateOpcode(neg,op);
 527
 528                 if ((op==Opcode.GE)&&
 529                     ((size==0)||(size==1)))
 530                     return false;
 531                 if ((op==Opcode.GT)&&
 532                     (size==0))
 533                     return false;
 534             }
 535         }
 536         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 537     }
 538
 539     /** Does increasing (or decreasing if satisfy=false) the size of
 540      * the set or relation des falsify the predicate dp. */
 541
 542     private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 543         if ((des!=dp.getPredicate().getDescriptor()) &&
 544             //((des instanceof SetDescriptor)||
 545             !dp.getPredicate().usesDescriptor(des))//)
 546             return false;
 547
 548         /* This if handles all the c comparisons in the paper */
 549         if (des==dp.getPredicate().getDescriptor()&&
 550             (satisfy)&&
 551             (dp.getPredicate() instanceof ExprPredicate)&&
 552             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 553             boolean neg2=dp.isNegated();
 554             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 555             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 556             op2=Opcode.translateOpcode(neg2,op2);
 557
 558
 559             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 560             {
 561                 if ((maxsize!=-1)&&
 562                     ((op2==Opcode.LT&&size2>maxsize)||
 563                      (op2==Opcode.LE&&size2>=maxsize)||
 564                      (op2==Opcode.EQ&&size2>=maxsize)))
 565                     return false;
 566
 567                 if ((op2==Opcode.GE)||
 568                     (op2==Opcode.GT)||
 569                     (op2==Opcode.NE)&&(size2==0))
 570                     return false;
 571             }
 572         }
 573         /* This if handles all the c comparisons in the paper */
 574         if (des==dp.getPredicate().getDescriptor()&&
 575             (!satisfy)&&
 576             (dp.getPredicate() instanceof ExprPredicate)&&
 577             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 578             boolean neg2=dp.isNegated();
 579             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 580             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 581             op2=Opcode.translateOpcode(neg2,op2);
 582             {
 583                 if (((op2==Opcode.EQ)&&(size2==0))||
 584                     (op2==Opcode.LE)||
 585                     (op2==Opcode.LT))
 586                     return false;
 587             }
 588         }
 589         if ((des==dp.getPredicate().getDescriptor())&&
 590             satisfy&&
 591             (dp.getPredicate() instanceof InclusionPredicate)&&
 592             (dp.isNegated()==false))
 593             return false; /* Could only satisfy this predicate */
 594
 595         if ((des==dp.getPredicate().getDescriptor())&&
 596             (!satisfy)&&
 597             (dp.getPredicate() instanceof InclusionPredicate)&&
 598             (dp.isNegated()==true))
 599             return false; /* Could only satisfy this predicate */
 600
 601         return true;
 602     }
 603
 604     /** This method test whether satisfying (or falsifying depending
 605      * on the flag satisfy) a rule that adds an object(or tuple) to
 606      * the set(or relation) descriptor may increase (or decrease
 607      * depending on the flag satisfyrule) the scope of a constraint or
 608      * model defintion rule r.  */
 609
 610     static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 611         for(int i=0;i<r.numQuantifiers();i++) {
 612             Quantifier q=r.getQuantifier(i);
 613             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 614                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 615                     return true;
 616             } else if (q instanceof ForQuantifier) {
 617                 if (q.getRequiredDescriptors().contains(des))
 618                     return true;
 619             } else throw new Error("Unrecognized Quantifier");
 620         }
 621         return false;
 622     }
 623
 624     static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
 625         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 626             return interferesquantifier(ar.getDescriptor(),true,q,true);
 627         return false;
 628     }
 629
 630     static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
 631         return interferesquantifier(des, satisfy, q,true);
 632     }
 633
 634     static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 635         if (interferesquantifier(des,satisfy,r,satisfyrule))
 636             return true;
 637         /* Scan DNF form */
 638         DNFRule drule=r.getDNFGuardExpr();
 639         for(int i=0;i<drule.size();i++) {
 640             RuleConjunction rconj=drule.get(i);
 641             for(int j=0;j<rconj.size();j++) {
 642                 DNFExpr dexpr=rconj.get(j);
 643                 Expr expr=dexpr.getExpr();
 644                 boolean negated=dexpr.getNegation();
 645                 /*
 646                   satisfy  negated
 647                   Yes      No             Yes
 648                   Yes      Yes            No
 649                   No       No             No
 650                   No       Yes            Yes
 651                 */
 652                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 653                 if (satisfiesrule==satisfyrule) {
 654                     /* Effect is the one being tested for */
 655                     /* Only expr's to be concerned with are TupleOfExpr and
 656                        ElementOfExpr */
 657                     if (expr.getRequiredDescriptors().contains(des)) {
 658                         if (((expr instanceof ElementOfExpr)||
 659                             (expr instanceof TupleOfExpr))&&
 660                             (expr.getRequiredDescriptors().size()==1))
 661                             return true;
 662                         else
 663                             throw new Error("Unrecognized EXPR");
 664                     }
 665                 }
 666             }
 667         }
 668         return false;
 669     }
 670 }