diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 876e3cff5..bbf27d25d 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -149,7 +149,7 @@ extern "C" { LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_minus_inf(to_sort(s)) : ctx->float_util().mk_plus_inf(to_sort(s))); + Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_ninf(to_sort(s)) : ctx->float_util().mk_pinf(to_sort(s))); RETURN_Z3(r); Z3_CATCH_RETURN(0); } diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 625ed9ade..816df906e 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -163,6 +163,11 @@ decl_plugin * float_decl_plugin::mk_fresh() { } sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { + if (ebits > sbits) + m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported"); + if (ebits <= 2) + m_manager->raise_exception("floating point sorts with ebits <= 2 are currently not supported"); + parameter p1(ebits), p2(sbits); parameter ps[2] = { p1, p2 }; sort_size sz; @@ -841,13 +846,13 @@ app * float_util::mk_nan(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * float_util::mk_plus_inf(unsigned ebits, unsigned sbits) { +app * float_util::mk_pinf(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_pinf(ebits, sbits, v); return mk_value(v); } -app * float_util::mk_minus_inf(unsigned ebits, unsigned sbits) { +app * float_util::mk_ninf(unsigned ebits, unsigned sbits) { scoped_mpf v(fm()); fm().mk_ninf(ebits, sbits, v); return mk_value(v); diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index bd180c45c..ebf424578 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -221,11 +221,11 @@ public: app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_ZERO); } app * mk_nan(unsigned ebits, unsigned sbits); - app * mk_plus_inf(unsigned ebits, unsigned sbits); - app * mk_minus_inf(unsigned ebits, unsigned sbits); + app * mk_pinf(unsigned ebits, unsigned sbits); + app * mk_ninf(unsigned ebits, unsigned sbits); app * mk_nan(sort * s) { return mk_nan(get_ebits(s), get_sbits(s)); } - app * mk_plus_inf(sort * s) { return mk_plus_inf(get_ebits(s), get_sbits(s)); } - app * mk_minus_inf(sort * s) { return mk_minus_inf(get_ebits(s), get_sbits(s)); } + app * mk_pinf(sort * s) { return mk_pinf(get_ebits(s), get_sbits(s)); } + app * mk_ninf(sort * s) { return mk_ninf(get_ebits(s), get_sbits(s)); } app * mk_value(mpf const & v) { return m_plugin->mk_value(v); } bool is_value(expr * n) { return m_plugin->is_value(n); } @@ -238,8 +238,8 @@ public: app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); } bool is_nan(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nan(v); } - bool is_plus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); } - bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); } + bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); } + bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); } bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); } bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index afad59dff..be951098a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -103,9 +103,9 @@ void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args mk_nan(f, result); else if (m_util.fm().is_inf(v)) { if (m_util.fm().sgn(v)) - mk_minus_inf(f, result); + mk_ninf(f, result); else - mk_plus_inf(f, result); + mk_pinf(f, result); } else { expr_ref bv_sgn(m), bv_sig(m), e(m), biased_exp(m); @@ -298,7 +298,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { } } -void fpa2bv_converter::mk_plus_inf(func_decl * f, expr_ref & result) { +void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) { sort * srt = f->get_range(); SASSERT(is_float(srt)); unsigned sbits = m_util.get_sbits(srt); @@ -311,7 +311,7 @@ void fpa2bv_converter::mk_plus_inf(func_decl * f, expr_ref & result) { result); } -void fpa2bv_converter::mk_minus_inf(func_decl * f, expr_ref & result) { +void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) { sort * srt = f->get_range(); SASSERT(is_float(srt)); unsigned sbits = m_util.get_sbits(srt); @@ -633,8 +633,8 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, mk_nan(f, nan); mk_nzero(f, nzero); mk_pzero(f, pzero); - mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_ninf(f, ninf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); @@ -781,8 +781,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, mk_nan(f, nan); mk_nzero(f, nzero); mk_pzero(f, pzero); - mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_ninf(f, ninf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); @@ -927,8 +927,8 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, mk_nan(f, nan); mk_nzero(f, nzero); mk_pzero(f, pzero); - mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_ninf(f, ninf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); @@ -1137,8 +1137,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, mk_nan(f, nan); mk_nzero(f, nzero); mk_pzero(f, pzero); - mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_ninf(f, ninf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); @@ -1447,8 +1447,8 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, mk_nan(f, nan); mk_nzero(f, nzero); mk_pzero(f, pzero); - mk_minus_inf(f, ninf); - mk_plus_inf(f, pinf); + mk_ninf(f, ninf); + mk_pinf(f, pinf); expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); mk_is_nan(x, x_is_nan); @@ -1871,9 +1871,11 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args mk_triple(args[0], args[1], args[2], result); } else if (num == 2 && - m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[0]) && + m_bv_util.get_bv_size(args[0]) == 3 && m_bv_util.is_bv(args[1])) { + mk_to_fp_signed(f, num, args, result); } else if (num == 3 && @@ -1968,8 +1970,8 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args one1 = m_bv_util.mk_numeral(1, 1); expr_ref ninf(m), pinf(m); - mk_plus_inf(f, pinf); - mk_minus_inf(f, ninf); + mk_pinf(f, pinf); + mk_ninf(f, ninf); // NaN -> NaN mk_is_nan(x, c1); @@ -2152,38 +2154,146 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); - - // This is meant to be a conversion from signed bitvector to float: + + // This is a conversion from signed bitvector to float: // ; from signed machine integer, represented as a 2's complement bit vector // ((_ to_fp eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb)) - - - // Semantics: - //((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)): + // Semantics: // Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format). // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite // number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite - // number such that [[fp.to_real]](y) is closest to n according to rounding mode r. - - NOT_IMPLEMENTED_YET(); + // number such that [[fp.to_real]](y) is closest to n according to rounding mode r. + SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - unsigned sz = sbits + ebits; - SASSERT(m_bv_util.get_bv_size(args[0]) == 3); - SASSERT(m_bv_util.get_bv_size(args[1]) == sz); + SASSERT(m_bv_util.is_bv(args[0])); + SASSERT(m_bv_util.is_bv(args[1])); expr_ref rm(m), x(m); rm = args[0]; x = args[1]; - expr_ref sgn(m), sig(m), exp(m); - sgn = m_bv_util.mk_extract(sz - 1, sz - 1, x); - sig = m_bv_util.mk_extract(sz - ebits - 2, 0, x); - exp = m_bv_util.mk_extract(sz - 2, sz - ebits - 1, x); + dbg_decouple("fpa2bv_to_fp_signed_x", x); - round(f->get_range(), rm, sgn, sig, exp, result); + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned f_sz = sbits + ebits; + unsigned bv_sz = m_bv_util.get_bv_size(x); + SASSERT(m_bv_util.get_bv_size(rm) == 3); + + //if (bv_sz < f_sz) { + // x = m_bv_util.mk_zero_extend(f_sz - bv_sz, x); + // bv_sz = f_sz; + //} + + expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m); + bv0_1 = m_bv_util.mk_numeral(0, 1); + bv1_1 = m_bv_util.mk_numeral(1, 1); + bv0_sz = m_bv_util.mk_numeral(0, bv_sz); + bv1_sz = m_bv_util.mk_numeral(1, bv_sz); + + expr_ref is_zero(m), nzero(m), pzero(m), ninf(m), pinf(m); + is_zero = m.mk_eq(x, bv0_sz); + mk_nzero(f, nzero); + mk_pzero(f, pzero); + mk_ninf(f, ninf); + mk_pinf(f, pinf); + + // Special case: x == 0 -> p/n zero + expr_ref c1(m), v1(m), rm_is_to_neg(m); + c1 = is_zero; + mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + mk_ite(rm_is_to_neg, nzero, pzero, v1); + + // Special case: x != 0 + expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m); + expr_ref is_neg(m), x_abs(m); + is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x); + is_neg = m.mk_eq(is_neg_bit, bv1_1); + x_abs = m.mk_ite(is_neg, m_bv_util.mk_bv_neg(x), x); + dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg); + // x_abs has an extra bit in the front. + // x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2) + // bv_sz-2 is the "1.0" bit for the rounder. + + expr_ref lz(m), e_bv_sz(m), e_rest_sz(m); + mk_leading_zeros(x_abs, bv_sz, lz); + e_bv_sz = m_bv_util.mk_numeral(bv_sz, bv_sz); + e_rest_sz = m_bv_util.mk_bv_sub(e_bv_sz, lz); + SASSERT(m_bv_util.get_bv_size(lz) == m_bv_util.get_bv_size(e_bv_sz)); + dbg_decouple("fpa2bv_to_fp_signed_lz", lz); + expr_ref shifted_sig(m); + shifted_sig = m_bv_util.mk_bv_shl(x_abs, lz); + + expr_ref sticky(m); + // shifted_sig is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2) * 2^(-lz) + unsigned sig_sz = sbits + 4; // we want extra rounding bits. + if (sig_sz <= bv_sz) { + expr_ref sig_rest(m); + sig_4 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - sig_sz + 1, shifted_sig); // one short + sig_rest = m_bv_util.mk_extract(bv_sz - sig_sz, 0, shifted_sig); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest); + sig_4 = m_bv_util.mk_concat(sig_4, sticky); + } + else { + unsigned extra_bits = sig_sz - bv_sz; + expr_ref extra_zeros(m); + extra_zeros = m_bv_util.mk_numeral(0, extra_bits); + sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros); + lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz), + m_bv_util.mk_numeral(extra_bits, sig_sz)); + bv_sz = bv_sz + extra_bits; + SASSERT(is_well_sorted(m, lz)); + } + SASSERT(m_bv_util.get_bv_size(sig_4) == sig_sz); + + expr_ref s_exp(m), exp_rest(m); + s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz); + // s_exp = (bv_sz-2) + (-lz) signed + SASSERT(m_bv_util.get_bv_size(s_exp) == bv_sz); + + unsigned exp_sz = ebits + 2; // (+2 for rounder) + exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp); + // the remaining bits are 0 if ebits is large enough. + exp_too_large = m.mk_false(); // This is always in range. + + // The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits. + // exp < bv_sz (+sign bit which is [0]) + unsigned exp_worst_case_sz = (unsigned)((log(bv_sz) / log(2)) + 1); + + if (exp_sz < exp_worst_case_sz) { + // exp_sz < exp_worst_case_sz and exp >= 0. + // Take the maximum legal exponent; this + // allows us to keep the most precision. + expr_ref max_exp(m), max_exp_bvsz(m); + mk_max_exp(exp_sz, max_exp); + max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp); + + exp_too_large = m_bv_util.mk_ule(m_bv_util.mk_bv_add( + max_exp_bvsz, + m_bv_util.mk_numeral(1, bv_sz)), + s_exp); + sig_4 = m.mk_ite(exp_too_large, m_bv_util.mk_numeral(0, sig_sz), sig_4); + exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2); + } + dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large); + + expr_ref sgn(m), sig(m), exp(m); + sgn = is_neg_bit; + sig = sig_4; + exp = exp_2; + + dbg_decouple("fpa2bv_to_fp_signed_sgn", sgn); + dbg_decouple("fpa2bv_to_fp_signed_sig", sig); + dbg_decouple("fpa2bv_to_fp_signed_exp", exp); + + SASSERT(m_bv_util.get_bv_size(sig) == sbits + 4); + SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); + + expr_ref v2(m); + round(f->get_range(), rm, sgn, sig, exp, v2); + + mk_ite(c1, v1, v2, result); } void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2538,7 +2648,7 @@ void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) { void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { unsigned ebits = m_bv_util.get_bv_size(e); - SASSERT(ebits >= 3); + SASSERT(ebits >= 2); expr_ref e_plus_one(m); e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits)); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index e83754e38..eb4435132 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -86,8 +86,8 @@ public: void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_var(unsigned base_inx, sort * srt, expr_ref & result); - void mk_plus_inf(func_decl * f, expr_ref & result); - void mk_minus_inf(func_decl * f, expr_ref & result); + void mk_pinf(func_decl * f, expr_ref & result); + void mk_ninf(func_decl * f, expr_ref & result); void mk_nan(func_decl * f, expr_ref & result); void mk_nzero(func_decl *f, expr_ref & result); void mk_pzero(func_decl *f, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index a5ff8f5ca..bb42bdf5d 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -113,8 +113,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_RM_TOWARD_POSITIVE: case OP_FLOAT_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE; - case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE; - case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE; + case OP_FLOAT_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; + case OP_FLOAT_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE; diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 583268c34..3c1f51990 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -205,14 +205,14 @@ br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) { result = arg1; return BR_DONE; } - if (m_util.is_plus_inf(arg1)) { + if (m_util.is_pinf(arg1)) { // - +oo --> -oo - result = m_util.mk_minus_inf(m().get_sort(arg1)); + result = m_util.mk_ninf(m().get_sort(arg1)); return BR_DONE; } - if (m_util.is_minus_inf(arg1)) { + if (m_util.is_ninf(arg1)) { // - -oo -> +oo - result = m_util.mk_plus_inf(m().get_sort(arg1)); + result = m_util.mk_pinf(m().get_sort(arg1)); return BR_DONE; } if (m_util.is_neg(arg1)) { @@ -366,22 +366,22 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { result = m().mk_false(); return BR_DONE; } - if (m_util.is_minus_inf(arg1)) { + if (m_util.is_ninf(arg1)) { // -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2)); return BR_REWRITE3; } - if (m_util.is_minus_inf(arg2)) { + if (m_util.is_ninf(arg2)) { // arg1 < -oo --> false result = m().mk_false(); return BR_DONE; } - if (m_util.is_plus_inf(arg1)) { + if (m_util.is_pinf(arg1)) { // +oo < arg2 --> false result = m().mk_false(); return BR_DONE; } - if (m_util.is_plus_inf(arg2)) { + if (m_util.is_pinf(arg2)) { // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1)); return BR_REWRITE3; diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index c555b71f1..fce54aaa4 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -1492,11 +1492,11 @@ namespace nlarith { } fml = mk_and(equivs.size(), equivs.c_ptr()); } - void mk_plus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { + void mk_pinf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { plus_inf_subst sub(*this); mk_inf_sign(sub, literals, fml, new_atoms); } - void mk_minus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { + void mk_ninf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) { minus_inf_subst sub(*this); mk_inf_sign(sub, literals, fml, new_atoms); } @@ -1704,10 +1704,10 @@ namespace nlarith { app_ref fml(m()); app_ref_vector new_atoms(m()); if (is_pos) { - mk_plus_inf_sign(literals, fml, new_atoms); + mk_pinf_sign(literals, fml, new_atoms); } else { - mk_minus_inf_sign(literals, fml, new_atoms); + mk_ninf_sign(literals, fml, new_atoms); } simple_branch* br = alloc(simple_branch, m(), fml); swap_atoms(br, literals.lits(), new_atoms); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 26ee88226..7552e276b 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -49,6 +49,24 @@ namespace smt { { } + void theory_fpa::add_extra_assertions() + { + ast_manager & m = get_manager(); + context & ctx = get_context(); + simplifier & simp = ctx.get_simplifier(); + + expr_ref_vector::iterator it = m_converter.extra_assertions.begin(); + expr_ref_vector::iterator end = m_converter.extra_assertions.end(); + for (; it != end; it++) { + expr_ref t(m); + proof_ref t_pr(m); + simp(*it, t, t_pr); + TRACE("t_fpa", tout << "extra: " << mk_ismt2_pp(t, m) << "\n";); + ctx.internalize_assertion(t, t_pr, 0); + } + m_converter.extra_assertions.reset(); + } + void theory_fpa::mk_bv_eq(expr * x, expr * y) { SASSERT(get_sort(x)->get_family_id() == m_converter.bu().get_family_id()); SASSERT(get_sort(y)->get_family_id() == m_converter.bu().get_family_id()); @@ -94,6 +112,8 @@ namespace smt { ctx.mk_th_axiom(get_id(), ~l, def); } + add_extra_assertions(); + return true; } @@ -134,7 +154,7 @@ namespace smt { simp(a->get_arg(1), sig, pr_sig); simp(a->get_arg(2), exp, pr_exp); - m_converter.mk_triple(sgn, sig, exp, bv_term); + m_converter.mk_triple(sgn, sig, exp, bv_term); } else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV || term->get_decl_kind() == OP_FLOAT_TO_REAL) { @@ -149,7 +169,9 @@ namespace smt { TRACE("t_fpa", tout << "converted: " << mk_ismt2_pp(bv_term, get_manager()) << "\n";); SASSERT(!m_trans_map.contains(term)); - m_trans_map.insert(term, bv_term, 0); + m_trans_map.insert(term, bv_term, 0); + + add_extra_assertions(); enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true); theory_var v = mk_var(e); @@ -176,11 +198,15 @@ namespace smt { m_rw(owner, converted); simp(converted, converted, pr); m_trans_map.insert(owner, converted, 0); + + add_extra_assertions(); sort * owner_sort = m.get_sort(owner); if (m_converter.is_rm(owner_sort)) { bv_util & bu = m_converter.bu(); - bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted))); + expr_ref t(m); + t = bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted))); + ctx.internalize_assertion(t, proof_ref(m), 0); } TRACE("t_fpa", tout << "new theory var (const): " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";); @@ -191,7 +217,8 @@ namespace smt { TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";); ast_manager & m = get_manager(); context & ctx = get_context(); - + float_util & fu = m_converter.fu(); + app * ax = get_enode(x)->get_owner(); app * ay = get_enode(y)->get_owner(); expr * ex, *ey; @@ -199,7 +226,7 @@ namespace smt { m_trans_map.get(ax, ex, px); m_trans_map.get(ay, ey, py); - if (m_converter.fu().is_float(get_enode(x)->get_owner())) { + if (fu.is_float(get_enode(x)->get_owner())) { expr * sgn_x, *sig_x, *exp_x; expr * sgn_y, *sig_y, *exp_y; split_triple(ex, sgn_x, sig_x, exp_x); @@ -209,7 +236,7 @@ namespace smt { mk_bv_eq(sig_x, sig_y); mk_bv_eq(exp_x, exp_y); } - else if (m_converter.fu().is_rm(get_enode(x)->get_owner())) { + else if (fu.is_rm(get_enode(x)->get_owner())) { mk_bv_eq(ex, ey); } else @@ -220,7 +247,8 @@ namespace smt { TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << "\n";); ast_manager & m = get_manager(); context & ctx = get_context(); - + float_util & fu = m_converter.fu(); + app * ax = get_enode(x)->get_owner(); app * ay = get_enode(y)->get_owner(); expr * ex, *ey; @@ -230,7 +258,7 @@ namespace smt { expr_ref deq(m); - if (m_converter.fu().is_float(m.get_sort(get_enode(x)->get_owner()))) { + if (fu.is_float(m.get_sort(get_enode(x)->get_owner()))) { expr * sgn_x, *sig_x, *exp_x; expr * sgn_y, *sig_y, *exp_y; split_triple(ex, sgn_x, sig_x, exp_x); @@ -240,7 +268,7 @@ namespace smt { m.mk_not(m.mk_eq(sig_x, sig_y)), m.mk_not(m.mk_eq(exp_x, exp_y))); } - else if (m_converter.fu().is_rm(m.get_sort(get_enode(x)->get_owner()))) { + else if (fu.is_rm(m.get_sort(get_enode(x)->get_owner()))) { deq = m.mk_not(m.mk_eq(ex, ey)); } else @@ -317,67 +345,65 @@ namespace smt { split_triple(bv_e, bv_sgn, bv_sig, bv_exp); family_id fid = m.get_family_id("bv"); - theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid); + theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid); app * e_sgn, *e_sig, *e_exp; - unsigned exp_sz = fpa_e_srt->get_parameter(0).get_int(); + unsigned ebits = fpa_e_srt->get_parameter(0).get_int(); + unsigned sbits = fpa_e_srt->get_parameter(1).get_int(); unsigned sig_sz = fpa_e_srt->get_parameter(1).get_int() - 1; + rational bias = mpfm.m_powers2.m1(ebits - 1); + rational sgn_r(0), sig_r(0), exp_r(bias); + e_sgn = (ctx.e_internalized(bv_sgn)) ? ctx.get_enode(bv_sgn)->get_owner() : - m_converter.bu().mk_numeral(0, 1); + bu.mk_numeral(0, 1); e_sig = (ctx.e_internalized(bv_sig)) ? ctx.get_enode(bv_sig)->get_owner() : - m_converter.bu().mk_numeral(0, sig_sz); + bu.mk_numeral(0, sig_sz); e_exp = (ctx.e_internalized(bv_exp)) ? ctx.get_enode(bv_exp)->get_owner() : - m_converter.bu().mk_numeral(0, exp_sz); + bu.mk_numeral(bias, ebits); TRACE("t_fpa", tout << "bv rep: [" << mk_ismt2_pp(e_sgn, m) << "\n" << mk_ismt2_pp(e_sig, m) << "\n" - << mk_ismt2_pp(e_exp, m) << "]\n";); - - rational sgn_r(0), sig_r(0), exp_r(0); + << mk_ismt2_pp(e_exp, m) << "]\n";); - if (ctx.e_internalized(bv_sgn) && ctx.get_enode(bv_sgn)->get_num_th_vars() > 0) - bv_th->get_fixed_value(e_sgn, sgn_r); // OK to fail - if (ctx.e_internalized(bv_sig) && ctx.get_enode(bv_sig)->get_num_th_vars() > 0) - bv_th->get_fixed_value(e_sig, sig_r); // OK to fail - if (ctx.e_internalized(bv_exp) && ctx.get_enode(bv_exp)->get_num_th_vars() > 0) - bv_th->get_fixed_value(e_exp, exp_r); // OK to fail - - TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " " - << sig_r.to_string() << " " - << exp_r.to_string() << "]\n";); + if (!ctx.e_internalized(bv_sgn) || + ctx.get_enode(bv_sgn)->get_num_th_vars() == 0 || + !bv_th->get_fixed_value(e_sgn, sgn_r)) + sgn_r = rational(0); + if (!ctx.e_internalized(bv_sig) || + ctx.get_enode(bv_sig)->get_num_th_vars() == 0 || + !bv_th->get_fixed_value(e_sig, sig_r)) + sig_r = rational(0); + if (!ctx.e_internalized(bv_exp) || + ctx.get_enode(bv_exp)->get_num_th_vars() == 0 || + !bv_th->get_fixed_value(e_exp, exp_r)) + exp_r = bias; // un-bias exponent rational exp_unbiased_r; - exp_unbiased_r = exp_r - mpfm.m_powers2.m1(exp_sz - 1); + exp_unbiased_r = exp_r - bias; - mpz sig_z; mpf_exp_t exp_z; - mpq sig_q, exp_q; - mpz sig_num, exp_num; + TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " " + << sig_r.to_string() << " " + << exp_unbiased_r.to_string() << "(" << exp_r.to_string() << ")]\n"; ); + + scoped_mpz sig_z(mpzm); + mpf_exp_t exp_z; + scoped_mpq sig_q(mpqm), exp_q(mpqm); + scoped_mpz sig_num(mpzm), exp_num(mpzm); mpqm.set(sig_q, sig_r.to_mpq()); - mpzm.set(sig_num, sig_q.numerator()); + mpzm.set(sig_num, sig_q.get().numerator()); mpqm.set(exp_q, exp_unbiased_r.to_mpq()); - mpzm.set(exp_num, exp_q.numerator()); + mpzm.set(exp_num, exp_q.get().numerator()); mpzm.set(sig_z, sig_num); exp_z = mpzm.get_int64(exp_num); - mpf fp_val; - mpfm.set(fp_val, exp_sz, sig_sz + 1, !sgn_r.is_zero(), sig_z, exp_z); + scoped_mpf fp_val(mpfm); + mpfm.set(fp_val, ebits, sbits, !sgn_r.is_zero(), sig_z, exp_z); - app * fp_val_e; - fp_val_e = fu.mk_value(fp_val); - - TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;); - - mpfm.del(fp_val); - mpzm.del(sig_num); - mpzm.del(exp_num); - mpqm.del(sig_q); - mpqm.del(exp_q); - mpzm.del(sig_z); - - res = alloc(expr_wrapper_proc, fp_val_e); + TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mpfm.to_string(fp_val) << std::endl;); + res = alloc(expr_wrapper_proc, m_factory->mk_value(fp_val)); } else UNREACHABLE(); @@ -445,7 +471,7 @@ namespace smt { void theory_fpa::reset_eh() { pop_scope_eh(m_trail_stack.get_num_scopes()); - m_rw.reset(); + m_rw.reset(); m_trans_map.reset(); m_bool_var2atom.reset(); m_temporaries.reset(); @@ -453,6 +479,8 @@ namespace smt { theory::reset_eh(); } - void theory_fpa::init_model(model_generator & m) { + void theory_fpa::init_model(model_generator & m) { + m_factory = alloc(fpa_factory, get_manager(), get_family_id()); + m.register_factory(m_factory); } }; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 41374fd8f..7b29b82de 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -23,9 +23,38 @@ Revision History: #include"trail.h" #include"fpa2bv_converter.h" #include"fpa2bv_rewriter.h" +#include"value_factory.h" namespace smt { + class fpa_factory : public value_factory { + float_util m_util; + + virtual app * mk_value_core(mpf const & val, sort * s) { + SASSERT(m_util.get_ebits(s) == val.get_ebits()); + SASSERT(m_util.get_sbits(s) == val.get_sbits()); + return m_util.mk_value(val); + } + + public: + fpa_factory(ast_manager & m, family_id fid) : + value_factory(m, fid), + m_util(m) { + } + + virtual ~fpa_factory() {} + + virtual expr * get_some_value(sort * s) { NOT_IMPLEMENTED_YET(); } + virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { NOT_IMPLEMENTED_YET(); } + virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); } + virtual void register_value(expr * n) { /* Ignore */ } + + app * mk_value(mpf const & x) { + return m_util.mk_value(x); + } + }; + + class theory_fpa : public theory { class th_trail_stack : public trail_stack { public: @@ -60,6 +89,7 @@ namespace smt { bool_var2atom m_bool_var2atom; enode_vector m_temporaries; int_vector m_tvars; + fpa_factory * m_factory; virtual final_check_status final_check_eh() { return FC_DONE; } virtual bool internalize_atom(app * atom, bool gate_ctx); @@ -78,7 +108,6 @@ namespace smt { void assign_eh(bool_var v, bool is_true); virtual void relevant_eh(app * n); virtual void init_model(model_generator & m); - public: theory_fpa(ast_manager& m); virtual ~theory_fpa(); @@ -91,7 +120,8 @@ namespace smt { sig = to_app(e)->get_arg(1); exp = to_app(e)->get_arg(2); } - + + void add_extra_assertions(); void mk_bv_eq(expr * x, expr * y); };