@@ -73,11 +73,24 @@ class depth_iterator_baset
73
73
typedef const exprt *pointer; // NOLINT
74
74
typedef const exprt &reference; // NOLINT
75
75
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
77
83
{
78
84
return m_stack==other.m_stack ;
79
85
}
80
86
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
+
81
94
// / Preincrement operator
82
95
// / Do not call on the end() iterator
83
96
depth_iterator_t &operator ++()
@@ -152,27 +165,39 @@ class depth_iterator_baset
152
165
depth_iterator_baset &operator =(depth_iterator_baset &&other)
153
166
{ m_stack=std::move (other.m_stack ); }
154
167
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
158
178
exprt &mutate ()
159
179
{
160
180
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 ());
162
183
for (auto &state : m_stack)
163
184
{
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
165
189
const auto i=operands.size ()-(state.end -state.it );
166
190
const auto it=operands.begin ()+i;
167
- state.expr = expr. get () ;
191
+ state.expr = * expr;
168
192
state.it =it;
169
193
state.end =operands.end ();
194
+ // Get the expr for the next level down to use in the next iteration
170
195
if (!(state==m_stack.back ()))
171
196
{
172
- expr= std::ref ( *it) ;
197
+ expr = & *it;
173
198
}
174
199
}
175
- return expr. get () ;
200
+ return * expr;
176
201
}
177
202
178
203
// / Pushes expression onto the stack
@@ -194,13 +219,6 @@ class depth_iterator_baset
194
219
{ return static_cast <depth_iterator_t &>(*this ); }
195
220
};
196
221
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
-
204
222
class const_depth_iteratort final :
205
223
public depth_iterator_baset<const_depth_iteratort>
206
224
{
@@ -215,17 +233,58 @@ class const_depth_iteratort final:
215
233
class depth_iteratort final :
216
234
public depth_iterator_baset<depth_iteratort>
217
235
{
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
+
218
241
public:
219
242
// / Create an end iterator
220
243
depth_iteratort ()=default ;
244
+
221
245
// / Create iterator starting at the supplied node (root)
222
246
// / 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
227
275
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
+ }
229
288
};
230
289
231
290
class const_unique_depth_iteratort final :
0 commit comments