@@ -1744,34 +1744,6 @@ static void update_index_set(
1744
1744
}
1745
1745
}
1746
1746
1747
- // Will be used to visit an expression and return the index used
1748
- // with the given char array that contains qvar
1749
- class find_index_visitort : public const_expr_visitort
1750
- {
1751
- private:
1752
- const exprt &str_;
1753
- const symbol_exprt &qvar_;
1754
-
1755
- public:
1756
- exprt index;
1757
-
1758
- explicit find_index_visitort (
1759
- const exprt &str, const symbol_exprt &qvar):
1760
- str_(str),
1761
- qvar_(qvar),
1762
- index(nil_exprt()) {}
1763
-
1764
- void operator ()(const exprt &expr) override
1765
- {
1766
- if (index .is_nil () && expr.id ()==ID_index)
1767
- {
1768
- const index_exprt &i=to_index_expr (expr);
1769
- if (i.array ()==str_ && find_qvar (i.index (), qvar_))
1770
- index =i.index ();
1771
- }
1772
- }
1773
- };
1774
-
1775
1747
// / Finds an index on `str` used in `expr` that contains `qvar`, for instance
1776
1748
// / with arguments ``(str[k]=='a')``, `str`, and `k`, the function should
1777
1749
// / return `k`.
@@ -1782,9 +1754,19 @@ class find_index_visitort: public const_expr_visitort
1782
1754
static exprt find_index (
1783
1755
const exprt &expr, const exprt &str, const symbol_exprt &qvar)
1784
1756
{
1785
- find_index_visitort v (str, qvar);
1786
- expr.visit (v);
1787
- return v.index ;
1757
+ const auto it=std::find_if (
1758
+ expr.depth_begin (),
1759
+ expr.depth_end (),
1760
+ [&] (const exprt &e) -> bool
1761
+ {
1762
+ return e.id ()==ID_index
1763
+ && to_index_expr (e).array ()==str
1764
+ && find_qvar (to_index_expr (e).index (), qvar);
1765
+ });
1766
+
1767
+ return it==expr.depth_end ()
1768
+ ?nil_exprt ()
1769
+ :to_index_expr (*it).index ();
1788
1770
}
1789
1771
1790
1772
// / \par parameters: a universally quantified formula `axiom`, an array of char
0 commit comments