diff --git a/svf/include/AE/Core/AbstractState.h b/svf/include/AE/Core/AbstractState.h index f495ebb8e..21e30ca6f 100644 --- a/svf/include/AE/Core/AbstractState.h +++ b/svf/include/AE/Core/AbstractState.h @@ -393,7 +393,7 @@ class AbstractState auto it = rhs.find(item.first); if (it == rhs.end()) return false; // judge from expr id - if (item.second.getInterval().geq(it->second.getInterval())) return false; + if (item.second.getInterval().contain(it->second.getInterval())) return false; } return true; } @@ -409,7 +409,8 @@ class AbstractState // judge from expr id if (it->second.isInterval() && item.second.isInterval()) { - if (!it->second.getInterval().geq(item.second.getInterval())) + if (!it->second.getInterval().contain( + item.second.getInterval())) return false; } diff --git a/svf/include/AE/Core/IntervalValue.h b/svf/include/AE/Core/IntervalValue.h index b50dd7300..ba68d1e2e 100644 --- a/svf/include/AE/Core/IntervalValue.h +++ b/svf/include/AE/Core/IntervalValue.h @@ -298,8 +298,11 @@ class IntervalValue this->_ub = plus_infinity(); } - /// Check current IntervalValue is smaller than or equal to the other - bool leq(const IntervalValue &other) const + /// Determines if the current IntervalValue is fully contained within another IntervalValue. + /// Example: this: [2, 3], other: [1, 4] -> returns true + /// Note: If the current interval is 'bottom', it is considered contained within any interval. + /// If the other interval is 'bottom', it cannot contain any interval. + bool containedWithin(const IntervalValue &other) const { if (this->isBottom()) { @@ -316,8 +319,11 @@ class IntervalValue } - /// Check current IntervalValue is greater than or equal to the other - bool geq(const IntervalValue &other) const + /// Determines if the current IntervalValue fully contains another IntervalValue. + /// Example: this: [1, 4], other: [2, 3] -> returns true + /// Note: If the current interval is 'bottom', it is considered to contain any interval. + /// If the other interval is 'bottom', it cannot be contained by any interval. + bool contain(const IntervalValue &other) const { if (this->isBottom()) { @@ -333,6 +339,38 @@ class IntervalValue } } + /// Check the upper bound of this Interval is less than or equal to the lower bound + /// e.g. [1, 3] < [3, 5] return true, lhs.ub <= rhs.lb + bool leq(const IntervalValue &other) const { + if (this->isBottom()) { + return true; + } + else if (other.isBottom()) + { + return false; + } + else + { + return this->_ub.leq(other._lb); + } + } + + /// Check the lower bound of this Interval is greater than or equal to the upper bound + /// e.g. [3, 5] > [1, 3] return true, lhs.lb >= rhs.ub + bool geq(const IntervalValue &other) const { + if (this->isBottom()) { + return true; + } + else if (other.isBottom()) + { + return false; + } + else + { + return this->_lb.geq(other._ub); + } + } + /// Equality comparison bool equals(const IntervalValue &other) const