simplifier: eliminate casts from bool to number

This usually enables subsequent simplification, e.g.,

((int)B) != 0

turns into

(B?1:0) != 0

and then into

B?1!=0:0!=0

and then into

B?true:false

which then turns into

B

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -557,6 +557,17 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     return std::move(inequality);
   }
 
+  // eliminate casts from proper bool
+  if(op_type.id() == ID_bool)
+  {
+    // rewrite (T)(bool) to bool?1:0
+    auto one = from_integer(1, expr_type);
+    auto zero = from_integer(0, expr_type);
+    exprt new_expr = if_exprt(expr.op(), std::move(one), std::move(zero));
+    simplify_node(new_expr);
+    return std::move(new_expr);
+  }
+
   // circular casts through types shorter than `int`
   if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
   {