Skip to content

Commit

Permalink
Simplify overflow-mult when one operand is 1
Browse files Browse the repository at this point in the history
1 (one) is a neutral element for multiplication.
  • Loading branch information
tautschnig committed Feb 3, 2022
1 parent 3c0d865 commit c2cbaad
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion src/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2174,14 +2174,23 @@ simplify_exprt::simplify_complex(const unary_exprt &expr)
simplify_exprt::resultt<>
simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
{
// zero is a neutral element for all operations supported here
// When one operand is zero, an overflow can only occur for a subtraction from
// zero.
if(
expr.op1().is_zero() ||
(expr.op0().is_zero() && expr.id() != ID_overflow_minus))
{
return false_exprt{};
}

// One is neutral element for multiplication
if(
expr.id() == ID_overflow_mult &&
(expr.op0().is_one() || expr.op1().is_one()))
{
return false_exprt{};
}

// we only handle the case of same operand types
if(expr.op0().type() != expr.op1().type())
return unchanged(expr);
Expand Down

0 comments on commit c2cbaad

Please sign in to comment.