Simplify (T)(a?b:c) to a?(T)b:(T)c

The idea of such a rule existed ever since 7285dda, but was possibly too
costly when doing it post-order for one would have to re-process
multiple sub-expressions. A pre-order rule avoids such repeat
processing.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1007,21 +1007,6 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     }
   }
 
-  #if 0
-  // (T)(a?b:c) --> a?(T)b:(T)c
-  if(expr.op().id()==ID_if &&
-     expr.op().operands().size()==3)
-  {
-    typecast_exprt tmp_op1(expr.op().op1(), expr_type);
-    typecast_exprt tmp_op2(expr.op().op2(), expr_type);
-    simplify_typecast(tmp_op1);
-    simplify_typecast(tmp_op2);
-    auto new_expr=if_exprt(expr.op().op0(), tmp_op1, tmp_op2, expr_type);
-    simplify_if(new_expr);
-    return std::move(new_expr);
-  }
-  #endif
-
   const irep_idt &expr_type_id=expr_type.id();
   const exprt &operand = expr.op();
   const irep_idt &op_type_id=op_type.id();
@@ -1349,6 +1334,35 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   return unchanged(expr);
 }
 
+bool simplify_exprt::simplify_typecast_preorder(typecast_exprt &expr)
+{
+  const typet &expr_type = as_const(expr).type();
+  const typet &op_type = as_const(expr).op().type();
+
+  // (T)(a?b:c) --> a?(T)b:(T)c; don't do this for floating-point type casts as
+  // the type cast itself may be costly
+  if(
+    as_const(expr).op().id() == ID_if && expr_type.id() != ID_floatbv &&
+    op_type.id() != ID_floatbv)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    simplify_if_preorder(if_expr);
+    expr.swap(if_expr);
+    return false;
+  }
+  else
+  {
+    auto r_it = simplify_rec(expr.op()); // recursive call
+    if(r_it.has_changed())
+    {
+      expr.op() = r_it.expr;
+      return false;
+    }
+    else
+      return true;
+  }
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_dereference(const dereference_exprt &expr)
 {
@@ -2616,6 +2630,8 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
   }
   else if(expr.id()==ID_if)
     result=simplify_if_preorder(to_if_expr(expr));
+  else if(expr.id() == ID_typecast)
+    result = simplify_typecast_preorder(to_typecast_expr(expr));
   else
   {
     if(expr.has_operands())

src/util/simplify_expr_class.h

@@ -147,6 +147,7 @@ class simplify_exprt
   // These below all return 'true' if the simplification wasn't applicable.
   // If false is returned, the expression has changed.
   NODISCARD resultt<> simplify_typecast(const typecast_exprt &);
+  bool simplify_typecast_preorder(typecast_exprt &);
   NODISCARD resultt<> simplify_extractbit(const extractbit_exprt &);
   NODISCARD resultt<> simplify_extractbits(const extractbits_exprt &);
   NODISCARD resultt<> simplify_concatenation(const concatenation_exprt &);

unit/util/simplify_expr.cpp

@@ -524,6 +524,21 @@ TEST_CASE("Simplifying cast expressions", "[core][util]")
     const auto simplified_expr = simplify_expr(expr, ns);
     REQUIRE(simplified_expr == expr);
   }
+
+  SECTION("Simplifying (unsigned)(B ? 4 : 5) > 3")
+  {
+    signedbv_typet sbv{4};
+    unsignedbv_typet ubv{4};
+
+    symbol_exprt b{"B", bool_typet{}};
+    if_exprt if_b{b, from_integer(4, sbv), from_integer(5, sbv)};
+
+    binary_relation_exprt comparison_gt{
+      typecast_exprt{if_b, ubv}, ID_gt, from_integer(3, ubv)};
+    exprt simp = simplify_expr(comparison_gt, ns);
+
+    REQUIRE(simp == true_exprt{});
+  }
 }
 
 TEST_CASE("Simplify bitor", "[core][util]")