Preparing typing of simplify_if, use lift_if

Author: tautschnig

src/util/simplify_expr.cpp

@@ -452,7 +452,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     simplify_typecast(tmp_op1);
     simplify_typecast(tmp_op2);
     expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, expr_type);
-    simplify_if(expr);
+    simplify_if(to_if_expr(expr));
     return false;
   }
   #endif
@@ -764,7 +764,7 @@ bool simplify_exprt::simplify_dereference(exprt &expr)
 
     expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
 
-    simplify_if(expr);
+    simplify_if(to_if_expr(expr));
 
     return false;
   }
@@ -2396,7 +2396,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
           expr.id()==ID_ge    || expr.id()==ID_le)
     result=simplify_inequality(expr) && result;
   else if(expr.id()==ID_if)
-    result=simplify_if(expr) && result;
+    result=simplify_if(to_if_expr(expr)) && result;
   else if(expr.id()==ID_lambda)
     result=simplify_lambda(expr) && result;
   else if(expr.id()==ID_with)

src/util/simplify_expr_array.cpp

@@ -117,12 +117,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
         return false;
       }
 
-      exprt if_expr(ID_if, expr.type());
-      if_expr.reserve_operands(3);
-      if_expr.move_to_operands(equality_expr);
-      if_expr.copy_to_operands(with_expr.op2());
-      if_expr.move_to_operands(new_index_expr);
-
+      if_exprt if_expr(equality_expr, with_expr.op2(), new_index_expr);
       simplify_if(if_expr);
 
       expr.swap(if_expr);

src/util/simplify_expr_int.cpp

@@ -1271,18 +1271,11 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
 
   if(tmp0.id()==ID_if && tmp0.operands().size()==3)
   {
-    const if_exprt &if_expr=to_if_expr(tmp0);
-
-    exprt tmp_op1=expr;
-    tmp_op1.op0()=if_expr.true_case();
-    simplify_inequality(tmp_op1);
-    exprt tmp_op2=expr;
-    tmp_op2.op0()=if_expr.false_case();
-    simplify_inequality(tmp_op2);
-
-    expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
-
-    simplify_if(expr);
+    if_exprt if_expr=lift_if(expr, 0);
+    simplify_inequality(if_expr.true_case());
+    simplify_inequality(if_expr.false_case());
+    simplify_if(if_expr);
+    expr.swap(if_expr);
 
     return false;
   }
@@ -1680,18 +1673,11 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
 
   if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
   {
-    const if_exprt &if_expr=to_if_expr(expr.op0());
-
-    exprt tmp_op1=expr;
-    tmp_op1.op0()=if_expr.true_case();
-    simplify_inequality_constant(tmp_op1);
-    exprt tmp_op2=expr;
-    tmp_op2.op0()=if_expr.false_case();
-    simplify_inequality_constant(tmp_op2);
-
-    expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
-
-    simplify_if(expr);
+    if_exprt if_expr=lift_if(expr, 0);
+    simplify_inequality_constant(if_expr.true_case());
+    simplify_inequality_constant(if_expr.false_case());
+    simplify_if(if_expr);
+    expr.swap(if_expr);
 
     return false;
   }

src/util/simplify_expr_pointer.cpp

@@ -258,18 +258,11 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
   if(ptr.id()==ID_if && ptr.operands().size()==3)
   {
-    const if_exprt &if_expr=to_if_expr(ptr);
-
-    exprt tmp_op1=expr;
-    tmp_op1.op0()=if_expr.true_case();
-    simplify_pointer_offset(tmp_op1);
-    exprt tmp_op2=expr;
-    tmp_op2.op0()=if_expr.false_case();
-    simplify_pointer_offset(tmp_op2);
-
-    expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
-
-    simplify_if(expr);
+    if_exprt if_expr=lift_if(expr, 0);
+    simplify_pointer_offset(if_expr.true_case());
+    simplify_pointer_offset(if_expr.false_case());
+    simplify_if(if_expr);
+    expr.swap(if_expr);
 
     return false;
   }
@@ -583,18 +576,11 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
 
   if(op.id()==ID_if && op.operands().size()==3)
   {
-    const if_exprt &if_expr=to_if_expr(op);
-
-    exprt tmp_op1=expr;
-    tmp_op1.op0()=if_expr.true_case();
-    simplify_dynamic_object(tmp_op1);
-    exprt tmp_op2=expr;
-    tmp_op2.op0()=if_expr.false_case();
-    simplify_dynamic_object(tmp_op2);
-
-    expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
-
-    simplify_if(expr);
+    if_exprt if_expr=lift_if(expr, 0);
+    simplify_dynamic_object(if_expr.true_case());
+    simplify_dynamic_object(if_expr.false_case());
+    simplify_if(if_expr);
+    expr.swap(if_expr);
 
     return false;
   }