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         /* This if handles all the c comparisons in the paper */
 184         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 185             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 186             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 187             (dp.getPredicate() instanceof ExprPredicate)&&
 188             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 189             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 190             boolean neg1=ar.getPredicate().isNegated();
 191             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 192             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 193             boolean neg2=dp.isNegated();
 194             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 195             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 196             op1=Opcode.translateOpcode(neg1,op1);
 197             op2=Opcode.translateOpcode(neg2,op2);
 198
 199             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 200                 int size1a=0;
 201                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 202                     size1a=size1;
 203                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 204                     size1a=size1+1;
 205
 206                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 207                     ((op2==Opcode.NE)&&(size1a!=size2))||
 208                     (op2==Opcode.GE)||
 209                     (op2==Opcode.GT)||
 210                     ((op2==Opcode.LE)&&(size1a<=size2))||
 211                     ((op2==Opcode.LT)&&(size1a<size2)))
 212                     return false;
 213             }
 214         }
 215         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 216             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 217             (dp.getPredicate() instanceof ExprPredicate)&&
 218             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 219             boolean neg2=dp.isNegated();
 220             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 221             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 222
 223             op2=Opcode.translateOpcode(neg2,op2);
 224
 225             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 226
 227             if ((maxsize!=-1)&&
 228                 ((op2==Opcode.LT&&size2>maxsize)||
 229                  (op2==Opcode.LE&&size2>=maxsize)||
 230                  (op2==Opcode.EQ&&size2>=maxsize)))
 231                 return false;
 232
 233             if (((op2==Opcode.NE)&&(size2==0))||
 234                 (op2==Opcode.GE)||
 235                 (op2==Opcode.GT))
 236                 return false;
 237         }
 238         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 239             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 240             (dp.getPredicate() instanceof ExprPredicate)&&
 241             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 242             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 243
 244             boolean neg1=ar.getPredicate().isNegated();
 245             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 246             boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
 247             int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
 248             Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 249
 250
 251             boolean neg2=dp.isNegated();
 252             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 253             boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 254             int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 255             Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 256
 257
 258             /* If the left sides of the comparisons are both from
 259                different sets, the update is orthogonal to the expr dp */
 260             {
 261                 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
 262                 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
 263                 SetDescriptor sd1=lexpr1.getSet();
 264                 SetDescriptor sd2=lexpr2.getSet();
 265                 if (termination.mutuallyexclusive(sd1,sd2))
 266                     return false;
 267             }
 268
 269             /* Translate the opcodes */
 270             op1=Opcode.translateOpcode(neg1,op1);
 271             op2=Opcode.translateOpcode(neg2,op2);
 272
 273             /* Obvious cases which can't interfere */
 274             if (((op1==Opcode.GT)||
 275                 (op1==Opcode.GE))&&
 276                 ((op2==Opcode.GT)||
 277                  (op2==Opcode.GE)))
 278                 return false;
 279             if (((op1==Opcode.LT)||
 280                 (op1==Opcode.LE))&&
 281                 ((op2==Opcode.LT)||
 282                  (op2==Opcode.LE)))
 283                 return false;
 284
 285             if (interferemodifies(ar.getPredicate(),dp))
 286                 return false;
 287
 288             if (isInt1&&isInt2) {
 289                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 290                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 291                     size1==size2)
 292                     return false;
 293                 int size1a=size1;
 294                 int size2a=size2;
 295                 if (op1==Opcode.GT)
 296                     size1a++;
 297                 if (op1==Opcode.LT)
 298                     size1a--;
 299                 if (op1==Opcode.NE)
 300                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 301
 302                 if (op2==Opcode.GT)
 303                     size2a++;
 304                 if (op2==Opcode.LT)
 305                     size2a--;
 306                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 307                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 308                     (size1a<=size2a))
 309                     return false;
 310                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 311                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 312                     (size1a>=size2a))
 313                     return false;
 314                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 315                     (size1a==size2a))
 316                     return false;
 317                 if ((op1==Opcode.EQ)&&
 318                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 319                     (size1a<=size2a))
 320                     return false;
 321                 if ((op1==Opcode.EQ)&&
 322                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 323                     (size1a>=size2a))
 324                     return false;
 325                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 326                     if (size1a!=size2)
 327                         return false;
 328                 if ((op1==Opcode.NE)&&
 329                     (op2==Opcode.EQ)&&
 330                     (size1!=size2))
 331                     return false;
 332                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 333                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 334                     (size1!=size2a))
 335                     return false;
 336                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 337                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 338                     (size1!=size2a))
 339                     return false;
 340             }
 341         }
 342         /* This handles all the c comparisons in the paper */
 343         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 344             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 345             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 346             (dp.getPredicate() instanceof ExprPredicate)&&
 347             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 348             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 349             boolean neg1=ar.getPredicate().isNegated();
 350             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 351             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 352             boolean neg2=dp.isNegated();
 353             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 354             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 355             /* Translate the opcodes */
 356             op1=Opcode.translateOpcode(neg1,op1);
 357             op2=Opcode.translateOpcode(neg2,op2);
 358
 359             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 360                 int size1a=0;
 361
 362                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 363                     size1a=size1;
 364                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 365                     size1a=size1-1;
 366
 367                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 368                     ((op2==Opcode.NE)&&(size1a!=size2))||
 369                     (op2==Opcode.LE)||
 370                     (op2==Opcode.LT)||
 371                     ((op2==Opcode.GE)&&(size1a>=size2))||
 372                     ((op2==Opcode.GT)&&(size1a>size2)))
 373                     return false;
 374             }
 375         }
 376
 377         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 378             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 379             (dp.getPredicate() instanceof ExprPredicate)&&
 380             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 381             boolean neg2=dp.isNegated();
 382             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 383             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 384             op2=Opcode.translateOpcode(neg2,op2);
 385
 386             if (((op2==Opcode.EQ)&&(size2==0))||
 387                 (op2==Opcode.LE)||
 388                 (op2==Opcode.LT))
 389                 return false;
 390         }
 391         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 392             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 393             (dp.getPredicate() instanceof InclusionPredicate)&&
 394             (dp.isNegated()==false))
 395             return false; /* Could only satisfy this predicate */
 396
 397         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 398             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 399             (dp.getPredicate() instanceof InclusionPredicate)&&
 400             (dp.isNegated()==true))
 401             return false; /* Could only satisfy this predicate */
 402         return true;
 403     }
 404
 405     /** Does the increase (or decrease) in scope of a model defintion
 406      * rule represented by sn falsify the predicate dp. */
 407
 408     public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
 409         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 410             Rule r=sn.getRule();
 411             Set target=r.getInclusion().getTargetDescriptors();
 412             boolean match=false;
 413             for(int i=0;i<r.numQuantifiers();i++) {
 414                 Quantifier q=r.getQuantifier(i);
 415                 if (q instanceof SetQuantifier) {
 416                     SetQuantifier sq=(SetQuantifier) q;
 417                     if (target.contains(sq.getSet())) {
 418                         match=true;
 419                         break;
 420                     }
 421                 }
 422             }
 423             if (match&&
 424                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
 425                 (dp.getPredicate() instanceof ExprPredicate)&&
 426                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 427                 boolean neg=dp.isNegated();
 428                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 429                 int size=((ExprPredicate)dp.getPredicate()).rightSize();
 430                 op=Opcode.translateOpcode(neg,op);
 431
 432                 if ((op==Opcode.GE)&&
 433                     ((size==0)||(size==1)))
 434                     return false;
 435                 if ((op==Opcode.GT)&&
 436                     (size==0))
 437                     return false;
 438             }
 439         }
 440         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 441     }
 442
 443     /** Does increasing (or decreasing if satisfy=false) the size of
 444      * the set or relation des falsify the predicate dp. */
 445
 446     private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 447         if ((des!=dp.getPredicate().getDescriptor()) &&
 448             //((des instanceof SetDescriptor)||
 449             !dp.getPredicate().usesDescriptor(des))//)
 450             return false;
 451
 452         /* This if handles all the c comparisons in the paper */
 453         if (des==dp.getPredicate().getDescriptor()&&
 454             (satisfy)&&
 455             (dp.getPredicate() instanceof ExprPredicate)&&
 456             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 457             boolean neg2=dp.isNegated();
 458             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 459             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 460             op2=Opcode.translateOpcode(neg2,op2);
 461
 462
 463             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 464             {
 465                 if ((maxsize!=-1)&&
 466                     ((op2==Opcode.LT&&size2>maxsize)||
 467                      (op2==Opcode.LE&&size2>=maxsize)||
 468                      (op2==Opcode.EQ&&size2>=maxsize)))
 469                     return false;
 470
 471                 if ((op2==Opcode.GE)||
 472                     (op2==Opcode.GT)||
 473                     (op2==Opcode.NE)&&(size2==0))
 474                     return false;
 475             }
 476         }
 477         /* This if handles all the c comparisons in the paper */
 478         if (des==dp.getPredicate().getDescriptor()&&
 479             (!satisfy)&&
 480             (dp.getPredicate() instanceof ExprPredicate)&&
 481             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 482             boolean neg2=dp.isNegated();
 483             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 484             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 485             op2=Opcode.translateOpcode(neg2,op2);
 486             {
 487                 if (((op2==Opcode.EQ)&&(size2==0))||
 488                     (op2==Opcode.LE)||
 489                     (op2==Opcode.LT))
 490                     return false;
 491             }
 492         }
 493         if ((des==dp.getPredicate().getDescriptor())&&
 494             satisfy&&
 495             (dp.getPredicate() instanceof InclusionPredicate)&&
 496             (dp.isNegated()==false))
 497             return false; /* Could only satisfy this predicate */
 498
 499         if ((des==dp.getPredicate().getDescriptor())&&
 500             (!satisfy)&&
 501             (dp.getPredicate() instanceof InclusionPredicate)&&
 502             (dp.isNegated()==true))
 503             return false; /* Could only satisfy this predicate */
 504
 505         return true;
 506     }
 507
 508     /** This method test whether satisfying (or falsifying depending
 509      * on the flag satisfy) a rule that adds an object(or tuple) to
 510      * the set(or relation) descriptor may increase (or decrease
 511      * depending on the flag satisfyrule) the scope of a constraint or
 512      * model defintion rule r.  */
 513
 514     static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 515         for(int i=0;i<r.numQuantifiers();i++) {
 516             Quantifier q=r.getQuantifier(i);
 517             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 518                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 519                     return true;
 520             } else if (q instanceof ForQuantifier) {
 521                 if (q.getRequiredDescriptors().contains(des))
 522                     return true;
 523             } else throw new Error("Unrecognized Quantifier");
 524         }
 525         return false;
 526     }
 527
 528     static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
 529         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 530             return interferesquantifier(ar.getDescriptor(),true,q,true);
 531         return false;
 532     }
 533
 534     static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
 535         return interferesquantifier(des, satisfy, q,true);
 536     }
 537
 538     static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 539         if (interferesquantifier(des,satisfy,r,satisfyrule))
 540             return true;
 541         /* Scan DNF form */
 542         DNFRule drule=r.getDNFGuardExpr();
 543         for(int i=0;i<drule.size();i++) {
 544             RuleConjunction rconj=drule.get(i);
 545             for(int j=0;j<rconj.size();j++) {
 546                 DNFExpr dexpr=rconj.get(j);
 547                 Expr expr=dexpr.getExpr();
 548                 boolean negated=dexpr.getNegation();
 549                 /*
 550                   satisfy  negated
 551                   Yes      No             Yes
 552                   Yes      Yes            No
 553                   No       No             No
 554                   No       Yes            Yes
 555                 */
 556                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 557                 if (satisfiesrule==satisfyrule) {
 558                     /* Effect is the one being tested for */
 559                     /* Only expr's to be concerned with are TupleOfExpr and
 560                        ElementOfExpr */
 561                     if (expr.getRequiredDescriptors().contains(des)) {
 562                         if (((expr instanceof ElementOfExpr)||
 563                             (expr instanceof TupleOfExpr))&&
 564                             (expr.getRequiredDescriptors().size()==1))
 565                             return true;
 566                         else
 567                             throw new Error("Unrecognized EXPR");
 568                     }
 569                 }
 570             }
 571         }
 572         return false;
 573     }
 574 }