Skip to content

Commit 2dddea3

Browse files
committed
Use lift-if more consistently
1 parent d7a0797 commit 2dddea3

File tree

3 files changed

+9
-28
lines changed

3 files changed

+9
-28
lines changed

src/util/simplify_expr_array.cpp

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "simplify_expr_class.h"
1010

1111
#include "arith_tools.h"
12+
#include "expr_util.h"
1213
#include "namespace.h"
1314
#include "pointer_offset_size.h"
1415
#include "replace_expr.h"
@@ -213,15 +214,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
213214
}
214215
else if(array.id()==ID_if)
215216
{
216-
const if_exprt &if_expr=to_if_expr(array);
217-
exprt cond=if_expr.cond();
218-
219-
index_exprt idx_false=to_index_expr(expr);
220-
idx_false.array()=if_expr.false_case();
221-
222-
to_index_expr(expr).array()=if_expr.true_case();
223-
224-
expr=if_exprt(cond, expr, idx_false, expr.type());
217+
expr = lift_if(expr, 0);
225218
simplify_rec(expr);
226219

227220
return false;

src/util/simplify_expr_pointer.cpp

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -498,16 +498,11 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
498498

499499
if(op.id()==ID_if)
500500
{
501-
const if_exprt &if_expr=to_if_expr(op);
502-
exprt cond=if_expr.cond();
503-
504-
exprt p_o_false=expr;
505-
p_o_false.op0()=if_expr.false_case();
506-
507-
expr.op0()=if_expr.true_case();
508-
509-
expr=if_exprt(cond, expr, p_o_false, expr.type());
510-
simplify_rec(expr);
501+
if_exprt if_expr = lift_if(expr, 0);
502+
simplify_pointer_object(if_expr.true_case());
503+
simplify_pointer_object(if_expr.false_case());
504+
simplify_if(if_expr);
505+
expr.swap(if_expr);
511506

512507
return false;
513508
}

src/util/simplify_expr_struct.cpp

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "arith_tools.h"
1212
#include "byte_operators.h"
13+
#include "expr_util.h"
1314
#include "invariant.h"
1415
#include "namespace.h"
1516
#include "pointer_offset_size.h"
@@ -276,15 +277,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
276277
}
277278
else if(op.id()==ID_if)
278279
{
279-
const if_exprt &if_expr=to_if_expr(op);
280-
exprt cond=if_expr.cond();
281-
282-
member_exprt member_false=to_member_expr(expr);
283-
member_false.compound()=if_expr.false_case();
284-
285-
to_member_expr(expr).compound()=if_expr.true_case();
286-
287-
expr=if_exprt(cond, expr, member_false, expr.type());
280+
expr = lift_if(expr, 0);
288281
simplify_rec(expr);
289282

290283
return false;

0 commit comments

Comments
 (0)