@@ -350,6 +350,7 @@ static bool are_any_top(const abstract_object_sett &set)
350
350
// ///////////////
351
351
static abstract_object_sett
352
352
non_destructive_compact (const abstract_object_sett &values);
353
+ static abstract_object_sett destructive_compact (abstract_object_sett values);
353
354
static bool value_is_not_contained_in (
354
355
const abstract_object_pointert &object,
355
356
const std::vector<constant_interval_exprt> &intervals);
@@ -359,7 +360,13 @@ static abstract_object_sett compact_values(const abstract_object_sett &values)
359
360
if (values.size () <= value_set_abstract_objectt::max_value_set_size)
360
361
return values;
361
362
362
- return non_destructive_compact (values);
363
+ auto compacted = non_destructive_compact (values);
364
+ if (compacted.size () <= value_set_abstract_objectt::max_value_set_size)
365
+ return compacted;
366
+
367
+ compacted = destructive_compact (values);
368
+
369
+ return compacted;
363
370
}
364
371
365
372
static abstract_object_sett
@@ -392,6 +399,32 @@ non_destructive_compact(const abstract_object_sett &values)
392
399
return compacted;
393
400
}
394
401
402
+ exprt eval_expr (exprt e)
403
+ {
404
+ auto dummy_symbol_table = symbol_tablet{};
405
+ auto dummy_namespace = namespacet{dummy_symbol_table};
406
+
407
+ return simplify_expr (e, dummy_namespace);
408
+ }
409
+
410
+ static abstract_object_sett destructive_compact (abstract_object_sett values)
411
+ {
412
+ auto width = values.to_interval ();
413
+ auto slice_width = eval_expr (div_exprt (
414
+ minus_exprt (width.get_upper (), width.get_lower ()),
415
+ from_integer (3 , width.type ())));
416
+
417
+ auto lower_slice = constant_interval_exprt (
418
+ width.get_lower (), eval_expr (plus_exprt (width.get_lower (), slice_width)));
419
+ auto upper_slice = constant_interval_exprt (
420
+ eval_expr (minus_exprt (width.get_upper (), slice_width)), width.get_upper ());
421
+
422
+ values.insert (interval_abstract_valuet::make_interval (lower_slice));
423
+ values.insert (interval_abstract_valuet::make_interval (upper_slice));
424
+
425
+ return non_destructive_compact (values);
426
+ } // destructive_compact
427
+
395
428
static bool value_is_not_contained_in (
396
429
const abstract_object_pointert &object,
397
430
const std::vector<constant_interval_exprt> &intervals)
0 commit comments