improved LE logic
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1997 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
f29e267638
commit
ab51a624e1
|
@ -227,10 +227,8 @@ public class AdHocSemiDecisionProcedure extends AbstractSemiDecisionProcedure {
|
||||||
} else if (r.getRelation().equals(BinaryRelation.GE)) {
|
} else if (r.getRelation().equals(BinaryRelation.GE)) {
|
||||||
ITerm lhs = r.getTerms().get(0);
|
ITerm lhs = r.getTerms().get(0);
|
||||||
ITerm rhs = r.getTerms().get(1);
|
ITerm rhs = r.getTerms().get(1);
|
||||||
if (lhs instanceof IntConstant && rhs instanceof IntConstant) {
|
if (isLE(rhs, lhs)) {
|
||||||
IntConstant x = (IntConstant) lhs;
|
return true;
|
||||||
IntConstant y = (IntConstant) rhs;
|
|
||||||
return x.getVal().intValue() >= y.getVal().intValue();
|
|
||||||
}
|
}
|
||||||
} else if (r.getRelation().equals(BinaryRelation.LT)) {
|
} else if (r.getRelation().equals(BinaryRelation.LT)) {
|
||||||
ITerm lhs = r.getTerms().get(0);
|
ITerm lhs = r.getTerms().get(0);
|
||||||
|
@ -243,14 +241,49 @@ public class AdHocSemiDecisionProcedure extends AbstractSemiDecisionProcedure {
|
||||||
} else if (r.getRelation().equals(BinaryRelation.LE)) {
|
} else if (r.getRelation().equals(BinaryRelation.LE)) {
|
||||||
ITerm lhs = r.getTerms().get(0);
|
ITerm lhs = r.getTerms().get(0);
|
||||||
ITerm rhs = r.getTerms().get(1);
|
ITerm rhs = r.getTerms().get(1);
|
||||||
if (lhs instanceof IntConstant && rhs instanceof IntConstant) {
|
if (isLE(lhs, rhs)) {
|
||||||
IntConstant x = (IntConstant) lhs;
|
return true;
|
||||||
IntConstant y = (IntConstant) rhs;
|
|
||||||
return x.getVal().intValue() <= y.getVal().intValue();
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* do we know a <= b ?
|
||||||
|
*
|
||||||
|
* @return false if no or maybe
|
||||||
|
*/
|
||||||
|
public boolean isLE(ITerm a, ITerm b) {
|
||||||
|
|
||||||
|
if (a.equals(b)) {
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (a instanceof IntConstant && b instanceof IntConstant) {
|
||||||
|
IntConstant ac = (IntConstant) a;
|
||||||
|
IntConstant bc = (IntConstant) b;
|
||||||
|
return ac.getVal().intValue() <= bc.getVal().intValue();
|
||||||
|
}
|
||||||
|
if (a instanceof LongConstant && b instanceof LongConstant) {
|
||||||
|
LongConstant ac = (LongConstant) a;
|
||||||
|
LongConstant bc = (LongConstant) b;
|
||||||
|
return ac.getVal().longValue() <= bc.getVal().longValue();
|
||||||
|
}
|
||||||
|
if (a instanceof DoubleConstant && b instanceof DoubleConstant) {
|
||||||
|
DoubleConstant ac = (DoubleConstant) a;
|
||||||
|
DoubleConstant bc = (DoubleConstant) b;
|
||||||
|
return ac.getVal().doubleValue() <= bc.getVal().doubleValue();
|
||||||
|
}
|
||||||
|
if (a instanceof FloatConstant && b instanceof FloatConstant) {
|
||||||
|
FloatConstant ac = (FloatConstant) a;
|
||||||
|
FloatConstant bc = (FloatConstant) b;
|
||||||
|
return ac.getVal().floatValue() <= bc.getVal().floatValue();
|
||||||
|
}
|
||||||
|
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue