Skip to content

Commit 0bb17ee

Browse files
author
Daniel Kroening
committed
rewrite simplify_exprt::simplify_popcount using get_bitvector_bit
1 parent e2f2c22 commit 0bb17ee

File tree

1 file changed

+10
-14
lines changed

1 file changed

+10
-14
lines changed

src/util/simplify_expr.cpp

Lines changed: 10 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -135,25 +135,21 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
135135

136136
if(op.is_constant())
137137
{
138-
const typet &type=ns.follow(op.type());
138+
const typet &op_type = op.type();
139139

140-
if(type.id()==ID_signedbv ||
141-
type.id()==ID_unsignedbv)
140+
if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
142141
{
143-
mp_integer value;
144-
if(!to_integer(op, value))
145-
{
146-
std::size_t result;
142+
const auto width = to_bitvector_type(op_type).get_width();
143+
const auto &value = to_constant_expr(op).get_value();
144+
std::size_t result = 0;
147145

148-
for(result=0; value!=0; value=value>>1)
149-
if(value.is_odd())
150-
result++;
146+
for(std::size_t i = 0; i < width; i++)
147+
if(get_bitvector_bit(value, i))
148+
result++;
151149

152-
exprt simp_result = from_integer(result, expr.type());
153-
expr.swap(simp_result);
150+
expr = from_integer(result, expr.type());
154151

155-
return false;
156-
}
152+
return false;
157153
}
158154
}
159155

0 commit comments

Comments
 (0)