Merge pull request #4402 from diffblue/exprt-visit-lamba2

exprt::visit post-order traversal variant

Author: tautschnig

src/util/expr.cpp

@@ -243,6 +243,50 @@ const source_locationt &exprt::find_source_location() const
   return static_cast<const source_locationt &>(get_nil_irep());
 }
 
+template <typename T>
+void visit_post_template(std::function<void(T &)> visitor, T *_expr)
+{
+  struct stack_entryt
+  {
+    T *e;
+    bool operands_pushed;
+    explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
+    {
+    }
+  };
+
+  std::stack<stack_entryt> stack;
+
+  stack.emplace(_expr);
+
+  while(!stack.empty())
+  {
+    auto &top = stack.top();
+    if(top.operands_pushed)
+    {
+      visitor(*top.e);
+      stack.pop();
+    }
+    else
+    {
+      // do modification of 'top' before pushing in case 'top' isn't stable
+      top.operands_pushed = true;
+      for(auto &op : top.e->operands())
+        stack.emplace(&op);
+    }
+  }
+}
+
+void exprt::visit_post(std::function<void(exprt &)> visitor)
+{
+  visit_post_template(visitor, this);
+}
+
+void exprt::visit_post(std::function<void(const exprt &)> visitor) const
+{
+  visit_post_template(visitor, this);
+}
+
 template <typename T>
 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
 {

src/util/expr.h

@@ -332,6 +332,12 @@ class exprt:public irept
   void visit_pre(std::function<void(exprt &)>);
   void visit_pre(std::function<void(const exprt &)>) const;
 
+  /// These are post-order traversal visitors, i.e.,
+  /// the visitor is executed on a node _after_ its children
+  /// have been visited.
+  void visit_post(std::function<void(exprt &)>);
+  void visit_post(std::function<void(const exprt &)>) const;
+
   depth_iteratort depth_begin();
   depth_iteratort depth_end();
   const_depth_iteratort depth_begin() const;