Skip to content

Replace use of expr visitor by loop with depth_begin in find_index #1428

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 13, 2017
Merged

Replace use of expr visitor by loop with depth_begin in find_index #1428

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 13 additions & 31 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1744,34 +1744,6 @@ static void update_index_set(
}
}

// Will be used to visit an expression and return the index used
// with the given char array that contains qvar
class find_index_visitort: public const_expr_visitort
{
private:
const exprt &str_;
const symbol_exprt &qvar_;

public:
exprt index;

explicit find_index_visitort(
const exprt &str, const symbol_exprt &qvar):
str_(str),
qvar_(qvar),
index(nil_exprt()) {}

void operator()(const exprt &expr) override
{
if(index.is_nil() && expr.id()==ID_index)
{
const index_exprt &i=to_index_expr(expr);
if(i.array()==str_ && find_qvar(i.index(), qvar_))
index=i.index();
}
}
};

/// Finds an index on `str` used in `expr` that contains `qvar`, for instance
/// with arguments ``(str[k]=='a')``, `str`, and `k`, the function should
/// return `k`.
Expand All @@ -1782,9 +1754,19 @@ class find_index_visitort: public const_expr_visitort
static exprt find_index(
const exprt &expr, const exprt &str, const symbol_exprt &qvar)
{
find_index_visitort v(str, qvar);
expr.visit(v);
return v.index;
const auto it=std::find_if(
expr.depth_begin(),
expr.depth_end(),
[&] (const exprt &e) -> bool
{
return e.id()==ID_index
&& to_index_expr(e).array()==str
&& find_qvar(to_index_expr(e).index(), qvar);
});

return it==expr.depth_end()
?nil_exprt()
:to_index_expr(*it).index();
}

/// \par parameters: a universally quantified formula `axiom`, an array of char
Expand Down