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