From 35906889b60753ca34b931c0465607d46d3d1c88 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 5 Mar 2013 13:49:42 +0000 Subject: [PATCH] FPA: compilation bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 37eaa365a..42fdd0a62 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1476,8 +1476,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a expr_ref sticky(m), low(m), high(m); low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); - unsigned high_sz = m_bv_util.get_bv_size(high); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); res_sig = m_bv_util.mk_concat(high, sticky); } else @@ -1494,24 +1493,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp); else if (from_ebits > (to_ebits + 2)) { - expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), or_eq(m), not_or_eq(m), and_eq(m); + expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); low = m_bv_util.mk_extract(to_ebits+1, 0, exp); lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low); - high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high); - high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high); + high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); zero1 = m_bv_util.mk_numeral(0, 1); - m_simp.mk_eq(high_red_and, one1, and_eq); - m_simp.mk_eq(high_red_or, zero1, or_eq); + m_simp.mk_eq(high_red_and, one1, h_and_eq); + m_simp.mk_eq(high_red_or, zero1, h_or_eq); m_simp.mk_eq(lows, zero1, s_is_zero); m_simp.mk_eq(lows, one1, s_is_one); expr_ref c2(m); - m_simp.mk_ite(or_eq, s_is_one, m.mk_false(), c2); - m_simp.mk_ite(and_eq, s_is_zero, c2, exponent_overflow); + m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2); + m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow); // Note: Upon overflow, we _could_ try to shift the significand around... @@ -2416,4 +2415,4 @@ model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv) { return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv); -} \ No newline at end of file +}