@@ -153,31 +153,28 @@ simplify_exprt::simplify_popcount(const popcount_exprt &expr)
153
153
return unchanged (expr);
154
154
}
155
155
156
- bool simplify_exprt::simplify_function_application (exprt &expr)
156
+ simplify_exprt::resultt<> simplify_exprt::simplify_function_application (
157
+ const function_application_exprt &expr)
157
158
{
158
- const function_application_exprt &function_app =
159
- to_function_application_expr (expr);
159
+ if (expr. function (). id () != ID_symbol)
160
+ return unchanged (expr);
160
161
161
- if (function_app.function ().id () != ID_symbol)
162
- return true ;
163
-
164
- const irep_idt func_id =
165
- to_symbol_expr (function_app.function ()).get_identifier ();
162
+ const irep_idt &func_id = to_symbol_expr (expr.function ()).get_identifier ();
166
163
167
164
// Starts-with is used for .equals.
168
165
if (func_id == ID_cprover_string_startswith_func)
169
166
{
170
167
// We want to get both arguments of any starts-with comparison, and
171
168
// trace them back to the actual string instance. All variables on the
172
169
// way must be constant for us to be sure this will work.
173
- auto &first_argument = to_string_expr (function_app .arguments ().at (0 ));
174
- auto &second_argument = to_string_expr (function_app .arguments ().at (1 ));
170
+ auto &first_argument = to_string_expr (expr .arguments ().at (0 ));
171
+ auto &second_argument = to_string_expr (expr .arguments ().at (1 ));
175
172
176
173
const auto first_value_opt = try_get_string_data_array (first_argument, ns);
177
174
178
175
if (!first_value_opt)
179
176
{
180
- return true ;
177
+ return unchanged (expr) ;
181
178
}
182
179
183
180
const array_exprt &first_value = first_value_opt->get ();
@@ -187,17 +184,17 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
187
184
188
185
if (!second_value_opt)
189
186
{
190
- return true ;
187
+ return unchanged (expr) ;
191
188
}
192
189
193
190
const array_exprt &second_value = second_value_opt->get ();
194
191
195
192
mp_integer offset_int = 0 ;
196
- if (function_app .arguments ().size () == 3 )
193
+ if (expr .arguments ().size () == 3 )
197
194
{
198
- auto &offset = function_app .arguments ()[2 ];
195
+ auto &offset = expr .arguments ()[2 ];
199
196
if (offset.id () != ID_constant)
200
- return true ;
197
+ return unchanged (expr) ;
201
198
offset_int = numeric_cast_v<mp_integer>(to_constant_expr (offset));
202
199
}
203
200
@@ -224,26 +221,25 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
224
221
++second_it;
225
222
}
226
223
}
227
- expr = from_integer (is_prefix ? 1 : 0 , expr. type ());
228
- return false ;
224
+
225
+ return from_integer (is_prefix ? 1 : 0 , expr. type ()) ;
229
226
}
230
227
else if (func_id == ID_cprover_string_char_at_func)
231
228
{
232
- if (function_app .arguments ().at (1 ).id () != ID_constant)
229
+ if (expr .arguments ().at (1 ).id () != ID_constant)
233
230
{
234
- return true ;
231
+ return unchanged (expr) ;
235
232
}
236
233
237
- const auto &index = to_constant_expr (function_app .arguments ().at (1 ));
234
+ const auto &index = to_constant_expr (expr .arguments ().at (1 ));
238
235
239
- const refined_string_exprt &s =
240
- to_string_expr (function_app.arguments ().at (0 ));
236
+ const refined_string_exprt &s = to_string_expr (expr.arguments ().at (0 ));
241
237
242
238
const auto char_seq_opt = try_get_string_data_array (s, ns);
243
239
244
240
if (!char_seq_opt)
245
241
{
246
- return true ;
242
+ return unchanged (expr) ;
247
243
}
248
244
249
245
const array_exprt &char_seq = char_seq_opt->get ();
@@ -252,22 +248,20 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
252
248
253
249
if (!i_opt || *i_opt >= char_seq.operands ().size ())
254
250
{
255
- return true ;
251
+ return unchanged (expr) ;
256
252
}
257
253
258
254
const auto &c = to_constant_expr (char_seq.operands ().at (*i_opt));
259
255
260
256
if (c.type () != expr.type ())
261
257
{
262
- return true ;
258
+ return unchanged (expr) ;
263
259
}
264
260
265
- expr = c;
266
-
267
- return false ;
261
+ return c;
268
262
}
269
263
270
- return true ;
264
+ return unchanged (expr) ;
271
265
}
272
266
273
267
simplify_exprt::resultt<>
@@ -2540,7 +2534,14 @@ bool simplify_exprt::simplify_node(exprt &expr)
2540
2534
}
2541
2535
}
2542
2536
else if (expr.id () == ID_function_application)
2543
- no_change = simplify_function_application (expr) && no_change;
2537
+ {
2538
+ auto r = simplify_function_application (to_function_application_expr (expr));
2539
+ if (r.has_changed ())
2540
+ {
2541
+ no_change = false ;
2542
+ expr = r.expr ;
2543
+ }
2544
+ }
2544
2545
else if (expr.id () == ID_complex_real || expr.id () == ID_complex_imag)
2545
2546
no_change = simplify_complex (expr) && no_change;
2546
2547
0 commit comments