Skip to content

Commit

Permalink
fix intervalValue compare operators
Browse files Browse the repository at this point in the history
  • Loading branch information
jiawei.wang committed Nov 21, 2023
1 parent 3788a5f commit f4e3037
Showing 1 changed file with 74 additions and 26 deletions.
100 changes: 74 additions & 26 deletions svf/include/AbstractExecution/IntervalValue.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -577,74 +577,100 @@ inline IntervalValue operator%(const IntervalValue &lhs,
}
}

/// Greater than IntervalValues
// Compare two IntervalValues for greater than
inline IntervalValue operator>(const IntervalValue &lhs, const IntervalValue &rhs)
{
// If either lhs or rhs is bottom, the result is bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
else if (lhs.isTop() || lhs.isTop())
// If either lhs or rhs is top, the result is top
else if (lhs.isTop() || rhs.isTop())
{
return IntervalValue::top();
}
else
{
// If both lhs and rhs are numerals (lb = ub), directly compare their values
if (lhs.is_numeral() && rhs.is_numeral())
{
// It means lhs.lb() > rhs.lb()? true: false
return lhs.lb().leq(rhs.lb()) ? IntervalValue(0, 0) : IntervalValue(1, 1);
}
else
{
// lhs[3,4] rhs[1,2]
// Return [1,1] means lhs is totally greater than rhs
// When lhs.lb > rhs.ub, e.g., lhs:[3, 4] rhs:[1, 2]
// lhs.lb(3) > rhs.ub(2)
// It means lhs.lb() > rhs.ub()
if (!lhs.lb().leq(rhs.ub()))
{
return IntervalValue(1, 1);
// lhs[1,2] rhs[3,4]
}
else if (!lhs.ub().geq(rhs.lb()))
// Return [0,0] means lhs is totally impossible to be greater than rhs
// i.e., lhs is totally less than or equal to rhs
// When lhs.ub <= rhs.lb, e.g., lhs:[3, 4] rhs:[4，5]
// lhs.ub(4) <= rhs.lb(4)
else if (lhs.ub().leq(rhs.lb()))
{
return IntervalValue(0, 0);
}
// For other cases, lhs can be greater than or not, depending on the values
// e.g., lhs: [2,4], rhs: [1,3],
// lhs can be greater than rhs if lhs is 4 and rhs is 1.
// lhs can also not be greater than rhs if lhs is 2 and rhs is 3
else
{
// lhs[1,3] rhs[2,4]
return IntervalValue(0, 1);
}
}
}
}

