@@ -73,11 +73,24 @@ class depth_iterator_baset
7373 typedef const exprt *pointer; // NOLINT
7474 typedef const exprt &reference; // NOLINT
7575 typedef std::forward_iterator_tag iterator_category; // NOLINT
76- bool operator ==(const depth_iterator_t &other) const
76+
77+ template <typename other_depth_iterator_t >
78+ friend class depth_iterator_baset ;
79+
80+ template <typename other_depth_iterator_t >
81+ bool operator ==(
82+ const depth_iterator_baset<other_depth_iterator_t > &other) const
7783 {
7884 return m_stack==other.m_stack ;
7985 }
8086
87+ template <typename other_depth_iterator_t >
88+ bool operator !=(
89+ const depth_iterator_baset<other_depth_iterator_t > &other) const
90+ {
91+ return !(*this == other);
92+ }
93+
8194 // / Preincrement operator
8295 // / Do not call on the end() iterator
8396 depth_iterator_t &operator ++()
@@ -152,27 +165,39 @@ class depth_iterator_baset
152165 depth_iterator_baset &operator =(depth_iterator_baset &&other)
153166 { m_stack=std::move (other.m_stack ); }
154167
155- // / Obtain non-const exprt reference. Performs a copy-on-write on
156- // / the root node as a side effect. To be called only if a the root
157- // / is a non-const exprt. Do not call on the end() iterator
168+ const exprt &get_root ()
169+ {
170+ return m_stack.front ().expr .get ();
171+ }
172+
173+ // / Obtain non-const exprt reference. Performs a copy-on-write on the root
174+ // / node as a side effect.
175+ // / \remarks
176+ // / To be called only if a the root is a non-const exprt.
177+ // / Do not call on the end() iterator
158178 exprt &mutate ()
159179 {
160180 PRECONDITION (!m_stack.empty ());
161- auto expr=std::ref (const_cast <exprt &>(m_stack.front ().expr .get ()));
181+ // Cast the root expr to non-const
182+ exprt *expr = &const_cast <exprt &>(get_root ());
162183 for (auto &state : m_stack)
163184 {
164- auto &operands=expr.get ().operands ();
185+ // This deliberately breaks sharing as expr is now non-const
186+ auto &operands = expr->operands ();
187+ // Get iterators into the operands of the new expr corresponding to the
188+ // ones into the operands of the old expr
165189 const auto i=operands.size ()-(state.end -state.it );
166190 const auto it=operands.begin ()+i;
167- state.expr = expr. get () ;
191+ state.expr = * expr;
168192 state.it =it;
169193 state.end =operands.end ();
194+ // Get the expr for the next level down to use in the next iteration
170195 if (!(state==m_stack.back ()))
171196 {
172- expr= std::ref ( *it) ;
197+ expr = & *it;
173198 }
174199 }
175- return expr. get () ;
200+ return * expr;
176201 }
177202
178203 // / Pushes expression onto the stack
@@ -194,13 +219,6 @@ class depth_iterator_baset
194219 { return static_cast <depth_iterator_t &>(*this ); }
195220};
196221
197- template <typename T, typename std::enable_if<
198- std::is_base_of<depth_iterator_baset<T>, T>::value, int >::type=0 >
199- bool operator !=(
200- const T &left,
201- const T &right)
202- { return !(left==right); }
203-
204222class const_depth_iteratort final :
205223 public depth_iterator_baset<const_depth_iteratort>
206224{
@@ -215,17 +233,58 @@ class const_depth_iteratort final:
215233class depth_iteratort final :
216234 public depth_iterator_baset<depth_iteratort>
217235{
236+ private:
237+ // / If this is non-empty then the root is currently const and this function
238+ // / must be called before any mutations occur
239+ std::function<exprt &()> mutate_root;
240+
218241public:
219242 // / Create an end iterator
220243 depth_iteratort ()=default ;
244+
221245 // / Create iterator starting at the supplied node (root)
222246 // / All mutations of the child nodes will be reflected on this node
223- explicit depth_iteratort (exprt &expr):
224- depth_iterator_baset(expr) { }
225- // / Obtain non-const reference to the pointed exprt instance
226- // / Modifies root expression
247+ // / \param expr: The root node to begin iteration at
248+ explicit depth_iteratort (exprt &expr) : depth_iterator_baset(expr)
249+ {
250+ }
251+
252+ // / Create iterator starting at the supplied node (root)
253+ // / If mutations of the child nodes are required then the passed
254+ // / mutate_root function will be called to get a non-const copy of the same
255+ // / root on which the mutations will be done.
256+ // / \param expr: The root node to begin iteration at
257+ // / \param mutate_root: The function to call to get a non-const copy of the
258+ // / same root expression passed in the expr parameter
259+ explicit depth_iteratort (
260+ const exprt &expr,
261+ std::function<exprt &()> mutate_root)
262+ : depth_iterator_baset(expr), mutate_root(std::move(mutate_root))
263+ {
264+ // If you don't provide a mutate_root function then you must pass a
265+ // non-const exprt (use the other constructor).
266+ PRECONDITION (this ->mutate_root );
267+ }
268+
269+ // / Obtain non-const reference to the exprt instance currently pointed to
270+ // / by the iterator.
271+ // / If the iterator is currently using a const root exprt then calls
272+ // / mutate_root to get a non-const root and copies it if it is shared
273+ // / \returns A non-const reference to the element this iterator is
274+ // / currently pointing to
227275 exprt &mutate ()
228- { return depth_iterator_baset::mutate (); }
276+ {
277+ if (mutate_root)
278+ {
279+ exprt &new_root = mutate_root ();
280+ INVARIANT (
281+ &new_root.read () == &get_root ().read (),
282+ " mutate_root must return the same root node that depth_iteratort was "
283+ " constructed with" );
284+ mutate_root = nullptr ;
285+ }
286+ return depth_iterator_baset::mutate ();
287+ }
229288};
230289
231290class const_unique_depth_iteratort final :
0 commit comments