diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index d8241c7b0b8..9ffb093e269 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -171,12 +171,6 @@ void bv_refinementt::check_SAT(approximationt &a) if(a.over_state==MAX_STATE) return; - ieee_float_spect spec(to_floatbv_type(type)); - ieee_floatt o0(spec), o1(spec); - - o0.unpack(a.op0_value); - o1.unpack(a.op1_value); - // get actual rounding mode constant_exprt rounding_mode_expr = to_constant_expr(get(float_op.rounding_mode())); @@ -185,10 +179,13 @@ void bv_refinementt::check_SAT(approximationt &a) ieee_floatt::rounding_modet rounding_mode = (ieee_floatt::rounding_modet)rounding_mode_int; - ieee_floatt result=o0; - o0.rounding_mode=rounding_mode; - o1.rounding_mode=rounding_mode; - result.rounding_mode=rounding_mode; + ieee_float_spect spec(to_floatbv_type(type)); + ieee_floatt o0(spec, rounding_mode), o1(spec, rounding_mode); + + o0.unpack(a.op0_value); + o1.unpack(a.op1_value); + + ieee_floatt result = o0; if(a.expr.id()==ID_floatbv_plus) result+=o1; diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 788975ba040..daf6559fd11 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -129,20 +129,22 @@ class ieee_floatt // A helper to turn a rounding mode into a constant bitvector expression static constant_exprt rounding_mode_expr(rounding_modet); - rounding_modet rounding_mode; - ieee_float_spect spec; - explicit ieee_floatt(const ieee_float_spect &_spec): - rounding_mode(ROUND_TO_EVEN), - spec(_spec), sign_flag(false), exponent(0), fraction(0), - NaN_flag(false), infinity_flag(false) + explicit ieee_floatt(const ieee_float_spect &_spec) + : spec(_spec), + rounding_mode(ROUND_TO_EVEN), + sign_flag(false), + exponent(0), + fraction(0), + NaN_flag(false), + infinity_flag(false) { } - explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode) - : rounding_mode(__rounding_mode), - spec(std::move(__spec)), + ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode) + : spec(std::move(__spec)), + rounding_mode(__rounding_mode), sign_flag(false), exponent(0), fraction(0), @@ -151,14 +153,27 @@ class ieee_floatt { } - explicit ieee_floatt(const floatbv_typet &type): - rounding_mode(ROUND_TO_EVEN), - spec(ieee_float_spect(type)), - sign_flag(false), - exponent(0), - fraction(0), - NaN_flag(false), - infinity_flag(false) + explicit ieee_floatt(const floatbv_typet &type) + : spec(ieee_float_spect(type)), + rounding_mode(ROUND_TO_EVEN), + sign_flag(false), + exponent(0), + fraction(0), + NaN_flag(false), + infinity_flag(false) + { + } + + explicit ieee_floatt( + const floatbv_typet &type, + rounding_modet __rounding_mode) + : spec(ieee_float_spect(type)), + rounding_mode(__rounding_mode), + sign_flag(false), + exponent(0), + fraction(0), + NaN_flag(false), + infinity_flag(false) { } @@ -175,6 +190,12 @@ class ieee_floatt from_expr(expr); } + ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode) + : rounding_mode(__rounding_mode) + { + from_expr(expr); + } + void negate() { sign_flag=!sign_flag; @@ -316,6 +337,8 @@ class ieee_floatt void align(); void next_representable(bool greater); + rounding_modet rounding_mode; + // we store the number unpacked bool sign_flag; mp_integer exponent; // this is unbiased diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index f7fdd2952b3..1cce00bfa96 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -190,10 +190,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr) { if(dest_type.id()==ID_floatbv) // float to float { - ieee_floatt result(to_constant_expr(casted_expr)); - result.rounding_mode = + auto rounding_mode = (ieee_floatt::rounding_modet)numeric_cast_v( *rounding_mode_index); + ieee_floatt result(to_constant_expr(casted_expr), rounding_mode); result.change_spec( ieee_float_spect(to_floatbv_type(dest_type))); return result.to_expr(); @@ -203,10 +203,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr) { if(*rounding_mode_index == ieee_floatt::ROUND_TO_ZERO) { - ieee_floatt result(to_constant_expr(casted_expr)); - result.rounding_mode = + auto rounding_mode = (ieee_floatt::rounding_modet)numeric_cast_v( *rounding_mode_index); + ieee_floatt result(to_constant_expr(casted_expr), rounding_mode); mp_integer value=result.to_integer(); return from_integer(value, dest_type); } @@ -220,10 +220,10 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr) { if(dest_type.id()==ID_floatbv) // int to float { - ieee_floatt result(to_floatbv_type(dest_type)); - result.rounding_mode = + auto rounding_mode = (ieee_floatt::rounding_modet)numeric_cast_v( *rounding_mode_index); + ieee_floatt result(to_floatbv_type(dest_type), rounding_mode); result.from_integer(*value); return result.to_expr(); } @@ -296,16 +296,16 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr) if(op0.is_constant() && op1.is_constant() && op2.is_constant()) { - ieee_floatt v0(to_constant_expr(op0)); - ieee_floatt v1(to_constant_expr(op1)); + const auto rounding_mode_opt = numeric_cast(op2); - const auto rounding_mode = numeric_cast(op2); - if(rounding_mode.has_value()) + if(rounding_mode_opt.has_value()) { - v0.rounding_mode = + const auto rounding_mode = (ieee_floatt::rounding_modet)numeric_cast_v( - *rounding_mode); - v1.rounding_mode=v0.rounding_mode; + *rounding_mode_opt); + + ieee_floatt v0(to_constant_expr(op0), rounding_mode); + ieee_floatt v1(to_constant_expr(op1), rounding_mode); ieee_floatt result=v0;