Split convert_overflow into binary and unary variations

Because the code used for one operand vs two operands is slightly
different and because this facilitates a more type-specific
implementation.

Author: thomasspriggs

src/solvers/flattening/boolbv.cpp

@@ -417,10 +417,16 @@ literalt boolbvt::convert_rest(const exprt &expr)
   else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
     return convert_onehot(to_unary_expr(expr));
   else if(
-    can_cast_expr<binary_overflow_exprt>(expr) ||
-    can_cast_expr<unary_minus_overflow_exprt>(expr))
+    const auto binary_overflow =
+      expr_try_dynamic_cast<binary_overflow_exprt>(expr))
   {
-    return convert_overflow(expr);
+    return convert_binary_overflow(*binary_overflow);
+  }
+  else if(
+    const auto unary_overflow =
+      expr_try_dynamic_cast<unary_overflow_exprt>(expr))
+  {
+    return convert_unary_overflow(*unary_overflow);
   }
   else if(expr.id()==ID_isnan)
   {

src/solvers/flattening/boolbv.h

@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arrays.h"
 
 class array_comprehension_exprt;
+class binary_overflow_exprt;
 class bitreverse_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
@@ -38,6 +39,7 @@ class floatbv_typecast_exprt;
 class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
+class unary_overflow_exprt;
 class union_typet;
 
 class boolbvt:public arrayst
@@ -140,7 +142,8 @@ class boolbvt:public arrayst
   virtual literalt convert_reduction(const unary_exprt &expr);
   virtual literalt convert_onehot(const unary_exprt &expr);
   virtual literalt convert_extractbit(const extractbit_exprt &expr);
-  virtual literalt convert_overflow(const exprt &expr);
+  virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr);
+  virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr);
   virtual literalt convert_equality(const equal_exprt &expr);
   virtual literalt convert_verilog_case_equality(
     const binary_relation_exprt &expr);

src/solvers/flattening/boolbv_overflow.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-literalt boolbvt::convert_overflow(const exprt &expr)
+literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr)
 {
   const auto plus_or_minus_conversion =
     [&](
@@ -161,7 +161,13 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     return
       prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
   }
-  else if(
+
+  return SUB::convert_rest(expr);
+}
+
+literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr)
+{
+  if(
     const auto unary_minus_overflow =
       expr_try_dynamic_cast<unary_minus_overflow_exprt>(expr))
   {