diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 622c7cf94..560ee5885 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -319,8 +319,8 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < (int)tok.size()){ + size_t eqpos = tok.find('='); + if(eqpos >= 0 && eqpos < tok.size()){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; @@ -377,8 +377,8 @@ extern "C" { #else - static Z3_ast and_vec(Z3_context ctx,std::vector &c){ - return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; + static Z3_ast and_vec(Z3_context ctx,svector &c){ + return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; } static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){ @@ -395,15 +395,15 @@ extern "C" { } } else { - std::vector > chs(num); + std::vector > chs(num); for(int i = 0; i < num-1; i++){ - std::vector &c = chs[i]; + svector &c = chs[i]; c.push_back(cnsts[i]); Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c)); chs[parents[i]].push_back(foo); } { - std::vector &c = chs[num-1]; + svector &c = chs[num-1]; c.push_back(cnsts[num-1]); res = and_vec(ctx,c); } @@ -468,7 +468,7 @@ extern "C" { static std::string read_msg; static std::vector read_theory; - static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector &assertions){ + static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ read_error.clear(); try { std::string foo(filename); @@ -510,26 +510,26 @@ extern "C" { hash_map file_params; get_file_params(filename,file_params); - - int num_theory = 0; + + unsigned num_theory = 0; if(file_params.find("THEORY") != file_params.end()) num_theory = atoi(file_params["THEORY"].c_str()); - std::vector assertions; + svector assertions; if(!iZ3_parse(ctx,filename,error,assertions)) return false; - if(num_theory > (int)assertions.size()) - num_theory = assertions.size(); - int num = assertions.size() - num_theory; + if(num_theory > assertions.size()) + num_theory = assertions.size(); + unsigned num = assertions.size() - num_theory; read_cnsts.resize(num); read_parents.resize(num); read_theory.resize(num_theory); - for(int j = 0; j < num_theory; j++) + for(unsigned j = 0; j < num_theory; j++) read_theory[j] = assertions[j]; - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_cnsts[j] = assertions[j+num_theory]; if(ret_num_theory) @@ -543,12 +543,12 @@ extern "C" { return true; } - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_parents[j] = SHRT_MAX; hash_map pred_map; - for(int j = 0; j < num; j++){ + for(unsigned j = 0; j < num; j++){ Z3_ast lhs = 0, rhs = read_cnsts[j]; if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){ @@ -602,7 +602,7 @@ extern "C" { } } - for(int j = 0; j < num-1; j++) + for(unsigned j = 0; j < num-1; j++) if(read_parents[j] == SHRT_MIN){ read_error << "formula " << j+1 << ": unreferenced"; goto fail; diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 7615308b7..2dd0dd75a 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -35,7 +35,7 @@ public class BitVecNum extends BitVecExpr { Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int64"); + throw new Z3Exception("Numeral is not a long"); return res.value; } diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 22ec30ad2..959566619 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6424,7 +6424,7 @@ class Tactic: _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected") goal = _to_goal(goal) if len(arguments) > 0 or len(keywords) > 0: - p = args2params(arguments, keywords, a.ctx) + p = args2params(arguments, keywords, self.ctx) return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx) else: return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx) diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 85e0cc791..41c43b26c 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { // otherwise t2 is also a quantifier. return true; } - UNREACHABLE(); + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_DER: { @@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { match_fact(p, fact) && match_iff(fact.get(), t1, t2) && match_quantifier(t1, is_forall, decls1, body1) && - is_forall && - match_or(body1.get(), terms1)) { + is_forall) { // TBD: check that terms are set of equalities. // t2 is an instance of a predicate in terms1 return true; - } - UNREACHABLE(); + } + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_HYPOTHESIS: { @@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { } else { IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << - mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";); + mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";); } fmls[i] = premise1; } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index eaef956b7..4b7d47e0f 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -19,6 +19,7 @@ Revision History: --*/ + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 9f77934e5..7593e9a52 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -475,10 +475,11 @@ namespace smt { bool theory_arith::all_coeff_int(row const & r) const { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) + for (; it != end; ++it) { + if (!it->is_dead() && !it->m_coeff.is_int()) { TRACE("gomory_cut", display_row(tout, r, true);); return false; + } } return true; } diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 011169496..ebccf4d52 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1588,8 +1588,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * v2 = x; unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(ebits < sbits); + unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); @@ -1619,9 +1618,22 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * expr_ref shift(m), r_shifted(m), l_shifted(m); shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits-1, ebits+1), m_bv_util.mk_sign_extend(1, a_exp)); - r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-ebits-1, shift)); + if (sbits > (ebits+1)) + r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift)); + else if (sbits < (ebits+1)) + r_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(ebits+1-sbits, a_sig), shift)); + else // sbits == ebits+1 + r_shifted = m_bv_util.mk_bv_lshr(a_sig, shift); + SASSERT(is_well_sorted(m, r_shifted)); SASSERT(m_bv_util.get_bv_size(r_shifted) == sbits); - l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-ebits-1, shift)); + + if (sbits > (ebits+1)) + l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift)); + else if (sbits < (ebits+1)) + l_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+1-sbits, r_shifted), shift)); + else // sbits == ebits+1 + l_shifted = m_bv_util.mk_bv_shl(r_shifted, shift); + SASSERT(is_well_sorted(m, l_shifted)); SASSERT(m_bv_util.get_bv_size(l_shifted) == sbits); res_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), @@ -1825,146 +1837,158 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a mk_triple(args[0], args[1], args[2], result); } else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { - // We also support float to float conversion + // We also support float to float conversion + sort * s = f->get_range(); expr_ref rm(m), x(m); rm = args[0]; x = args[1]; - - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); - expr_ref one1(m); - one1 = m_bv_util.mk_numeral(1, 1); - expr_ref ninf(m), pinf(m); - mk_plus_inf(f, pinf); - mk_minus_inf(f, ninf); - - // NaN -> NaN - mk_is_nan(x, c1); - mk_nan(f, v1); - - // +0 -> +0 - mk_is_pzero(x, c2); - mk_pzero(f, v2); - - // -0 -> -0 - mk_is_nzero(x, c3); - mk_nzero(f, v3); - - // +oo -> +oo - mk_is_pinf(x, c4); - v4 = pinf; - - // -oo -> -oo - mk_is_ninf(x, c5); - v5 = ninf; - - // otherwise: the actual conversion with rounding. - sort * s = f->get_range(); - expr_ref sgn(m), sig(m), exp(m), lz(m); - unpack(x, sgn, sig, exp, lz, true); - - dbg_decouple("fpa2bv_to_float_x_sig", sig); - dbg_decouple("fpa2bv_to_float_x_exp", exp); - dbg_decouple("fpa2bv_to_float_lz", lz); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - - res_sgn = sgn; - - unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1])); - unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1])); + unsigned from_sbits = m_util.get_sbits(m.get_sort(x)); + unsigned from_ebits = m_util.get_ebits(m.get_sort(x)); unsigned to_sbits = m_util.get_sbits(s); unsigned to_ebits = m_util.get_ebits(s); - SASSERT(m_bv_util.get_bv_size(sgn) == 1); - SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); - SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); - SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); + if (from_sbits == to_sbits && from_ebits == to_ebits) + result = x; + else { + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); + expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); + expr_ref one1(m); - if (from_sbits < (to_sbits + 3)) - { - // make sure that sig has at least to_sbits + 3 - res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits)); - } - else if (from_sbits > (to_sbits + 3)) - { - // collapse the extra bits into a sticky bit. - 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); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); - res_sig = m_bv_util.mk_concat(high, sticky); - } - else - res_sig = sig; + one1 = m_bv_util.mk_numeral(1, 1); + expr_ref ninf(m), pinf(m); + mk_plus_inf(f, pinf); + mk_minus_inf(f, ninf); - res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder. - unsigned sig_sz = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_sz == to_sbits+4); + // NaN -> NaN + mk_is_nan(x, c1); + mk_nan(f, v1); - expr_ref exponent_overflow(m); - exponent_overflow = m.mk_false(); + // +0 -> +0 + mk_is_pzero(x, c2); + mk_pzero(f, v2); - if (from_ebits < (to_ebits + 2)) - { - res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp); - } - else if (from_ebits > (to_ebits + 2)) - { - 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); + // -0 -> -0 + mk_is_nzero(x, c3); + mk_nzero(f, v3); + + // +oo -> +oo + mk_is_pinf(x, c4); + v4 = pinf; + + // -oo -> -oo + mk_is_ninf(x, c5); + v5 = ninf; - 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()); + // otherwise: the actual conversion with rounding. + expr_ref sgn(m), sig(m), exp(m), lz(m); + unpack(x, sgn, sig, exp, lz, true); - zero1 = m_bv_util.mk_numeral(0, 1); - 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); + dbg_decouple("fpa2bv_to_float_x_sig", sig); + dbg_decouple("fpa2bv_to_float_x_exp", exp); + dbg_decouple("fpa2bv_to_float_lz", lz); + + expr_ref res_sgn(m), res_sig(m), res_exp(m); + + res_sgn = sgn; + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); + SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); + SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); + + if (from_sbits < (to_sbits + 3)) + { + // make sure that sig has at least to_sbits + 3 + res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits)); + } + else if (from_sbits > (to_sbits + 3)) + { + // collapse the extra bits into a sticky bit. + 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); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); + res_sig = m_bv_util.mk_concat(high, sticky); + } + else + res_sig = sig; + + res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder. + unsigned sig_sz = m_bv_util.get_bv_size(res_sig); + SASSERT(sig_sz == to_sbits+4); + + expr_ref exponent_overflow(m); + exponent_overflow = m.mk_false(); + + if (from_ebits < (to_ebits + 2)) + { + res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp); + + // subtract lz for subnormal numbers. + expr_ref lz_ext(m); + lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz); + res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); + } + else if (from_ebits > (to_ebits + 2)) + { + 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); - expr_ref c2(m); - 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); + 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, 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); - // Note: Upon overflow, we _could_ try to shift the significand around... + expr_ref c2(m); + 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... - res_exp = low; - } - else - res_exp = exp; + // subtract lz for subnormal numbers. + expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m); + lz_ext = m_bv_util.mk_extract(to_ebits+1, 0, lz); + lz_rest = m_bv_util.mk_extract(from_ebits-1, to_ebits+2, lz); + lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); + m_simp.mk_eq(lz_redor, one1, lz_redor_bool); + m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); - // subtract lz for subnormal numbers. - expr_ref lz_ext(m); - lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz); - res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); - SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + res_exp = m_bv_util.mk_bv_sub(low, lz_ext); + } + else // from_ebits == (to_ebits + 2) + res_exp = m_bv_util.mk_bv_sub(exp, lz); - dbg_decouple("fpa2bv_to_float_res_sig", res_sig); - dbg_decouple("fpa2bv_to_float_res_exp", res_exp); + SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + SASSERT(is_well_sorted(m, res_exp)); - expr_ref rounded(m); - round(s, rm, res_sgn, res_sig, res_exp, rounded); - + dbg_decouple("fpa2bv_to_float_res_sig", res_sig); + dbg_decouple("fpa2bv_to_float_res_exp", res_exp); - expr_ref is_neg(m), sig_inf(m); - m_simp.mk_eq(sgn, one1, is_neg); - mk_ite(is_neg, ninf, pinf, sig_inf); + expr_ref rounded(m); + round(s, rm, res_sgn, res_sig, res_exp, rounded); + + expr_ref is_neg(m), sig_inf(m); + m_simp.mk_eq(sgn, one1, is_neg); + mk_ite(is_neg, ninf, pinf, sig_inf); - dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); + dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); + mk_ite(exponent_overflow, sig_inf, rounded, v6); - mk_ite(exponent_overflow, sig_inf, rounded, v6); - - // And finally, we tie them together. - mk_ite(c5, v5, v6, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); + // And finally, we tie them together. + mk_ite(c5, v5, v6, result); + mk_ite(c4, v4, result, result); + mk_ite(c3, v3, result, result); + mk_ite(c2, v2, result, result); + mk_ite(c1, v1, result, result); + } } else { // .. other than that, we only support rationals for asFloat @@ -2167,14 +2191,14 @@ void fpa2bv_converter::mk_bot_exp(unsigned sz, expr_ref & result) { } void fpa2bv_converter::mk_min_exp(unsigned ebits, expr_ref & result) { - SASSERT(ebits > 0); + SASSERT(ebits >= 2); const mpz & z = m_mpf_manager.m_powers2.m1(ebits-1, true); result = m_bv_util.mk_numeral(z + mpz(1), ebits); } void fpa2bv_converter::mk_max_exp(unsigned ebits, expr_ref & result) { - SASSERT(ebits > 0); - result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits); + SASSERT(ebits >= 2); + result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits); } void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result) { @@ -2220,14 +2244,14 @@ void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) { unsigned ebits = m_bv_util.get_bv_size(e); SASSERT(ebits >= 2); - expr_ref mask(m); - mask = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits); - result = m_bv_util.mk_bv_add(e, mask); + expr_ref bias(m); + bias = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits); + result = m_bv_util.mk_bv_add(e, bias); } void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { unsigned ebits = m_bv_util.get_bv_size(e); - SASSERT(ebits >= 2); + SASSERT(ebits >= 3); expr_ref e_plus_one(m); e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits)); @@ -2263,6 +2287,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref expr_ref denormal_sig(m), denormal_exp(m); denormal_sig = m_bv_util.mk_zero_extend(1, sig); + SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0. denormal_exp = m_bv_util.mk_numeral(1, ebits); mk_unbias(denormal_exp, denormal_exp); dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); @@ -2436,13 +2461,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)); t = m_bv_util.mk_bv_sub(t, lz); t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); - expr_ref TINY(m); + dbg_decouple("fpa2bv_rnd_t", t); + expr_ref TINY(m); TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2)); - - TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); - SASSERT(is_well_sorted(m, TINY)); - dbg_decouple("fpa2bv_rnd_TINY", TINY); + TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); + SASSERT(is_well_sorted(m, TINY)); expr_ref beta(m); beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2)); @@ -2455,7 +2479,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & dbg_decouple("fpa2bv_rnd_e_min", e_min); dbg_decouple("fpa2bv_rnd_e_max", e_max); - expr_ref sigma(m), sigma_add(m), e_min_p2(m); + expr_ref sigma(m), sigma_add(m); sigma_add = m_bv_util.mk_bv_sub(exp, m_bv_util.mk_sign_extend(2, e_min)); sigma_add = m_bv_util.mk_bv_add(sigma_add, m_bv_util.mk_numeral(1, ebits+2)); m_simp.mk_ite(TINY, sigma_add, lz, sigma); @@ -2477,9 +2501,10 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m); sigma_neg = m_bv_util.mk_bv_neg(sigma); sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size); - sigma_le_cap = m_bv_util.mk_sle(sigma_neg, sigma_cap); + sigma_le_cap = m_bv_util.mk_ule(sigma_neg, sigma_cap); m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); + dbg_decouple("fpa2bv_rnd_sigma_cap", sigma_cap); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size)); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 735d21c99..5910f55c9 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -360,6 +360,8 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode mk_inf(ebits, sbits, x.sign, o); else if (is_zero(x)) mk_zero(ebits, sbits, x.sign, o); + else if (x.ebits == ebits && x.sbits == sbits) + set(o, x); else { set(o, x); unpack(o, true); @@ -1378,12 +1380,12 @@ bool mpf_manager::has_top_exp(mpf const & x) { } mpf_exp_t mpf_manager::mk_bot_exp(unsigned ebits) { - SASSERT(ebits > 0); + SASSERT(ebits >= 2); return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, true)); } mpf_exp_t mpf_manager::mk_top_exp(unsigned ebits) { - SASSERT(ebits > 0); + SASSERT(ebits >= 2); return m_mpz_manager.get_int64(m_powers2(ebits-1)); }