Make convert_abs take an abs_exprt parameter

Author: romainbrenguier

src/solvers/flattening/boolbv.cpp

@@ -253,7 +253,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bitvector(expr.op0());
   }
   else if(expr.id()==ID_abs)
-    return convert_abs(expr);
+    return convert_abs(to_abs_expr(expr));
   else if(expr.id() == ID_bswap)
     return convert_bswap(to_bswap_expr(expr));
   else if(expr.id()==ID_byte_extract_little_endian ||

src/solvers/flattening/boolbv.h

@@ -163,7 +163,7 @@ class boolbvt:public arrayst
   virtual bvt convert_shift(const binary_exprt &expr);
   virtual bvt convert_bitwise(const exprt &expr);
   virtual bvt convert_unary_minus(const unary_exprt &expr);
-  virtual bvt convert_abs(const exprt &expr);
+  virtual bvt convert_abs(const abs_exprt &expr);
   virtual bvt convert_concatenation(const exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);
   virtual bvt convert_bv_literals(const exprt &expr);

src/solvers/flattening/boolbv_abs.cpp

@@ -14,26 +14,19 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/floatbv/float_utils.h>
 
-bvt boolbvt::convert_abs(const exprt &expr)
+bvt boolbvt::convert_abs(const abs_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t width = boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  const exprt::operandst &operands=expr.operands();
+  const bvt &op_bv=convert_bv(expr.op());
 
-  if(operands.size()!=1)
-    throw "abs takes one operand";
-
-  const exprt &op0=expr.op0();
-
-  const bvt &op_bv=convert_bv(op0);
-
-  if(op0.type()!=expr.type())
+  if(expr.op().type()!=expr.type())
     return conversion_failed(expr);
 
-  bvtypet bvtype=get_bvtype(expr.type());
+  const bvtypet bvtype = get_bvtype(expr.type());
 
   if(bvtype==bvtypet::IS_FIXED ||
      bvtype==bvtypet::IS_SIGNED ||