From be1df279ecac4bb3a9a07008368540d1b860faba Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:11:07 -0400 Subject: [PATCH 1/8] make proof_checker less verbose --- src/ast/proof_checker/proof_checker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 45223cdb7..df4a8e344 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -1299,7 +1299,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& is_pos = !is_pos; } if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) { - IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";); return false; } SASSERT(lit->get_num_args() == 2); @@ -1363,7 +1363,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& rw(sum); } - IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";); #endif return true; From 15451ae8580a8bf230ce2d1257bc7f0a64b19d80 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:13:08 -0400 Subject: [PATCH 2/8] extra flags to control quant_hoist --- src/ast/rewriter/quant_hoist.cpp | 80 ++++++++++++++++++-------------- src/ast/rewriter/quant_hoist.h | 8 ++-- 2 files changed, 50 insertions(+), 38 deletions(-) diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index e59a079e7..9c345851a 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -41,9 +41,9 @@ public: m_rewriter(m) {} - void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { + void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) { quantifier_type qt = Q_none_pos; - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); @@ -51,36 +51,38 @@ public: is_fa = (Q_forall_pos == qt); } - void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { + void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { quantifier_type qt = Q_exists_pos; - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); } - void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { + void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) { quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos; expr_ref result(m); - pull_quantifier(fml, qt, vars, result); + pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok); TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); fml = result; } - void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) { + void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) { unsigned nd = q->get_num_decls(); for (unsigned i = 0; i < nd; ++i) { sort* s = q->get_decl_sort(i); - app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s); + symbol const& sym = q->get_decl_name (i); + app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s) + : m.mk_const (sym, s); vars.push_back(a); } expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd); instantiate(m, q, exprs, result); } - unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh, bool rewrite_ok) { unsigned index = var_counter().get_next_var(fml); while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) { quantifier* q = to_quantifier(fml); @@ -97,7 +99,7 @@ public: return index; } app_ref_vector vars(m); - pull_quantifier(is_forall, fml, vars); + pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok); if (vars.empty()) { return index; } @@ -192,7 +194,7 @@ private: } - void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) { + void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { if (!has_quantifiers(fml)) { result = fml; @@ -209,38 +211,48 @@ private: if (m.is_and(fml)) { num_args = a->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - pull_quantifier(a->get_arg(i), qt, vars, tmp); + pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok); args.push_back(tmp); } + if (rewrite_ok) { m_rewriter.mk_and(args.size(), args.c_ptr(), result); + } + else { + result = m.mk_and (args.size (), args.c_ptr ()); + } } else if (m.is_or(fml)) { num_args = to_app(fml)->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp); + pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok); args.push_back(tmp); } + if (rewrite_ok) { m_rewriter.mk_or(args.size(), args.c_ptr(), result); + } + else { + result = m.mk_or (args.size (), args.c_ptr ()); + } } else if (m.is_not(fml)) { - pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp); + pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok); negate(qt); result = m.mk_not(tmp); } else if (m.is_implies(fml, t1, t2)) { - pull_quantifier(t1, negate(qt), vars, tmp); + pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok); negate(qt); - pull_quantifier(t2, qt, vars, result); + pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok); result = m.mk_implies(tmp, result); } else if (m.is_ite(fml, t1, t2, t3)) { expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m); - pull_quantifier(t2, qt, vars, tt2); - pull_quantifier(t3, qt, vars, tt3); + pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok); + pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok); if (has_quantifiers(t1)) { - pull_quantifier(t1, qt, vars, tt1); + pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); nt1 = m.mk_not(t1); - pull_quantifier(nt1, qt, vars, ntt1); + pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3)); } else { @@ -249,12 +261,12 @@ private: } else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) { expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m); - pull_quantifier(t1, qt, vars, tt1); - pull_quantifier(t2, qt, vars, tt2); + pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); + pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok); nt1 = m.mk_not(t1); nt2 = m.mk_not(t2); - pull_quantifier(nt1, qt, vars, ntt1); - pull_quantifier(nt2, qt, vars, ntt2); + pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); + pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1)); } else { @@ -271,8 +283,8 @@ private: break; } set_quantifier_type(qt, q->is_forall()); - extract_quantifier(q, vars, tmp); - pull_quantifier(tmp, qt, vars, result); + extract_quantifier(q, vars, tmp, use_fresh); + pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok); break; } case AST_VAR: @@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() { dealloc(m_impl); } -void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { - (*m_impl)(fml, vars, is_fa, result); +void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) { + (*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok); } -void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { - m_impl->pull_exists(fml, vars, result); +void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) { + m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok); } -void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { - m_impl->pull_quantifier(is_forall, fml, vars); +void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) { + m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok); } -unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names) { - return m_impl->pull_quantifier(is_forall, fml, sorts, names); +unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh, bool rewrite_ok) { + return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok); } diff --git a/src/ast/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h index 90e6ec7ad..52a2fcda1 100644 --- a/src/ast/rewriter/quant_hoist.h +++ b/src/ast/rewriter/quant_hoist.h @@ -43,14 +43,14 @@ public: or, and, implies, ite (then and else branch only). */ - void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result); + void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); /** \brief Pull top-most existential quantifier up. The list of variables is empty if there are no top-level existential quantifier. */ - void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result); + void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); /** @@ -58,7 +58,7 @@ public: The list of variables is empty if there are no top-level universal/existential quantifier. */ - void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars); + void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true); /** \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up. @@ -66,7 +66,7 @@ public: Return index of maximal variable. */ - unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names); + unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector* sorts, svector* names, bool use_fresh = true, bool rewrite_ok = true); }; From 7670b49ada29df98776a15fdebf2a85be4de3631 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:14:35 -0400 Subject: [PATCH 3/8] mark mk_true() and mk_false() const --- src/ast/ast.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index f71d5135c..75d3eb0f2 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2021,8 +2021,8 @@ public: app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); } app * mk_distinct(unsigned num_args, expr * const * args); app * mk_distinct_expanded(unsigned num_args, expr * const * args); - app * mk_true() { return m_true; } - app * mk_false() { return m_false; } + app * mk_true() const { return m_true; } + app * mk_false() const { return m_false; } app * mk_bool_val(bool b) { return b?m_true:m_false; } app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } From 331eec8a05e857773e196dcbafbd4aff589c87a2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:19:16 -0400 Subject: [PATCH 4/8] option to control array_der in qe_lite --- src/qe/qe_lite.cpp | 15 +++++++++------ src/qe/qe_lite.h | 5 ++++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index ce182a97b..ff2abde75 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2342,6 +2342,7 @@ private: elim_star m_elim_star; th_rewriter m_rewriter; + bool m_use_array_der; bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) { index = fmls.size(); if (index <= 1) { @@ -2359,13 +2360,14 @@ private: } public: - impl(ast_manager & m, params_ref const & p): + impl(ast_manager & m, params_ref const & p, bool use_array_der): m(m), m_der(m, p), m_fm(m), m_array_der(m), m_elim_star(*this), - m_rewriter(m) {} + m_rewriter(m), + m_use_array_der(use_array_der) {} void operator()(app_ref_vector& vars, expr_ref& fml) { if (vars.empty()) { @@ -2445,14 +2447,15 @@ public: m_array_der.set_is_variable_proc(is_var); m_der(fmls); m_fm(fmls); - m_array_der(fmls); + // AG: disalble m_array_der() since it interferes with other array handling + if (m_use_array_der) m_array_der(fmls); TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); } }; -qe_lite::qe_lite(ast_manager & m, params_ref const & p) { - m_impl = alloc(impl, m, p); +qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) { + m_impl = alloc(impl, m, p, use_array_der); } qe_lite::~qe_lite() { @@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic { imp(ast_manager& m, params_ref const & p): m(m), - m_qe(m, p) + m_qe(m, p, true) {} void checkpoint() { diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h index cff547f36..a918ab33d 100644 --- a/src/qe/qe_lite.h +++ b/src/qe/qe_lite.h @@ -31,7 +31,10 @@ class qe_lite { class impl; impl * m_impl; public: - qe_lite(ast_manager & m, params_ref const & p); + /** + use_array_der controls whether equalities over array reads are simplified + */ + qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true); ~qe_lite(); From 1d5713c3764a6f9fb62f2fff39d5dc727c4d2321 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 31 Jul 2017 14:21:30 -0400 Subject: [PATCH 5/8] move semantics for ref --- src/util/ref.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/util/ref.h b/src/util/ref.h index d9663f9a4..811aba9af 100644 --- a/src/util/ref.h +++ b/src/util/ref.h @@ -50,6 +50,7 @@ public: inc_ref(); } + ref (ref && r): m_ptr (r.detach ()) {} ~ref() { dec_ref(); } @@ -89,6 +90,14 @@ public: return *this; } + ref & operator=(ref &&r) { + if (this != &r) { + dec_ref (); + m_ptr = r.detach (); + } + return *this; + } + void reset() { dec_ref(); m_ptr = 0; @@ -107,6 +116,11 @@ public: friend bool operator!=(const ref & r1, const ref & r2) { return r1.m_ptr != r2.m_ptr; } + friend void swap (ref &r1, ref &r2) { + T* tmp = r1.m_ptr; + r1.m_ptr = r2.m_ptr; + r2.m_ptr = tmp; + } }; /** From ecfd241e19fd2a6c5459dd69011a106e6f87587c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 19:44:36 +0100 Subject: [PATCH 6/8] Injected 3 missing bits of precision into fp.rem. Relates to #872. --- src/ast/fpa/fpa2bv_converter.cpp | 53 ++++++++++++++++---------------- src/util/mpf.cpp | 27 ++++++++-------- 2 files changed, 42 insertions(+), 38 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 864293380..7e56df405 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1535,11 +1535,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // Extend c expr_ref c_sig_ext(m); - c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits - 1))); + c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits - 1 + 3))); c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); + mul_sig = m_bv_util.mk_concat(mul_sig, m_bv_util.mk_numeral(0, 3)); - SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits); - SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits); + SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits + 3); dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext); dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext); @@ -1550,10 +1551,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m); m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn); - m_simp.mk_ite(swap_cond, c_sig_ext, mul_sig, e_sig); // has 2 * sbits + m_simp.mk_ite(swap_cond, c_sig_ext, mul_sig, e_sig); // has 2 * sbits + 3 m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2 m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn); - m_simp.mk_ite(swap_cond, mul_sig, c_sig_ext, f_sig); // has 2 * sbits + m_simp.mk_ite(swap_cond, mul_sig, c_sig_ext, f_sig); // has 2 * sbits + 3 m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 SASSERT(is_well_sorted(m, e_sgn)); @@ -1563,8 +1564,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(is_well_sorted(m, f_sig)); SASSERT(is_well_sorted(m, f_exp)); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits); - SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits + 3); SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2); SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2); @@ -1581,7 +1582,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // cap the delta expr_ref cap(m), cap_le_delta(m); - cap = m_bv_util.mk_numeral(2*sbits, ebits+2); + cap = m_bv_util.mk_numeral(2*sbits+3, ebits+2); cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2); @@ -1593,14 +1594,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref alignment_sticky_raw(m), alignment_sticky(m); shifted_big = m_bv_util.mk_bv_lshr( m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), - m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta)); - shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big); + m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta)); + shifted_f_sig = m_bv_util.mk_extract(3*sbits-1+3, sbits, shifted_big); alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get()); dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig); dbg_decouple("fpa2bv_fma_f_sig_alignment_sticky", alignment_sticky); SASSERT(is_well_sorted(m, alignment_sticky)); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+3); SASSERT(is_well_sorted(m, shifted_f_sig)); // Significant addition. @@ -1612,14 +1613,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); dbg_decouple("fpa2bv_fma_eq_sgn", eq_sgn); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits + 2); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+2+3); dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); expr_ref sum(m), e_plus_f(m), e_minus_f(m), sticky_wide(m); - sticky_wide = m_bv_util.mk_zero_extend(2*sbits+1, alignment_sticky); + sticky_wide = m_bv_util.mk_zero_extend(2*sbits+1+3, alignment_sticky); e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); e_plus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_plus_f), zero_1), m_bv_util.mk_bv_add(e_plus_f, sticky_wide), @@ -1632,12 +1633,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig); m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); - SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits + 2); + SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+2+3); SASSERT(is_well_sorted(m, sum)); dbg_decouple("fpa2bv_fma_add_sum", sum); expr_ref sign_bv(m), n_sum(m); - sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum); + sign_bv = m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+1+3, sum); n_sum = m_bv_util.mk_bv_neg(sum); dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); @@ -1661,14 +1662,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_res_sgn", res_sgn); expr_ref is_sig_neg(m); - is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits + 1, sig_abs)); + is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+1+3, sig_abs)); sig_abs = m.mk_ite(is_sig_neg, m_bv_util.mk_bv_neg(sig_abs), sig_abs); dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg); // Result could have overflown into 4.xxx. - SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2); + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+2+3); expr_ref extra(m), extra_is_zero(m); - extra = m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs); + extra = m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+3, sig_abs); extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2)); dbg_decouple("fpa2bv_fma_extra", extra); @@ -1685,7 +1686,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, sig_lz_capped = m.mk_ite(m_bv_util.mk_sle(sig_lz, max_exp_delta), sig_lz, max_exp_delta); renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2); res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta); - sig_abs = m_bv_util.mk_bv_shl(sig_abs, m_bv_util.mk_zero_extend(2*sbits-ebits, renorm_delta)); + sig_abs = m_bv_util.mk_bv_shl(sig_abs, m_bv_util.mk_zero_extend(2*sbits+3-ebits, renorm_delta)); dbg_decouple("fpa2bv_fma_min_exp", min_exp); dbg_decouple("fpa2bv_fma_max_exp_delta", max_exp_delta); dbg_decouple("fpa2bv_fma_sig_lz", sig_lz); @@ -1699,26 +1700,26 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, } expr_ref sig_abs_h1(m), sticky_h1(m), sticky_h1_red(m), sig_abs_h1_f(m), res_sig_1(m); - sticky_h1 = m_bv_util.mk_extract(sbits - 5 + too_short, 0, sig_abs); - sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 4 + too_short, sig_abs); + sticky_h1 = m_bv_util.mk_extract(sbits - 5 + too_short + 3, 0, sig_abs); + sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 4 + too_short + 3, sig_abs); sticky_h1_red = m_bv_util.mk_zero_extend(sbits + 5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red }; sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args); res_sig_1 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h1_f); - SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits - 4 + too_short); + SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits - 4 + too_short + 3); SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits + 6); SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits + 6); SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits + 6); SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits + 4); expr_ref sig_abs_h2(m), sticky_h2(m), sticky_h2_red(m), sig_abs_h2_f(m), res_sig_2(m); - sticky_h2 = m_bv_util.mk_extract(sbits - 4 + too_short, 0, sig_abs); - sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 3 + too_short, sig_abs); + sticky_h2 = m_bv_util.mk_extract(sbits - 4 + too_short + 3, 0, sig_abs); + sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 3 + too_short + 3, sig_abs); sticky_h2_red = m_bv_util.mk_zero_extend(sbits + 4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red }; sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args)); res_sig_2 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h2_f); - SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits - 3 + too_short); + SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits - 3 + too_short + 3); SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits + 5); SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits + 5); SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits + 6); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 6f61a78e9..ed97db721 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -840,16 +840,19 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co SASSERT(m_mpz_manager.lt(mr.significand(), m_powers2(2*x.sbits))); SASSERT(m_mpz_manager.ge(mr.significand(), m_powers2(2*x.sbits - 2))); - // Introduce extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2] - c.set(x.ebits+2, 2*x.sbits-1, c.sign(), c.exponent(), c.significand()); - m_mpz_manager.mul2k(c.significand(), x.sbits - 1); + // Introduce (sbits+3) extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2] + c.set(x.ebits+2, 2*x.sbits-1+3, c.sign(), c.exponent(), c.significand()); + m_mpz_manager.mul2k(c.significand(), x.sbits - 1 + 3); + // And + 3 bits into mr as well. + mr.set(x.ebits + 2, 2 * x.sbits - 1 + 3, mr.sign(), mr.exponent(), mr.significand()); + m_mpz_manager.mul2k(mr.significand(), 3); TRACE("mpf_dbg", tout << "C_= " << to_string(c) << std::endl; tout << "C_= " << to_string_binary(c, 1, 0) << std::endl;); - SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2*x.sbits))); + SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2*x.sbits + 3))); SASSERT(m_mpz_manager.is_zero(c.significand()) || - m_mpz_manager.ge(c.significand(), m_powers2(2*x.sbits - 2))); + m_mpz_manager.ge(c.significand(), m_powers2(2*x.sbits - 2 + 3))); if (exp(c) > exp(mr)) { TRACE("mpf_dbg", tout << "Swap!" << std::endl;); @@ -860,8 +863,8 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co mpf_exp_t exp_delta_w = exp(mr) - exp(c); SASSERT(exp(mr) >= exp(c) && exp_delta_w >= 0); - if (exp_delta_w > 2 * x.sbits) - exp_delta_w = 2 * x.sbits; + if (exp_delta_w > 2 * x.sbits + 3) + exp_delta_w = 2 * x.sbits + 3; unsigned exp_delta = (unsigned)exp_delta_w; @@ -905,8 +908,8 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co // Renormalize bool renorm_sticky = false; - SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1))); - if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits))) + SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1 + 3))); + if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3))) { SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI. @@ -919,7 +922,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co mpf_exp_t min_exp = mk_min_exp(x.ebits); unsigned sig_width = m_mpz_manager.prev_power_of_two(res.get().significand) + 1; - mpf_exp_t sig_lz = 2 * x.sbits - sig_width; + mpf_exp_t sig_lz = 2 * x.sbits + 3 - sig_width; mpf_exp_t max_exp_delta = res.exponent() - min_exp; unsigned renorm_delta = (unsigned) std::max((mpf_exp_t)0, std::min(sig_lz, max_exp_delta)); res.get().exponent -= renorm_delta; @@ -930,11 +933,11 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0)); if (x.sbits >= 4) { - m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4), o.significand, sticky_rem); + m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem); renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem); } else { - m_mpz_manager.mul2k(res.significand(), 4 - x.sbits, o.significand); + m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand); } if (renorm_sticky && m_mpz_manager.is_even(o.significand)) From 52cf80d63722ec6c322daa01c01fd7755306d9f8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 19:53:55 +0100 Subject: [PATCH 7/8] Simplified bit-vector bounds in fp.rem. Relates to #872. --- src/ast/fpa/fpa2bv_converter.cpp | 64 ++++++++++++++++---------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7e56df405..0f4d26739 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1535,12 +1535,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // Extend c expr_ref c_sig_ext(m); - c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits - 1 + 3))); + c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits+2))); c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); mul_sig = m_bv_util.mk_concat(mul_sig, m_bv_util.mk_numeral(0, 3)); - SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits + 3); - SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits+3); + SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2*sbits+3); dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext); dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext); @@ -1564,8 +1564,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(is_well_sorted(m, f_sig)); SASSERT(is_well_sorted(m, f_exp)); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits + 3); - SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+3); + SASSERT(m_bv_util.get_bv_size(f_sig) == 2*sbits+3); SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2); SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2); @@ -1595,7 +1595,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, shifted_big = m_bv_util.mk_bv_lshr( m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta)); - shifted_f_sig = m_bv_util.mk_extract(3*sbits-1+3, sbits, shifted_big); + shifted_f_sig = m_bv_util.mk_extract(3*sbits+2, sbits, shifted_big); alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get()); dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig); @@ -1613,14 +1613,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); dbg_decouple("fpa2bv_fma_eq_sgn", eq_sgn); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+2+3); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+5); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+5); dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); expr_ref sum(m), e_plus_f(m), e_minus_f(m), sticky_wide(m); - sticky_wide = m_bv_util.mk_zero_extend(2*sbits+1+3, alignment_sticky); + sticky_wide = m_bv_util.mk_zero_extend(2*sbits+4, alignment_sticky); e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); e_plus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_plus_f), zero_1), m_bv_util.mk_bv_add(e_plus_f, sticky_wide), @@ -1633,12 +1633,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig); m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); - SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+5); SASSERT(is_well_sorted(m, sum)); dbg_decouple("fpa2bv_fma_add_sum", sum); expr_ref sign_bv(m), n_sum(m); - sign_bv = m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+1+3, sum); + sign_bv = m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sum); n_sum = m_bv_util.mk_bv_neg(sum); dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); @@ -1662,14 +1662,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_res_sgn", res_sgn); expr_ref is_sig_neg(m); - is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+1+3, sig_abs)); + is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sig_abs)); sig_abs = m.mk_ite(is_sig_neg, m_bv_util.mk_bv_neg(sig_abs), sig_abs); dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg); // Result could have overflown into 4.xxx. - SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+4); expr_ref extra(m), extra_is_zero(m); - extra = m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+3, sig_abs); + extra = m_bv_util.mk_extract(2*sbits+4, 2*sbits+3, sig_abs); extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2)); dbg_decouple("fpa2bv_fma_extra", extra); @@ -1700,30 +1700,30 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, } expr_ref sig_abs_h1(m), sticky_h1(m), sticky_h1_red(m), sig_abs_h1_f(m), res_sig_1(m); - sticky_h1 = m_bv_util.mk_extract(sbits - 5 + too_short + 3, 0, sig_abs); - sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 4 + too_short + 3, sig_abs); - sticky_h1_red = m_bv_util.mk_zero_extend(sbits + 5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); + sticky_h1 = m_bv_util.mk_extract(sbits+too_short-2, 0, sig_abs); + sig_abs_h1 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits-1+too_short, sig_abs); + sticky_h1_red = m_bv_util.mk_zero_extend(sbits+5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red }; sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args); - res_sig_1 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h1_f); - SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits - 4 + too_short + 3); - SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits + 4); + res_sig_1 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h1_f); + SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits+too_short-1); + SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits+6); + SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits+6); + SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits+6); + SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits+4); expr_ref sig_abs_h2(m), sticky_h2(m), sticky_h2_red(m), sig_abs_h2_f(m), res_sig_2(m); - sticky_h2 = m_bv_util.mk_extract(sbits - 4 + too_short + 3, 0, sig_abs); - sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 3 + too_short + 3, sig_abs); - sticky_h2_red = m_bv_util.mk_zero_extend(sbits + 4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); + sticky_h2 = m_bv_util.mk_extract(sbits+too_short-1, 0, sig_abs); + sig_abs_h2 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits+too_short, sig_abs); + sticky_h2_red = m_bv_util.mk_zero_extend(sbits+4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red }; sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args)); - res_sig_2 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h2_f); - SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits - 3 + too_short + 3); - SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits + 5); - SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits + 5); - SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits + 4); + res_sig_2 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h2_f); + SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits+too_short); + SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits+5); + SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits+5); + SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits+6); + SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits+4); res_sig = m.mk_ite(extra_is_zero, res_sig_1, res_sig_2); From 507356c7bf6aa472abb1625a9a24465aeb9c9667 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 20:18:39 +0100 Subject: [PATCH 8/8] Fixed bug in fpa2bv converter. Fixes #1178. --- src/ast/fpa/fpa2bv_converter.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 0f4d26739..c84b2a691 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2714,12 +2714,12 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con SASSERT(m_util.is_bv2rm(args[0])); expr * bv_rm = to_app(args[0])->get_arg(0); - rational e; - if (!m_arith_util.is_numeral(args[1], e)) + rational q; + if (!m_arith_util.is_numeral(args[1], q)) UNREACHABLE(); - rational q; - if (!m_arith_util.is_numeral(args[2], q)) + rational e; + if (!m_arith_util.is_numeral(args[2], e)) UNREACHABLE(); SASSERT(e.is_int64());