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
  12     /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
  13      * Rule r. */
  14
  15     static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
  16         boolean mayadd=false;
  17         boolean mayremove=false;
  18         switch (ar.getType()) {
  19         case AbstractRepair.ADDTOSET:
  20         case AbstractRepair.ADDTORELATION:
  21             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  22                 return true;
  23             mayadd=true;
  24             break;
  25         case AbstractRepair.REMOVEFROMSET:
  26         case AbstractRepair.REMOVEFROMRELATION:
  27             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  28                 return true;
  29             mayremove=true;
  30             break;
  31         case AbstractRepair.MODIFYRELATION:
  32             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  33                 return true;
  34             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  35                 return true;
  36             mayadd=true;
  37             mayremove=true;
  38         break;
  39         default:
  40             throw new Error("Unrecognized Abstract Repair");
  41         }
  42         DNFRule drule=null;
  43         if (satisfy)
  44             drule=r.getDNFGuardExpr();
  45         else
  46             drule=r.getDNFNegGuardExpr();
  47
  48         for(int i=0;i<drule.size();i++) {
  49             RuleConjunction rconj=drule.get(i);
  50             for(int j=0;j<rconj.size();j++) {
  51                 DNFExpr dexpr=rconj.get(j);
  52                 Expr expr=dexpr.getExpr();
  53                 if (expr.usesDescriptor(ar.getDescriptor())) {
  54                     /* Need to check */
  55                     if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
  56                         return true;
  57                 }
  58             }
  59         }
  60         return false;
  61     }
  62
  63     /** This method is designed to check that modifying a relation
  64      * doesn't violate a relation well-formedness constraint
  65      * (ie. [forall <a,b> in R], a in S1 and b in S2; */
  66
  67     public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
  68         if (c.numQuantifiers()==1&&
  69             (c.getQuantifier(0) instanceof RelationQuantifier)) {
  70             RelationQuantifier rq=(RelationQuantifier)c.getQuantifier(0);
  71             if (rq.getRelation()==ar.getDescriptor()) {
  72                 Hashtable ht=new Hashtable();
  73                 if (ar.getDomainSet()!=null)
  74                     ht.put(rq.x,ar.getDomainSet());
  75                 if (ar.getRangeSet()!=null)
  76                     ht.put(rq.y,ar.getRangeSet());
  77                 DNFConstraint dconst=c.dnfconstraint;
  78             conjloop:
  79                 for(int i=0;i<dconst.size();i++) {
  80                     Conjunction conj=dconst.get(i);
  81                 predloop:
  82                     for(int j=0;j<conj.size();j++) {
  83                         DNFPredicate dpred=conj.get(j);
  84                         Predicate p=dpred.getPredicate();
  85                         if ((p instanceof InclusionPredicate)&&(!dpred.isNegated())) {
  86                             InclusionPredicate ip=(InclusionPredicate)p;
  87                             if (ip.expr instanceof VarExpr&&
  88                                 ip.setexpr.getDescriptor() instanceof SetDescriptor) {
  89                                 VarDescriptor vd=((VarExpr)ip.expr).getVar();
  90                                 if (ht.containsKey(vd)) {
  91                                     SetDescriptor td=(SetDescriptor)ip.setexpr.getDescriptor();
  92                                     SetDescriptor s=(SetDescriptor)ht.get(vd);
  93                                     if (td.isSubset(s))
  94                                         continue predloop;
  95                                 }
  96                             }
  97                         }
  98                         continue conjloop;
  99                     }
 100                     return true;
 101                 }
 102             }
 103         }
 104         return false;
 105     }
 106
 107
 108     /** Check to see if performing the repair ar on repair_c does not
 109      *  inferere with interfere_c.  Returns true if there is no
 110      *  interference.  */
 111
 112     public boolean interferemodifies(AbstractRepair ar, Constraint repair_c, DNFPredicate interfere_pred, Constraint interfere_c) {
 113         DNFConstraint precondition=repair_c.getDNFConstraint().not();
 114         if (repair_c.numQuantifiers()!=1||
 115             interfere_c.numQuantifiers()!=1||
 116             !(repair_c.getQuantifier(0) instanceof SetQuantifier)||
 117             !(interfere_c.getQuantifier(0) instanceof SetQuantifier)||
 118             ((SetQuantifier)repair_c.getQuantifier(0)).getSet()!=((SetQuantifier)interfere_c.getQuantifier(0)).getSet())
 119             return false;
 120
 121         Hashtable mapping=new Hashtable();
 122         mapping.put(((SetQuantifier)repair_c.getQuantifier(0)).getVar(),
 123                     ((SetQuantifier)interfere_c.getQuantifier(0)).getVar());
 124
 125         if (ar.getType()!=AbstractRepair.MODIFYRELATION||
 126             !(ar.getPredicate().getPredicate() instanceof ExprPredicate)||
 127             !(interfere_pred.getPredicate() instanceof ExprPredicate))
 128             return false;
 129         Expr e=((ExprPredicate)interfere_pred.getPredicate()).expr;
 130         Expr leftside=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).left;
 131         Set relationset=e.useDescriptor(ar.getDescriptor());
 132         for(Iterator relit=relationset.iterator();relit.hasNext();) {
 133             Expr e2=(Expr)relit.next();
 134             if (!leftside.equals(mapping,e2))
 135                 return false;
 136         }
 137         /* Prune precondition using any ar's in the same conjunction */
 138         adjustcondition(precondition, ar);
 139         Conjunction conj=findConjunction(repair_c.getDNFConstraint(),ar.getPredicate());
 140         for(int i=0;i<conj.size();i++) {
 141             DNFPredicate dp=conj.get(i);
 142             Set s=(Set)termination.predtoabstractmap.get(dp);
 143             for(Iterator it=s.iterator();it.hasNext();) {
 144                 GraphNode gn=(GraphNode)it.next();
 145                 TermNode tn=(TermNode)gn.getOwner();
 146                 AbstractRepair dp_ar=tn.getAbstract();
 147                 adjustcondition(precondition, dp_ar);
 148             }
 149         }
 150         /* We now have precondition after interference */
 151         if (precondition.size()==0)
 152             return false;
 153         DNFConstraint infr_const=interfere_c.getDNFConstraint();
 154
 155     next_conj:
 156         for(int i=0;i<infr_const.size();i++) {
 157             Conjunction infr_conj=infr_const.get(i);
 158             for(int j=0;j<infr_conj.size();j++) {
 159                 DNFPredicate infr_dp=infr_conj.get(j);
 160             next_pre_conj:
 161                 for(int i2=0;i2<precondition.size();i2++) {
 162                     Conjunction pre_conj=precondition.get(i2);
 163                     for(int j2=0;j2<pre_conj.size();j2++) {
 164                         DNFPredicate pre_dp=pre_conj.get(j2);
 165                         if (checkPreEnsures(pre_dp,infr_dp,mapping))
 166                             continue next_pre_conj;
 167
 168                     }
 169                     continue next_conj; /* The precondition doesn't ensure this conjunction is true */
 170                 }
 171             }
 172             return true; /*Found a conjunction that must be
 173                            true...therefore the precondition
 174                            guarantees that the second constraint is
 175                            always true after repair*/
 176         }
 177         return false;
 178     }
 179
 180     static private Conjunction findConjunction(DNFConstraint cons, DNFPredicate dp) {
 181         for(int i=0;i<cons.size();i++) {
 182             Conjunction conj=cons.get(i);
 183             for(int j=0;j<conj.size();j++) {
 184                 DNFPredicate curr_dp=conj.get(j);
 185                 if (curr_dp==dp)
 186                     return conj;
 187             }
 188         }
 189         throw new Error("Not found");
 190     }
 191
 192     /** This method removes predicates that the abstract repair may
 193      *  violate. */
 194
 195     private void adjustcondition(DNFConstraint precond, AbstractRepair ar) {
 196         HashSet conjremove=new HashSet();
 197         for(int i=0;i<precond.size();i++) {
 198             Conjunction conj=precond.get(i);
 199             HashSet toremove=new HashSet();
 200             for(int j=0;j<conj.size();j++) {
 201                 DNFPredicate dp=conj.get(j);
 202                 if (interfereswithpredicate(ar,dp)) {
 203                     /* Remove dp from precond */
 204                     toremove.add(dp);
 205                 }
 206             }
 207             conj.predicates.removeAll(toremove);
 208             if (conj.size()==0)
 209                 conjremove.add(conj);
 210         }
 211         precond.conjunctions.removeAll(conjremove);
 212     }
 213
 214     private boolean checkPreEnsures(DNFPredicate pre_dp,  DNFPredicate infr_dp, Hashtable mapping) {
 215         if (pre_dp.isNegated()==infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
 216             (infr_dp.getPredicate() instanceof ExprPredicate)) {
 217             if (((ExprPredicate)pre_dp.getPredicate()).expr.equals(mapping, ((ExprPredicate)infr_dp.getPredicate()).expr))
 218                 return true;
 219         }
 220         if ((!pre_dp.isNegated())&&infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
 221             (infr_dp.getPredicate() instanceof ExprPredicate)) {
 222             ExprPredicate pre_ep=(ExprPredicate)pre_dp.getPredicate();
 223             ExprPredicate infr_ep=(ExprPredicate)infr_dp.getPredicate();
 224             if (pre_ep.getType()==ExprPredicate.COMPARISON&&
 225                 infr_ep.getType()==ExprPredicate.COMPARISON&&
 226                 pre_ep.isRightInt()&&
 227                 infr_ep.isRightInt()&&
 228                 pre_ep.rightSize()!=infr_ep.rightSize()&&
 229                 pre_ep.getOp()==Opcode.EQ&&
 230                 infr_ep.getOp()==Opcode.EQ) {
 231                 if (((OpExpr)pre_ep.expr).left.equals(mapping,((OpExpr)infr_ep.expr).left))
 232                     return true;
 233             }
 234         }
 235         return false;
 236     }
 237
 238     /** This method checks whether a modify relation abstract repair
 239      * to satisfy ar may violate dp.  It returns true if there is no
 240      * interference. */
 241
 242     private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
 243         boolean neg1=ar.isNegated();
 244         Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
 245         Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;
 246         Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
 247         RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
 248
 249         boolean neg2=dp.isNegated();
 250         Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 251         Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 252         Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
 253
 254         /* Translate the opcodes */
 255         op1=Opcode.translateOpcode(neg1,op1);
 256         op2=Opcode.translateOpcode(neg2,op2);
 257
 258         if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 259             ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 260             !rexpr2.usesDescriptor(updated_des)) {
 261             Hashtable varmap=new Hashtable();
 262             Expr l1=lexpr1;
 263             Expr l2=lexpr2;
 264
 265             boolean initialrelation=true;
 266             boolean onetoone=true;
 267             while(true) {
 268                 if ((l1 instanceof VarExpr)&&
 269                     (l2 instanceof VarExpr)) {
 270                     VarDescriptor vd1=((VarExpr)l1).getVar();
 271                     VarDescriptor vd2=((VarExpr)l2).getVar();
 272                     varmap.put(vd1,vd2);
 273                     break;
 274                 } else if ((l1 instanceof RelationExpr)&&
 275                            (l2 instanceof RelationExpr)) {
 276                     RelationExpr re1=(RelationExpr)l1;
 277                     RelationExpr re2=(RelationExpr)l2;
 278                     if (re1.getRelation()!=re2.getRelation()||
 279                         re1.inverted()!=re2.inverted())
 280                         return false;
 281
 282                     if (!initialrelation) {
 283                         if (!(
 284                               ConstraintDependence.rulesensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)||
 285                               ConstraintDependence.constraintsensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)))
 286                             onetoone=false;
 287                         //need check one-to-one property here
 288                     } else initialrelation=false;
 289                     l1=re1.getExpr();
 290                     l2=re2.getExpr();
 291                 } else return false; // bad match
 292             }
 293             Set freevars=rexpr1.freeVars();
 294             if (freevars!=null)
 295                 for(Iterator it=freevars.iterator();it.hasNext();) {
 296                     VarDescriptor vd=(VarDescriptor)it.next();
 297                     if (vd.isGlobal())
 298                         continue; //globals are fine
 299                     else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
 300                         continue;
 301                     else if (termination.maxsize.getsize(vd.getSet())==1)
 302                         continue;
 303                     return false;
 304                 }
 305             return rexpr1.equals(varmap,rexpr2);
 306         }
 307         return false;
 308     }
 309
 310     /** Returns true if performing the AbstractRepair ar may falsify
 311         the predicate dp. */
 312
 313     public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
 314         if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
 315             //      ((ar.getDescriptor() instanceof SetDescriptor)||
 316             // If the second predicate uses the size of the set, modifying the set size could falsify it...
 317             !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
 318             //)
 319             return false;
 320
 321
 322         // If the update changes something in the middle of a size
 323         // expression, it interferes with it.
 324         if ((dp.getPredicate() instanceof ExprPredicate)&&
 325             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
 326             (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
 327             ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
 328             ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
 329             return true;
 330         }
 331
 332         // If the update changes something in the middle of a
 333         // comparison expression, it interferes with it.
 334         if ((dp.getPredicate() instanceof ExprPredicate)&&
 335             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
 336             (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
 337             return true;
 338         }
 339
 340         /* This if handles all the c comparisons in the paper */
 341         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 342             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 343             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 344             (dp.getPredicate() instanceof ExprPredicate)&&
 345             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 346             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 347             boolean neg1=ar.getPredicate().isNegated();
 348             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 349             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 350             boolean neg2=dp.isNegated();
 351             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 352             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 353             op1=Opcode.translateOpcode(neg1,op1);
 354             op2=Opcode.translateOpcode(neg2,op2);
 355
 356             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 357                 int size1a=0;
 358                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 359                     size1a=size1;
 360                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 361                     size1a=size1+1;
 362
 363                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 364                     ((op2==Opcode.NE)&&(size1a!=size2))||
 365                     (op2==Opcode.GE)||
 366                     (op2==Opcode.GT)||
 367                     ((op2==Opcode.LE)&&(size1a<=size2))||
 368                     ((op2==Opcode.LT)&&(size1a<size2)))
 369                     return false;
 370             }
 371         }
 372
 373         /* This if handles all the c comparisons in the paper */
 374         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 375             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 376             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 377             (dp.getPredicate() instanceof ExprPredicate)&&
 378             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 379             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 380             boolean neg1=ar.getPredicate().isNegated();
 381             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 382             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 383             int size2=1;
 384             op1=Opcode.translateOpcode(neg1,op1);
 385
 386             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
 387                 int size1a=0;
 388                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
 389                     size1a=size1;
 390                 if((op1==Opcode.GT)||(op1==Opcode.NE))
 391                     size1a=size1+1;
 392                 if (size1a==size2)
 393                     return false;
 394             }
 395         }
 396
 397         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 398             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 399             (dp.getPredicate() instanceof ExprPredicate)&&
 400             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 401             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 402             int size1=1;
 403
 404             boolean neg2=dp.isNegated();
 405             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 406             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 407
 408             op2=Opcode.translateOpcode(neg2,op2);
 409
 410             if (((op2==Opcode.EQ)&&(size1==size2))||
 411                 ((op2==Opcode.NE)&&(size1!=size2))||
 412                 ((op2==Opcode.GE)&&(size1>=size2))||
 413                 ((op2==Opcode.GT)&&(size1>size2))||
 414                 ((op2==Opcode.LE)&&(size1<=size2))||
 415                 ((op2==Opcode.LT)&&(size1<size2)))
 416                 return false;
 417         }
 418
 419         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 420             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 421             (dp.getPredicate() instanceof ExprPredicate)&&
 422             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 423             boolean neg2=dp.isNegated();
 424             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 425             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 426
 427             op2=Opcode.translateOpcode(neg2,op2);
 428
 429             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 430
 431             if ((maxsize!=-1)&&
 432                 ((op2==Opcode.LT&&size2>maxsize)||
 433                  (op2==Opcode.LE&&size2>=maxsize)||
 434                  (op2==Opcode.EQ&&size2>=maxsize)))
 435                 return false;
 436
 437             if (((op2==Opcode.NE)&&(size2==0))||
 438                 (op2==Opcode.GE)||
 439                 (op2==Opcode.GT))
 440                 return false;
 441         }
 442
 443
 444         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 445             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 446             (dp.getPredicate() instanceof ExprPredicate)&&
 447             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 448             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 449
 450             boolean neg1=ar.getPredicate().isNegated();
 451             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 452             boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
 453             int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
 454             Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 455
 456
 457             boolean neg2=dp.isNegated();
 458             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 459             boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 460             int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 461             Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 462
 463
 464             /* If the left sides of the comparisons are both from
 465                different sets, the update is orthogonal to the expr dp */
 466             {
 467                 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
 468                 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
 469                 SetDescriptor sd1=lexpr1.getSet();
 470                 SetDescriptor sd2=lexpr2.getSet();
 471                 if (termination.mutuallyexclusive(sd1,sd2))
 472                     return false;
 473             }
 474
 475             /* Translate the opcodes */
 476             op1=Opcode.translateOpcode(neg1,op1);
 477             op2=Opcode.translateOpcode(neg2,op2);
 478
 479             /* Obvious cases which can't interfere */
 480             if (((op1==Opcode.GT)||
 481                 (op1==Opcode.GE))&&
 482                 ((op2==Opcode.GT)||
 483                  (op2==Opcode.GE)))
 484                 return false;
 485             if (((op1==Opcode.LT)||
 486                 (op1==Opcode.LE))&&
 487                 ((op2==Opcode.LT)||
 488                  (op2==Opcode.LE)))
 489                 return false;
 490
 491             if (interferemodifies(ar.getPredicate(),dp))
 492                 return false;
 493
 494             if (isInt1&&isInt2) {
 495                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 496                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 497                     size1==size2)
 498                     return false;
 499                 int size1a=size1;
 500                 int size2a=size2;
 501                 if (op1==Opcode.GT)
 502                     size1a++;
 503                 if (op1==Opcode.LT)
 504                     size1a--;
 505                 if (op1==Opcode.NE)
 506                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 507
 508                 if (op2==Opcode.GT)
 509                     size2a++;
 510                 if (op2==Opcode.LT)
 511                     size2a--;
 512                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 513                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 514                     (size1a<=size2a))
 515                     return false;
 516                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 517                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 518                     (size1a>=size2a))
 519                     return false;
 520                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 521                     (size1a==size2a))
 522                     return false;
 523                 if ((op1==Opcode.EQ)&&
 524                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 525                     (size1a<=size2a))
 526                     return false;
 527                 if ((op1==Opcode.EQ)&&
 528                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 529                     (size1a>=size2a))
 530                     return false;
 531                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 532                     if (size1a!=size2)
 533                         return false;
 534                 if ((op1==Opcode.NE)&&
 535                     (op2==Opcode.EQ)&&
 536                     (size1!=size2))
 537                     return false;
 538                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 539                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 540                     (size1!=size2a))
 541                     return false;
 542                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 543                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 544                     (size1!=size2a))
 545                     return false;
 546             }
 547         }
 548         /* This handles all the c comparisons in the paper */
 549         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 550             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 551             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 552             (dp.getPredicate() instanceof ExprPredicate)&&
 553             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 554             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 555             boolean neg1=ar.getPredicate().isNegated();
 556             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 557             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 558             boolean neg2=dp.isNegated();
 559             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 560             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 561             /* Translate the opcodes */
 562             op1=Opcode.translateOpcode(neg1,op1);
 563             op2=Opcode.translateOpcode(neg2,op2);
 564
 565             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 566                 int size1a=0;
 567
 568                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 569                     size1a=size1;
 570                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 571                     size1a=size1-1;
 572
 573                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 574                     ((op2==Opcode.NE)&&(size1a!=size2))||
 575                     (op2==Opcode.LE)||
 576                     (op2==Opcode.LT)||
 577                     ((op2==Opcode.GE)&&(size1a>=size2))||
 578                     ((op2==Opcode.GT)&&(size1a>size2)))
 579                     return false;
 580             }
 581         }
 582
 583         /* This handles all the c comparisons in the paper */
 584         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 585             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 586             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 587             (dp.getPredicate() instanceof ExprPredicate)&&
 588             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 589             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 590             boolean neg1=ar.getPredicate().isNegated();
 591             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 592             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 593             int size2=1;
 594             /* Translate the opcodes */
 595             op1=Opcode.translateOpcode(neg1,op1);
 596
 597             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 598                 int size1a=0;
 599
 600                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 601                     size1a=size1;
 602                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 603                     size1a=size1-1;
 604
 605                 if (size1a==size2)
 606                     return false;
 607             }
 608         }
 609
 610         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 611             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 612             (dp.getPredicate() instanceof ExprPredicate)&&
 613             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 614             boolean neg2=dp.isNegated();
 615             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 616             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 617             op2=Opcode.translateOpcode(neg2,op2);
 618
 619             if (((op2==Opcode.EQ)&&(size2==0))||
 620                 (op2==Opcode.LE)||
 621                 (op2==Opcode.LT))
 622                 return false;
 623         }
 624         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 625             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 626             (dp.getPredicate() instanceof InclusionPredicate)&&
 627             (dp.isNegated()==false))
 628             return false; /* Could only satisfy this predicate */
 629
 630         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 631             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 632             (dp.getPredicate() instanceof InclusionPredicate)&&
 633             (dp.isNegated()==true))
 634             return false; /* Could only satisfy this predicate */
 635         return true;
 636     }
 637
 638     /** Does the increase (or decrease) in scope of a model defintion
 639      * rule represented by sn falsify the predicate dp. */
 640
 641     public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
 642         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 643             Rule r=sn.getRule();
 644             Set target=r.getInclusion().getTargetDescriptors();
 645             boolean match=false;
 646             for(int i=0;i<r.numQuantifiers();i++) {
 647                 Quantifier q=r.getQuantifier(i);
 648                 if (q instanceof SetQuantifier) {
 649                     SetQuantifier sq=(SetQuantifier) q;
 650                     if (target.contains(sq.getSet())) {
 651                         match=true;
 652                         break;
 653                     }
 654                 }
 655             }
 656             if (match&&
 657                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
 658                 (dp.getPredicate() instanceof ExprPredicate)&&
 659                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 660                 boolean neg=dp.isNegated();
 661                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 662                 int size=((ExprPredicate)dp.getPredicate()).rightSize();
 663                 op=Opcode.translateOpcode(neg,op);
 664
 665                 if ((op==Opcode.GE)&&
 666                     ((size==0)||(size==1)))
 667                     return false;
 668                 if ((op==Opcode.GT)&&
 669                     (size==0))
 670                     return false;
 671             }
 672         }
 673         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 674     }
 675
 676     /** Does increasing (or decreasing if satisfy=false) the size of
 677      * the set or relation des falsify the predicate dp. */
 678
 679     private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 680         if ((des!=dp.getPredicate().getDescriptor()) &&
 681             //((des instanceof SetDescriptor)||
 682             !dp.getPredicate().usesDescriptor(des))//)
 683             return false;
 684
 685         /* This if handles all the c comparisons in the paper */
 686         if (des==dp.getPredicate().getDescriptor()&&
 687             (satisfy)&&
 688             (dp.getPredicate() instanceof ExprPredicate)&&
 689             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 690             boolean neg2=dp.isNegated();
 691             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 692             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 693             op2=Opcode.translateOpcode(neg2,op2);
 694
 695
 696             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 697             {
 698                 if ((maxsize!=-1)&&
 699                     ((op2==Opcode.LT&&size2>maxsize)||
 700                      (op2==Opcode.LE&&size2>=maxsize)||
 701                      (op2==Opcode.EQ&&size2>=maxsize)))
 702                     return false;
 703
 704                 if ((op2==Opcode.GE)||
 705                     (op2==Opcode.GT)||
 706                     (op2==Opcode.NE)&&(size2==0))
 707                     return false;
 708             }
 709         }
 710         /* This if handles all the c comparisons in the paper */
 711         if (des==dp.getPredicate().getDescriptor()&&
 712             (!satisfy)&&
 713             (dp.getPredicate() instanceof ExprPredicate)&&
 714             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 715             boolean neg2=dp.isNegated();
 716             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 717             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 718             op2=Opcode.translateOpcode(neg2,op2);
 719             {
 720                 if (((op2==Opcode.EQ)&&(size2==0))||
 721                     (op2==Opcode.LE)||
 722                     (op2==Opcode.LT))
 723                     return false;
 724             }
 725         }
 726         if ((des==dp.getPredicate().getDescriptor())&&
 727             satisfy&&
 728             (dp.getPredicate() instanceof InclusionPredicate)&&
 729             (dp.isNegated()==false))
 730             return false; /* Could only satisfy this predicate */
 731
 732         if ((des==dp.getPredicate().getDescriptor())&&
 733             (!satisfy)&&
 734             (dp.getPredicate() instanceof InclusionPredicate)&&
 735             (dp.isNegated()==true))
 736             return false; /* Could only satisfy this predicate */
 737
 738         return true;
 739     }
 740
 741     /** This method test whether satisfying (or falsifying depending
 742      * on the flag satisfy) a rule that adds an object(or tuple) to
 743      * the set(or relation) descriptor may increase (or decrease
 744      * depending on the flag satisfyrule) the scope of a constraint or
 745      * model defintion rule r.  */
 746
 747     static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 748         for(int i=0;i<r.numQuantifiers();i++) {
 749             Quantifier q=r.getQuantifier(i);
 750             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 751                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 752                     return true;
 753             } else if (q instanceof ForQuantifier) {
 754                 if (q.getRequiredDescriptors().contains(des))
 755                     return true;
 756             } else throw new Error("Unrecognized Quantifier");
 757         }
 758         return false;
 759     }
 760
 761     static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
 762         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 763             return interferesquantifier(ar.getDescriptor(),true,q,true);
 764         return false;
 765     }
 766
 767     static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
 768         return interferesquantifier(des, satisfy, q,true);
 769     }
 770
 771     static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 772         if (interferesquantifier(des,satisfy,r,satisfyrule))
 773             return true;
 774         /* Scan DNF form */
 775         DNFRule drule=r.getDNFGuardExpr();
 776         for(int i=0;i<drule.size();i++) {
 777             RuleConjunction rconj=drule.get(i);
 778             for(int j=0;j<rconj.size();j++) {
 779                 DNFExpr dexpr=rconj.get(j);
 780                 Expr expr=dexpr.getExpr();
 781                 boolean negated=dexpr.getNegation();
 782                 /*
 783                   satisfy  negated
 784                   Yes      No             Yes
 785                   Yes      Yes            No
 786                   No       No             No
 787                   No       Yes            Yes
 788                 */
 789                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 790                 if (satisfiesrule==satisfyrule) {
 791                     /* Effect is the one being tested for */
 792                     /* Only expr's to be concerned with are TupleOfExpr and
 793                        ElementOfExpr */
 794                     if (expr.getRequiredDescriptors().contains(des)) {
 795                         if (((expr instanceof ElementOfExpr)||
 796                             (expr instanceof TupleOfExpr))&&
 797                             (expr.getRequiredDescriptors().size()==1))
 798                             return true;
 799                         else
 800                             throw new Error("Unrecognized EXPR");
 801                     }
 802                 }
 803             }
 804         }
 805         return false;
 806     }
 807 }