Skip to content

Commit 3d3296c

Browse files
Refactor find_qvar
Use standard algorithm instead of defining a visitor class
1 parent 7f86b50 commit 3d3296c

File tree

1 file changed

+2
-20
lines changed

1 file changed

+2
-20
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 2 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1848,32 +1848,14 @@ static exprt compute_inverse_function(
18481848
return sum_over_map(elems, f.type(), neg);
18491849
}
18501850

1851-
class find_qvar_visitort : public const_expr_visitort
1852-
{
1853-
private:
1854-
const exprt &qvar_;
1855-
1856-
public:
1857-
bool found;
1858-
1859-
explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
1860-
1861-
void operator()(const exprt &expr) override
1862-
{
1863-
if(expr==qvar_)
1864-
found=true;
1865-
}
1866-
};
1867-
18681851
/// look for the symbol and return true if it is found
18691852
/// \param index: an index expression
18701853
/// \param qvar: a symbol expression
18711854
/// \return a Boolean
18721855
static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
18731856
{
1874-
find_qvar_visitort v2(qvar);
1875-
index.visit(v2);
1876-
return v2.found;
1857+
return std::find(index.depth_begin(), index.depth_end(), qvar) !=
1858+
index.depth_end();
18771859
}
18781860

18791861
/// Add to the index set all the indices that appear in the formulas and the

0 commit comments

Comments
 (0)