From fddc4e311f4a407e771b0b3b20d92e49b1658ee6 Mon Sep 17 00:00:00 2001 From: Virgile ROBLES Date: Fri, 26 Jan 2018 00:30:59 +0100 Subject: [PATCH 1/4] Fix encoding error The encode/decode is not needed and fails if any non-ASCII character is returned by g++ or clang++ --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 03256125c..3a719d322 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -889,7 +889,7 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8') + version_string = check_output([cc, '--version']) return version_string.find('clang') != -1 def is_CXX_clangpp(): From 8689921e9cf96426ca47054f3f618300e7e1ce27 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 3 Feb 2018 15:16:23 +0000 Subject: [PATCH 2/4] Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug. --- src/ast/fpa/fpa2bv_converter.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d2a946e0c..b2c07d56e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3139,6 +3139,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args unsigned bv_sz = (unsigned)f->get_parameter(0).get_int(); expr_ref bv0(m), bv1(m); + bv0 = m_bv_util.mk_numeral(0, 1); bv1 = m_bv_util.mk_numeral(1, 1); expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m); @@ -3188,9 +3189,9 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_zero_extend(2, lz)); - // big_sig is +- [... bv_sz+2 bits ...].[r][g][ ... sbits-1 ... ] - big_sig = m_bv_util.mk_zero_extend(bv_sz+2, sig); - unsigned big_sig_sz = sig_sz+bv_sz+2; + // big_sig is +- [... bv_sz+2 bits ...][1].[r][ ... sbits-1 ... ] + big_sig = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(bv_sz + 2, sig), bv0); + unsigned big_sig_sz = sig_sz+1+bv_sz+2; SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz); is_neg_shift = m_bv_util.mk_sle(exp_m_lz, m_bv_util.mk_numeral(0, ebits+2)); From c3ed9860318d3d9ae2b5f9c5da31264188b05794 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 3 Feb 2018 16:44:44 +0000 Subject: [PATCH 3/4] Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. --- src/ast/fpa/fpa2bv_converter.cpp | 6 +----- src/util/mpf.cpp | 2 +- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b2c07d56e..7c13d4315 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3746,14 +3746,10 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la expr * nround_lors[2] = { not_round, not_lors }; expr * pos_args[2] = { sgn, not_rors }; expr * neg_args[2] = { not_sgn, not_rors }; - expr * nl_r[2] = { last, not_round }; - expr * nl_nr_sn[3] = { not_last, not_round, not_sticky }; expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m); inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nround_lors)); - expr *taway_args[2] = { m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nl_r)), - m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(3, nl_nr_sn)) }; - inc_taway = m_bv_util.mk_bv_or(2, taway_args); + inc_taway = round; inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args)); inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9e309a726..b9829f02d 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -2045,7 +2045,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) { bool inc = false; switch (rm) { case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break; - case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; + case MPF_ROUND_NEAREST_TAWAY: inc = round; break; case MPF_ROUND_TOWARD_POSITIVE: inc = (!o.sign && (round || sticky)); break; case MPF_ROUND_TOWARD_NEGATIVE: inc = (o.sign && (round || sticky)); break; case MPF_ROUND_TOWARD_ZERO: inc = false; break; From 333374229d99157f6edd5bc6d21af595ed89dbd2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 3 Feb 2018 16:48:05 +0000 Subject: [PATCH 4/4] Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug. --- src/ast/fpa/fpa2bv_converter.cpp | 36 ++++++++++++++++++-------------- src/ast/fpa/fpa2bv_converter.h | 1 + 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7c13d4315..df5d56505 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3098,13 +3098,11 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex join_fp(result, result); } else { - expr * n = args[0]; - expr_ref n_bv(m); - join_fp(n, n_bv); + expr_ref nw = nan_wrap(args[0]); - sort * domain[1] = { m.get_sort(n_bv) }; + sort * domain[1] = { m.get_sort(nw) }; func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); - result = m.mk_app(f_bv, n_bv); + result = m.mk_app(f_bv, nw); expr_ref exp_bv(m), exp_all_ones(m); exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); @@ -3280,6 +3278,17 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } +expr_ref fpa2bv_converter::nan_wrap(expr * n) { + expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m); + mk_is_nan(n, arg_is_nan); + mk_nan(m.get_sort(n), nan); + join_fp(nan, nan_bv); + join_fp(n, n_bv); + res = expr_ref(m.mk_ite(arg_is_nan, nan_bv, n_bv), m); + SASSERT(is_well_sorted(m, res)); + return res; +} + void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); SASSERT(m_util.is_bv2rm(args[0])); @@ -3289,13 +3298,10 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range())); else { expr * rm_bv = to_app(args[0])->get_arg(0); - expr * n = args[1]; - expr_ref n_bv(m); - join_fp(n, n_bv); - - sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) }; + expr_ref nw = nan_wrap(args[1]); + sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(nw) }; func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); - result = m.mk_app(f_bv, rm_bv, n_bv); + result = m.mk_app(f_bv, rm_bv, nw); } TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); @@ -3309,12 +3315,10 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr result = m_arith_util.mk_numeral(rational(0), false); else { expr * n = args[0]; - expr_ref n_bv(m); - join_fp(n, n_bv); - - sort * domain[1] = { m.get_sort(n_bv) }; + expr_ref nw = nan_wrap(n); + sort * domain[1] = { m.get_sort(nw) }; func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); - result = m.mk_app(f_bv, n_bv); + result = m.mk_app(f_bv, nw); } } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index f0e50ba2d..062f7afe9 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -219,6 +219,7 @@ private: void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range); + expr_ref nan_wrap(expr * n); }; #endif