smt2 backend: fix floating-point values

Author: Daniel Kroening

scripts/delete_failing_smt2_solver_tests

@@ -29,7 +29,6 @@ rm Float13/test.desc
 rm Float20/test.desc
 rm Float22/test.desc
 rm Float23/test.desc
-rm Float24/test.desc
 rm Float3/test.desc
 rm Float4/test.desc
 rm Float5/test.desc

src/solvers/floatbv/float_bv.cpp

@@ -103,21 +103,19 @@ ieee_float_spect float_bvt::get_spec(const exprt &expr)
 exprt float_bvt::abs(const exprt &op, const ieee_float_spect &spec)
 {
   // we mask away the sign bit, which is the most significant bit
-  std::string mask_str(spec.width(), '1');
-  mask_str[0]='0';
+  const mp_integer v = power(2, spec.width() - 1) - 1;
 
-  constant_exprt mask(mask_str, op.type());
+  constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
 
   return bitand_exprt(op, mask);
 }
 
 exprt float_bvt::negation(const exprt &op, const ieee_float_spect &spec)
 {
   // we flip the sign bit with an xor
-  std::string mask_str(spec.width(), '0');
-  mask_str[0]='1';
+  const mp_integer v = power(2, spec.width() - 1);
 
-  constant_exprt mask(mask_str, op.type());
+  constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
 
   return bitxor_exprt(op, mask);
 }
@@ -150,10 +148,9 @@ exprt float_bvt::is_zero(const exprt &src)
   const floatbv_typet &type=to_floatbv_type(src.type());
   std::size_t width=type.get_width();
 
-  std::string mask_str(width, '1');
-  mask_str[0]='0';
+  const mp_integer v = power(2, width - 1) - 1;
 
-  constant_exprt mask(mask_str, src.type());
+  constant_exprt mask(integer2bvrep(v, width), src.type());
 
   ieee_floatt z(type);
   z.make_zero();

src/solvers/smt2/smt2_conv.cpp

@@ -325,7 +325,7 @@ constant_exprt smt2_convt::parse_literal(
           type.id()==ID_floatbv)
   {
     std::size_t width=boolbv_width(type);
-    return constant_exprt(integer2binary(value, width), type);
+    return constant_exprt(integer2bvrep(value, width), type);
   }
   else if(type.id()==ID_integer ||
           type.id()==ID_range)
@@ -2776,11 +2776,8 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
     else
     {
       // produce corresponding bit-vector
-      ieee_float_spect spec(floatbv_type);
-
-      mp_integer v=binary2integer(
-        id2string(expr.get_value()), false);
-
+      const ieee_float_spect spec(floatbv_type);
+      const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
       out << "(_ bv" << v << " " << spec.width() << ")";
     }
   }