Skip to content

Commit eda58d0

Browse files
author
Daniel Kroening
committed
pre/post traversal expression transformers
Transformers for expressions that offer an interface similar to that offered by the goto-program API. Both pre- and post-traversal options are available. The key benefit over the non-const visit method is that sharing is only broken up when required.
1 parent 16f63e8 commit eda58d0

File tree

2 files changed

+61
-0
lines changed

2 files changed

+61
-0
lines changed

Diff for: src/util/expr.cpp

+59
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,65 @@ void exprt::visit_post(std::function<void(const exprt &)> visitor) const
287287
visit_post_template(visitor, this);
288288
}
289289

290+
optionalt<exprt>
291+
exprt::transform_pre(std::function<optionalt<exprt>(exprt)> visitor) const
292+
{
293+
auto visitor_result = visitor(*this);
294+
295+
exprt tmp;
296+
297+
if(visitor_result.has_value())
298+
tmp = visitor_result.value();
299+
else
300+
tmp = *this;
301+
302+
bool op_changed = false;
303+
304+
for(auto &op : tmp.operands()) // this breaks sharing
305+
{
306+
auto op_result = op.transform_pre(visitor);
307+
if(op_result.has_value())
308+
{
309+
op = std::move(op_result.value());
310+
op_changed = true;
311+
}
312+
}
313+
314+
if(op_changed)
315+
return std::move(tmp);
316+
else
317+
return visitor_result;
318+
}
319+
320+
optionalt<exprt>
321+
exprt::transform_post(std::function<optionalt<exprt>(exprt)> visitor) const
322+
{
323+
exprt tmp = *this;
324+
bool op_changed = false;
325+
326+
for(auto &op : tmp.operands()) // this breaks sharing
327+
{
328+
auto op_result = op.transform_post(visitor);
329+
if(op_result.has_value())
330+
{
331+
op = std::move(op_result.value());
332+
op_changed = true;
333+
}
334+
}
335+
336+
if(op_changed)
337+
{
338+
auto visitor_result = visitor(tmp);
339+
340+
if(visitor_result.has_value())
341+
return std::move(visitor_result.value());
342+
else
343+
return std::move(tmp);
344+
}
345+
else
346+
return visitor(*this);
347+
}
348+
290349
template <typename T>
291350
static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
292351
{

Diff for: src/util/expr.h

+2
Original file line numberDiff line numberDiff line change
@@ -332,12 +332,14 @@ class exprt:public irept
332332
void visit(class const_expr_visitort &visitor) const;
333333
void visit_pre(std::function<void(exprt &)>);
334334
void visit_pre(std::function<void(const exprt &)>) const;
335+
optionalt<exprt> transform_pre(std::function<optionalt<exprt>(exprt)>) const;
335336

336337
/// These are post-order traversal visitors, i.e.,
337338
/// the visitor is executed on a node _after_ its children
338339
/// have been visited.
339340
void visit_post(std::function<void(exprt &)>);
340341
void visit_post(std::function<void(const exprt &)>) const;
342+
optionalt<exprt> transform_post(std::function<optionalt<exprt>(exprt)>) const;
341343

342344
depth_iteratort depth_begin();
343345
depth_iteratort depth_end();

0 commit comments

Comments
 (0)