Skip to content

Commit e125e8a

Browse files
Refactor gather_indices to use for_each instead of visitor
1 parent 4b36fc6 commit e125e8a

File tree

1 file changed

+12
-22
lines changed

1 file changed

+12
-22
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 12 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -2003,31 +2003,21 @@ static optionalt<exprt> find_counter_example(
20032003
typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
20042004

20052005
/// \related string_constraintt
2006-
class gather_indices_visitort: public const_expr_visitort
2006+
static array_index_mapt gather_indices(const exprt &expr)
20072007
{
2008-
public:
20092008
array_index_mapt indices;
2010-
2011-
gather_indices_visitort(): indices() {}
2012-
2013-
void operator()(const exprt &expr) override
2014-
{
2015-
if(expr.id()==ID_index)
2009+
// clang-format off
2010+
std::for_each(
2011+
expr.depth_begin(),
2012+
expr.depth_end(),
2013+
[&](const exprt &expr)
20162014
{
2017-
const index_exprt &index=to_index_expr(expr);
2018-
const exprt &s(index.array());
2019-
const exprt &i(index.index());
2020-
indices[s].push_back(i);
2021-
}
2022-
}
2023-
};
2024-
2025-
/// \related string_constraintt
2026-
static array_index_mapt gather_indices(const exprt &expr)
2027-
{
2028-
gather_indices_visitort v;
2029-
expr.visit(v);
2030-
return v.indices;
2015+
const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
2016+
if(index_expr)
2017+
indices[index_expr->array()].push_back(index_expr->index());
2018+
});
2019+
// clang-format on
2020+
return indices;
20312021
}
20322022

20332023
/// \param expr: an expression

0 commit comments

Comments
 (0)