import java.util.*;
class AbstractInterferes {
- static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
+ Termination termination;
+
+ public AbstractInterferes(Termination t) {
+ termination=t;
+ }
+
+ /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
+ * Rule r. */
+
+ static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
boolean mayadd=false;
boolean mayremove=false;
switch (ar.getType()) {
return false;
}
+ public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
+ if (c.numQuantifiers()==1&&
+ (c.getQuantifier(0) instanceof RelationQuantifier)) {
+ RelationQuantifier rq=(RelationQuantifier)c.getQuantifier(0);
+ if (rq.getRelation()==ar.getDescriptor()) {
+ Hashtable ht=new Hashtable();
+ if (ar.getDomainSet()!=null)
+ ht.put(rq.x,ar.getDomainSet());
+ if (ar.getRangeSet()!=null)
+ ht.put(rq.y,ar.getRangeSet());
+ DNFConstraint dconst=c.dnfconstraint;
+ conjloop:
+ for(int i=0;i<dconst.size();i++) {
+ Conjunction conj=dconst.get(i);
+ predloop:
+ for(int j=0;j<conj.size();j++) {
+ DNFPredicate dpred=conj.get(j);
+ Predicate p=dpred.getPredicate();
+ if ((p instanceof InclusionPredicate)&&(!dpred.isNegated())) {
+ InclusionPredicate ip=(InclusionPredicate)p;
+ if (ip.expr instanceof VarExpr&&
+ ip.setexpr.getDescriptor() instanceof SetDescriptor) {
+ VarDescriptor vd=((VarExpr)ip.expr).getVar();
+ if (ht.containsKey(vd)) {
+ SetDescriptor td=(SetDescriptor)ip.setexpr.getDescriptor();
+ SetDescriptor s=(SetDescriptor)ht.get(vd);
+ if (td.isSubset(s))
+ continue predloop;
+ }
+ }
+ }
+ continue conjloop;
+ }
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ /** This method checks whether a modify relation abstract repair
+ * to satisfy ar may violate dp. It returns true if there is no
+ * interference. */
+
+ private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
+ boolean neg1=ar.isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
+ Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;
+ Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
+ RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
+
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+ Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
+
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
+ ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
+ !rexpr2.usesDescriptor(updated_des)) {
+ Hashtable varmap=new Hashtable();
+ Expr l1=lexpr1;
+ Expr l2=lexpr2;
+
+ boolean initialrelation=true;
+ boolean onetoone=true;
+ while(true) {
+ if ((l1 instanceof VarExpr)&&
+ (l2 instanceof VarExpr)) {
+ VarDescriptor vd1=((VarExpr)l1).getVar();
+ VarDescriptor vd2=((VarExpr)l2).getVar();
+ varmap.put(vd1,vd2);
+ break;
+ } else if ((l1 instanceof RelationExpr)&&
+ (l2 instanceof RelationExpr)) {
+ RelationExpr re1=(RelationExpr)l1;
+ RelationExpr re2=(RelationExpr)l2;
+ if (re1.getRelation()!=re2.getRelation()||
+ re1.inverted()!=re2.inverted())
+ return false;
+
+ if (!initialrelation) {
+ if (!(
+ ConstraintDependence.rulesensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)||
+ ConstraintDependence.constraintsensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)))
+ onetoone=false;
+ //need check one-to-one property here
+ } else initialrelation=false;
+ l1=re1.getExpr();
+ l2=re2.getExpr();
+ } else return false; // bad match
+ }
+ Set freevars=rexpr1.freeVars();
+ if (freevars!=null)
+ for(Iterator it=freevars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor)it.next();
+ if (vd.isGlobal())
+ continue; //globals are fine
+ else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
+ continue;
+ else if (termination.maxsize.getsize(vd.getSet())==1)
+ continue;
+ return false;
+ }
+ return rexpr1.equals(varmap,rexpr2);
+ }
+ return false;
+ }
+
+ /** Does performing the AbstractRepair ar falsify the predicate dp */
- static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
+ public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
- ((ar.getDescriptor() instanceof SetDescriptor)||
- !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
+ // ((ar.getDescriptor() instanceof SetDescriptor)||
+ // If the second predicate uses the size of the set, modifying the set size could falsify it...
+ !dp.getPredicate().usesDescriptor(ar.getDescriptor()))
+ //)
return false;
+
+ // If the update changes something in the middle of a size
+ // expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
+ (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
+ return true;
+ }
+
+ // If the update changes something in the middle of a
+ // comparison expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
+ (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
+ return true;
+ }
+
/* This if handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg1=ar.getPredicate().isNegated();
Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
- int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
- if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
- (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
int size1a=0;
- if (!neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.GE))
- size1a=size1;
- if((op1==Opcode.GT)||(op1==Opcode.NE))
- size1a=size1+1;
- }
- if (neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.LE))
- size1a=size1+1;
- if((op1==Opcode.LT)||(op1==Opcode.NE))
- size1a=size1;
- }
- if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
- (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
- (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
- (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
- (!neg2&&(op2==Opcode.GE))||
- (!neg2&&(op2==Opcode.GT))||
- (neg2&&(op2==Opcode.LE))||
- (neg2&&(op2==Opcode.LT))||
- (neg2&&(op2==Opcode.GE)&&(size1a<size2))||
- (neg2&&(op2==Opcode.GT)&&(size1a<=size2))||
- (!neg2&&(op2==Opcode.LE)&&(size1a<=size2))||
- (!neg2&&(op2==Opcode.LT)&&(size1a<size2)))
+ if((op1==Opcode.EQ)||(op1==Opcode.GE))
+ size1a=size1;
+ if((op1==Opcode.GT)||(op1==Opcode.NE))
+ size1a=size1+1;
+
+ if (((op2==Opcode.EQ)&&(size1a==size2))||
+ ((op2==Opcode.NE)&&(size1a!=size2))||
+ (op2==Opcode.GE)||
+ (op2==Opcode.GT)||
+ ((op2==Opcode.LE)&&(size1a<=size2))||
+ ((op2==Opcode.LT)&&(size1a<size2)))
return false;
- }
+ }
}
+ /* This if handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+ boolean neg1=ar.getPredicate().isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
+ int size1a=0;
+ if((op1==Opcode.EQ)||(op1==Opcode.GE))
+ size1a=size1;
+ if((op1==Opcode.GT)||(op1==Opcode.NE))
+ size1a=size1+1;
+ if (size1a==size2)
+ return false;
+ }
+ }
+
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.MODIFYRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ int size1=1;
+
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
- if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
- (neg2&&(op2==Opcode.NE)&&(size2==0))||
- (!neg2&&(op2==Opcode.GE))||
- (!neg2&&(op2==Opcode.GT))||
- (neg2&&(op2==Opcode.LE))||
- (neg2&&(op2==Opcode.LT)))
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op2==Opcode.EQ)&&(size1==size2))||
+ ((op2==Opcode.NE)&&(size1!=size2))||
+ ((op2==Opcode.GE)&&(size1>=size2))||
+ ((op2==Opcode.GT)&&(size1>size2))||
+ ((op2==Opcode.LE)&&(size1<=size2))||
+ ((op2==Opcode.LT)&&(size1<size2)))
return false;
}
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
+
+ if ((maxsize!=-1)&&
+ ((op2==Opcode.LT&&size2>maxsize)||
+ (op2==Opcode.LE&&size2>=maxsize)||
+ (op2==Opcode.EQ&&size2>=maxsize)))
+ return false;
+
+ if (((op2==Opcode.NE)&&(size2==0))||
+ (op2==Opcode.GE)||
+ (op2==Opcode.GT))
+ return false;
+ }
+
+
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.MODIFYRELATION)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+
+ boolean neg1=ar.getPredicate().isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+ boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
+ int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
+ Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
+
+
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
+ int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
+ Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+
+
+ /* If the left sides of the comparisons are both from
+ different sets, the update is orthogonal to the expr dp */
+ {
+ Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
+ Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
+ SetDescriptor sd1=lexpr1.getSet();
+ SetDescriptor sd2=lexpr2.getSet();
+ if (termination.mutuallyexclusive(sd1,sd2))
+ return false;
+ }
+
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ /* Obvious cases which can't interfere */
+ if (((op1==Opcode.GT)||
+ (op1==Opcode.GE))&&
+ ((op2==Opcode.GT)||
+ (op2==Opcode.GE)))
+ return false;
+ if (((op1==Opcode.LT)||
+ (op1==Opcode.LE))&&
+ ((op2==Opcode.LT)||
+ (op2==Opcode.LE)))
+ return false;
+
+ if (interferemodifies(ar.getPredicate(),dp))
+ return false;
+
+ if (isInt1&&isInt2) {
+ if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
+ ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
+ size1==size2)
+ return false;
+ int size1a=size1;
+ int size2a=size2;
+ if (op1==Opcode.GT)
+ size1a++;
+ if (op1==Opcode.LT)
+ size1a--;
+ if (op1==Opcode.NE)
+ size1a++; /*FLAGNE this is current behavior for NE repairs */
+
+ if (op2==Opcode.GT)
+ size2a++;
+ if (op2==Opcode.LT)
+ size2a--;
+ if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
+ ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
+ (size1a<=size2a))
+ return false;
+ if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
+ ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
+ (size1a>=size2a))
+ return false;
+ if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
+ (size1a==size2a))
+ return false;
+ if ((op1==Opcode.EQ)&&
+ ((op2==Opcode.LE)||(op2==Opcode.LT))&&
+ (size1a<=size2a))
+ return false;
+ if ((op1==Opcode.EQ)&&
+ ((op2==Opcode.GE)||(op2==Opcode.GT))&&
+ (size1a>=size2a))
+ return false;
+ if (op2==Opcode.NE) /*FLAGNE this is current behavior for NE repairs */
+ if (size1a!=size2)
+ return false;
+ if ((op1==Opcode.NE)&&
+ (op2==Opcode.EQ)&&
+ (size1!=size2))
+ return false;
+ if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
+ ((op2==Opcode.GT)||(op2==Opcode.GE))&&
+ (size1!=size2a))
+ return false;
+ if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
+ ((op2==Opcode.LT)||(op2==Opcode.LE))&&
+ (size1!=size2a))
+ return false;
+ }
+ }
/* This handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg1=ar.getPredicate().isNegated();
Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
- int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
- if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
- (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
int size1a=0;
- if (neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.GE))
- size1a=size1-1;
- if((op1==Opcode.GT)||(op1==Opcode.NE))
- size1a=size1;
- }
- if (!neg1) {
- if((op1==Opcode.EQ)||(op1==Opcode.LE))
- size1a=size1;
- if((op1==Opcode.LT)||(op1==Opcode.NE))
- size1a=size1-1;
- }
- if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
- (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
- (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
- (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
- (neg2&&(op2==Opcode.GE))||
- (neg2&&(op2==Opcode.GT))||
- (!neg2&&(op2==Opcode.LE))||
- (!neg2&&(op2==Opcode.LT))||
- (!neg2&&(op2==Opcode.GE)&&(size1a>=size2))||
- (!neg2&&(op2==Opcode.GT)&&(size1a>size2))||
- (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
- (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
+
+ if((op1==Opcode.EQ)||(op1==Opcode.LE))
+ size1a=size1;
+ if((op1==Opcode.LT)||(op1==Opcode.NE))
+ size1a=size1-1;
+
+ if (((op2==Opcode.EQ)&&(size1a==size2))||
+ ((op2==Opcode.NE)&&(size1a!=size2))||
+ (op2==Opcode.LE)||
+ (op2==Opcode.LT)||
+ ((op2==Opcode.GE)&&(size1a>=size2))||
+ ((op2==Opcode.GT)&&(size1a>size2)))
+ return false;
+ }
+ }
+
+ /* This handles all the c comparisons in the paper */
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+ boolean neg1=ar.getPredicate().isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
+ int size1a=0;
+
+ if((op1==Opcode.EQ)||(op1==Opcode.LE))
+ size1a=size1;
+ if((op1==Opcode.LT)||(op1==Opcode.NE))
+ size1a=size1-1;
+
+ if (size1a==size2)
return false;
}
}
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
- if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
- (neg2&&(op2==Opcode.NE)&&(size2==0))||
- (neg2&&(op2==Opcode.GE))||
- (neg2&&(op2==Opcode.GT))||
- (!neg2&&(op2==Opcode.LE))||
- (!neg2&&(op2==Opcode.LT)))
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op2==Opcode.EQ)&&(size2==0))||
+ (op2==Opcode.LE)||
+ (op2==Opcode.LT))
return false;
-
}
if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
(dp.getPredicate() instanceof InclusionPredicate)&&
(dp.isNegated()==true))
return false; /* Could only satisfy this predicate */
-
return true;
}
- static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
+ /** Does the increase (or decrease) in scope of a model defintion
+ * rule represented by sn falsify the predicate dp. */
+
+ public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
Rule r=sn.getRule();
Set target=r.getInclusion().getTargetDescriptors();
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg=dp.isNegated();
Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
- int size=((ExprPredicate)dp.getPredicate()).leftsize();
- if (neg) {
- /* remove negation through opcode translation */
- if (op==Opcode.GT)
- op=Opcode.LE;
- else if (op==Opcode.GE)
- op=Opcode.LT;
- else if (op==Opcode.EQ)
- op=Opcode.NE;
- else if (op==Opcode.NE)
- op=Opcode.EQ;
- else if (op==Opcode.LT)
- op=Opcode.GE;
- else if (op==Opcode.LE)
- op=Opcode.GT;
- }
+ int size=((ExprPredicate)dp.getPredicate()).rightSize();
+ op=Opcode.translateOpcode(neg,op);
+
if ((op==Opcode.GE)&&
((size==0)||(size==1)))
return false;
return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
}
- static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
+ /** Does increasing (or decreasing if satisfy=false) the size of
+ * the set or relation des falsify the predicate dp. */
+
+ private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
if ((des!=dp.getPredicate().getDescriptor()) &&
- ((des instanceof SetDescriptor)||
- !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
+ //((des instanceof SetDescriptor)||
+ !dp.getPredicate().usesDescriptor(des))//)
return false;
/* This if handles all the c comparisons in the paper */
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op2=Opcode.translateOpcode(neg2,op2);
+
+
+ int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
{
- if ((!neg2&&(op2==Opcode.GE))||
- (!neg2&&(op2==Opcode.GT))||
- (neg2&&(op2==Opcode.EQ)&&(size2==0))||
- (!neg2&&(op2==Opcode.NE)&&(size2==0))||
- (neg2&&(op2==Opcode.LE))||
- (neg2&&(op2==Opcode.LT)))
+ if ((maxsize!=-1)&&
+ ((op2==Opcode.LT&&size2>maxsize)||
+ (op2==Opcode.LE&&size2>=maxsize)||
+ (op2==Opcode.EQ&&size2>=maxsize)))
+ return false;
+
+ if ((op2==Opcode.GE)||
+ (op2==Opcode.GT)||
+ (op2==Opcode.NE)&&(size2==0))
return false;
}
}
(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
boolean neg2=dp.isNegated();
Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
- int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+ op2=Opcode.translateOpcode(neg2,op2);
{
- if ((neg2&&(op2==Opcode.GE))||
- (neg2&&(op2==Opcode.GT))||
- (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
- (neg2&&(op2==Opcode.NE)&&(size2==0))||
- (!neg2&&(op2==Opcode.LE))||
- (!neg2&&(op2==Opcode.LT)))
+ if (((op2==Opcode.EQ)&&(size2==0))||
+ (op2==Opcode.LE)||
+ (op2==Opcode.LT))
return false;
}
}
return true;
}
- static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
+ /** This method test whether satisfying (or falsifying depending
+ * on the flag satisfy) a rule that adds an object(or tuple) to
+ * the set(or relation) descriptor may increase (or decrease
+ * depending on the flag satisfyrule) the scope of a constraint or
+ * model defintion rule r. */
+
+ static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
for(int i=0;i<r.numQuantifiers();i++) {
Quantifier q=r.getQuantifier(i);
if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
return false;
}
- static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+ static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
return interferesquantifier(ar.getDescriptor(),true,q,true);
return false;
}
- static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+ static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
return interferesquantifier(des, satisfy, q,true);
}
- static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+ static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
if (interferesquantifier(des,satisfy,r,satisfyrule))
return true;
/* Scan DNF form */