/// Greater than IntervalValues
// Compare two IntervalValues for less than
inline IntervalValue operator<(const IntervalValue &lhs, const IntervalValue &rhs)
{
// If either lhs or rhs is bottom, the result is bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
else if (lhs.isTop() || lhs.isTop())
// If either lhs or rhs is top, the result is top
else if (lhs.isTop() || rhs.isTop())
{
return IntervalValue::top();
}
else
{
// If both lhs and rhs are numerals (lb = ub), directly compare their values
if (lhs.is_numeral() && rhs.is_numeral())
{
// It means lhs.lb() < rhs.lb()? true: false
return lhs.lb().geq(rhs.lb()) ? IntervalValue(0, 0) : IntervalValue(1, 1);
}
else
{
// lhs [1,2] rhs [3,4]
// Return [1,1] means lhs is totally less than rhs
// When lhs.ub < rhs.lb, e.g., lhs:[1, 2] rhs:[3, 4]
// lhs.ub(2) < rhs.lb(3)
// It means lhs.ub() < rhs.lb()
if (!lhs.ub().geq(rhs.lb()))
{
return IntervalValue(1, 1);
// lhs [3,4] rhs [1,2]
}
else if (!lhs.lb().leq(rhs.ub()))
// Return [0,0] means lhs is totally impossible to be less than rhs
// i.e., lhs is totally greater than or equal to rhs
// When lhs.ub >= rhs.lb, e.g., lhs:[3, 4] rhs:[4，5]
// lhs.ub(4) >= rhs.lb(4)
else if (rhs.ub().geq(lhs.lb()))
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// For other cases, lhs can be less than rhs or not, depending on the values
// e.g., lhs: [2,4], rhs: [1,3],
// lhs can be less than rhs if lhs is 2, rhs is 3.
// lhs can also not be less than rhs if lhs is 4 and rhs is 1
else
{
return IntervalValue(0, 1);
Expand All @@ -654,79 +680,101 @@ inline IntervalValue operator<(const IntervalValue &lhs, const IntervalValue &rh
}


/// Greater than IntervalValues
// Compare two IntervalValues for greater than or equal to
inline IntervalValue operator>=(const IntervalValue &lhs, const IntervalValue &rhs)
{
// If either lhs or rhs is bottom, the result is bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
else if (lhs.isTop() || lhs.isTop())
// If either lhs or rhs is top, the result is top
else if (lhs.isTop() || rhs.isTop())
{
return IntervalValue::top();
}
else
{
// If both lhs and rhs are numerals (lb = ub), directly compare their values
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().geq(rhs.lb()) ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs [2,3] rhs [1,2]
// Return [1,1] means lhs is totally greater than or equal to rhs
// When lhs.lb >= rhs.ub, e.g., lhs:[2, 3] rhs:[1, 2]
// lhs.lb(2) >= rhs.ub(2)
if (lhs.lb().geq(rhs.ub()))
{
return IntervalValue(1, 1);
// lhs [1,2] rhs[3,4]
}
// Return [0,0] means lhs is totally impossible to be greater than or equal to rhs
// i.e., lhs is totally less than rhs
// When lhs.ub < rhs.lb, e.g., lhs:[1, 2] rhs:[3, 4]
// lhs.ub(2) < rhs.lb(3)
// It means lhs.ub() < rhs.lb()
else if (!lhs.ub().geq(rhs.lb()))
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// For other cases, lhs can be greater than or equal to rhs or not, depending on the values
// e.g., lhs: [2,4], rhs: [1,3],
// lhs can be greater than or equal to rhs if lhs is 3, rhs is 2.
// lhs can also not be greater than or equal to rhs if lhs is 2 and rhs is 3
else
{
if (lhs.equals(rhs)) return IntervalValue(1, 1);
else return IntervalValue(0, 1);
return IntervalValue(0, 1);
}
}
}
}

/// Greater than IntervalValues
// Compare two IntervalValues for less than or equal to
inline IntervalValue operator<=(const IntervalValue &lhs, const IntervalValue &rhs)
{
// If either lhs or rhs is bottom, the result is bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
else if (lhs.isTop() || lhs.isTop())
// If either lhs or rhs is top, the result is top
else if (lhs.isTop() || rhs.isTop())
{
return IntervalValue::top();
}
else
{
// If both lhs and rhs are numerals (lb = ub), directly compare their values
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().leq(rhs.lb()) ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs [1,2] rhs [2,3]
// Return [1,1] means lhs is totally less than or equal to rhs
// When lhs.ub <= rhs.lb, e.g., lhs:[1, 2] rhs:[2, 3]
// lhs.ub(2) <= rhs.lb(2)
if (lhs.ub().leq(rhs.lb()))
{
return IntervalValue(1, 1);
// lhs [3,4] rhs[1,2]
}
// Return [0,0] means lhs is totally impossible to be less than or equal to rhs
// i.e., lhs is totally greater than rhs
// When lhs.lb > rhs.ub, e.g., lhs:[3, 4] rhs:[1, 2]
// lhs.lb(3) > rhs.ub(2)
// It means lhs.lb() > rhs.ub()
else if (!lhs.lb().leq(rhs.ub()))
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// For other cases, lhs can be less than or equal to rhs or not, depending on the values
// e.g., lhs: [2,4], rhs: [1,3],
// lhs can be less than or equal to rhs if lhs is 3, rhs is 3.
// lhs can also not be less than or equal to rhs if lhs is 3 and rhs is 2
else
{
if (lhs.equals(rhs)) return IntervalValue(1, 1);
else return IntervalValue(0, 1);
return IntervalValue(0, 1);
}
}
}
Expand Down

0 comments on commit f4e3037

Please sign in to comment.