File tree Expand file tree Collapse file tree 1 file changed +12
-22
lines changed
Expand file tree Collapse file tree 1 file changed +12
-22
lines changed Original file line number Diff line number Diff line change @@ -2003,31 +2003,21 @@ static optionalt<exprt> find_counter_example(
20032003typedef 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
You can’t perform that action at this time.
0 commit comments