@@ -446,20 +446,18 @@ bool simplify_exprt::simplify_mod(exprt &expr)
446
446
447
447
bool simplify_exprt::simplify_plus (exprt &expr)
448
448
{
449
- if (! is_number ( expr. type ()) &&
450
- expr .type ().id ()!= ID_pointer)
449
+ auto const &plus_expr = to_plus_expr ( expr);
450
+ if (! is_number (plus_expr. type ()) && plus_expr .type ().id () != ID_pointer)
451
451
return true ;
452
452
453
453
bool result=true ;
454
454
455
455
exprt::operandst &operands=expr.operands ();
456
456
457
- assert (expr.id ()==ID_plus);
458
-
459
457
// floating-point addition is _NOT_ associative; thus,
460
458
// there is special case for float
461
459
462
- if (ns.follow (expr .type ()).id ()== ID_floatbv)
460
+ if (ns.follow (plus_expr .type ()).id () == ID_floatbv)
463
461
{
464
462
// we only merge neighboring constants!
465
463
Forall_expr (it, operands)
@@ -482,14 +480,13 @@ bool simplify_exprt::simplify_plus(exprt &expr)
482
480
else
483
481
{
484
482
// ((T*)p+a)+b -> (T*)p+(a+b)
485
- if (expr.type ().id ()==ID_pointer &&
486
- expr.operands ().size ()==2 &&
487
- expr.op0 ().id ()==ID_plus &&
488
- expr.op0 ().operands ().size ()==2 )
483
+ if (
484
+ plus_expr.type ().id () == ID_pointer && plus_expr.operands ().size () == 2 &&
485
+ plus_expr.op0 ().id () == ID_plus && plus_expr.op0 ().operands ().size () == 2 )
489
486
{
490
- exprt op0=expr .op0 ();
487
+ exprt op0 = plus_expr .op0 ();
491
488
492
- if (expr .op0 ().op1 ().id ()== ID_plus)
489
+ if (plus_expr .op0 ().op1 ().id () == ID_plus)
493
490
op0.op1 ().copy_to_operands (expr.op1 ());
494
491
else
495
492
op0.op1 ()=plus_exprt (op0.op1 (), expr.op1 ());
@@ -504,7 +501,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
504
501
505
502
// count the constants
506
503
size_t count=0 ;
507
- forall_operands (it, expr )
504
+ forall_operands (it, plus_expr )
508
505
if (is_number (it->type ()) && it->is_constant ())
509
506
count++;
510
507
@@ -588,7 +585,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
588
585
589
586
if (operands.empty ())
590
587
{
591
- expr= from_integer (0 , expr .type ());
588
+ expr = from_integer (0 , plus_expr .type ());
592
589
CHECK_RETURN (expr.is_not_nil ());
593
590
return false ;
594
591
}
0 commit comments