From 5344d6f3c02f02aa980f916eb8ae09acba7ae81b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 15 Jan 2015 19:25:49 +0000 Subject: [PATCH] various bugfixes and extensions for FPA Signed-off-by: Christoph M. Wintersteiger --- src/ast/fpa/fpa2bv_converter.cpp | 237 ++++++------- src/ast/fpa/fpa2bv_converter.h | 16 +- src/ast/fpa/fpa2bv_rewriter.h | 10 +- src/ast/fpa_decl_plugin.cpp | 12 +- src/ast/fpa_decl_plugin.h | 7 +- src/ast/rewriter/fpa_rewriter.cpp | 10 +- src/smt/asserted_formulas.cpp | 4 +- src/smt/theory_fpa.cpp | 412 +++++++++++++--------- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- src/tactic/fpa/qffp_tactic.cpp | 27 +- 10 files changed, 396 insertions(+), 341 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f6ce259f2..4cdb64d8d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -44,8 +44,8 @@ fpa2bv_converter::~fpa2bv_converter() { } void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { - SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_TO_FP)); - SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP)); expr_ref sgn(m), s(m), e(m); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn); @@ -64,20 +64,20 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { } void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { - SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_TO_FP)); - SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_FP)); expr *t_sgn, *t_sig, *t_exp; expr *f_sgn, *f_sig, *f_exp; - split_triple(t, t_sgn, t_sig, t_exp); - split_triple(f, f_sgn, f_sig, f_exp); + split_fp(t, t_sgn, t_exp, t_sig); + split_fp(f, f_sgn, f_exp, f_sig); expr_ref sgn(m), s(m), e(m); m_simp.mk_ite(c, t_sgn, f_sgn, sgn); m_simp.mk_ite(c, t_sig, f_sig, s); m_simp.mk_ite(c, t_exp, f_exp, e); - mk_triple(sgn, s, e, result); + mk_fp(sgn, e, s, result); } void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -111,7 +111,7 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar mk_bias(e, biased_exp); - mk_triple(bv_sgn, bv_sig, biased_exp, result); + mk_fp(bv_sgn, biased_exp, bv_sig, result); TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is " << mk_ismt2_pp(result, m) << std::endl;); @@ -158,7 +158,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { SASSERT(m_bv_util.get_bv_size(e) == ebits); #endif - mk_triple(sgn, s, e, result); + mk_fp(sgn, e, s, result); m_const2bv.insert(f, result); m.inc_ref(f); @@ -177,7 +177,7 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) s = m.mk_var(base_inx + 1, m_bv_util.mk_sort(sbits-1)); e = m.mk_var(base_inx + 2, m_bv_util.mk_sort(ebits)); - mk_triple(sgn, s, e, result); + mk_fp(sgn, e, s, result); } void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) @@ -191,7 +191,7 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex if (is_float(args[i])) { expr * sgn, * sig, * exp; - split_triple(args[i], sgn, sig, exp); + split_fp(args[i], sgn, exp, sig); new_args.push_back(sgn); new_args.push_back(sig); new_args.push_back(exp); @@ -210,7 +210,7 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex a_sgn = m.mk_app(fd3.f_sgn, new_args.size(), new_args.c_ptr()); a_sig = m.mk_app(fd3.f_sig, new_args.size(), new_args.c_ptr()); a_exp = m.mk_app(fd3.f_exp, new_args.size(), new_args.c_ptr()); - mk_triple(a_sgn, a_sig, a_exp, result); + mk_fp(a_sgn, a_exp, a_sig, result); } else { sort_ref_buffer new_domain(m); @@ -256,7 +256,7 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex m.inc_ref(f_sgn); m.inc_ref(f_sig); m.inc_ref(f_exp); - mk_triple(a_sgn, a_sig, a_exp, result); + mk_fp(a_sgn, a_exp, a_sig, result); } } @@ -300,10 +300,10 @@ void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); expr_ref top_exp(m); mk_top_exp(ebits, top_exp); - mk_triple(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_numeral(0, sbits-1), - top_exp, - result); + mk_fp(m_bv_util.mk_numeral(0, 1), + top_exp, + m_bv_util.mk_numeral(0, sbits-1), + result); } void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) { @@ -313,10 +313,10 @@ void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); expr_ref top_exp(m); mk_top_exp(ebits, top_exp); - mk_triple(m_bv_util.mk_numeral(1, 1), - m_bv_util.mk_numeral(0, sbits-1), - top_exp, - result); + mk_fp(m_bv_util.mk_numeral(1, 1), + top_exp, + m_bv_util.mk_numeral(0, sbits-1), + result); } void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) { @@ -326,10 +326,10 @@ void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); expr_ref top_exp(m); mk_top_exp(ebits, top_exp); - mk_triple(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_numeral(1, sbits-1), - top_exp, - result); + mk_fp(m_bv_util.mk_numeral(0, 1), + top_exp, + m_bv_util.mk_numeral(1, sbits-1), + result); } void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) { @@ -339,10 +339,10 @@ void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); expr_ref bot_exp(m); mk_bot_exp(ebits, bot_exp); - mk_triple(m_bv_util.mk_numeral(1, 1), - m_bv_util.mk_numeral(0, sbits-1), - bot_exp, - result); + mk_fp(m_bv_util.mk_numeral(1, 1), + bot_exp, + m_bv_util.mk_numeral(0, sbits - 1), + result); } void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) { @@ -352,10 +352,10 @@ void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); expr_ref bot_exp(m); mk_bot_exp(ebits, bot_exp); - mk_triple(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_numeral(0, sbits-1), - bot_exp, - result); + mk_fp(m_bv_util.mk_numeral(0, 1), + bot_exp, + m_bv_util.mk_numeral(0, sbits-1), + result); } void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, @@ -607,13 +607,13 @@ void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; - split_triple(args[0], sgn, s, e); + split_fp(args[0], sgn, e, s); expr_ref c(m), nsgn(m); mk_is_nan(args[0], c); nsgn = m_bv_util.mk_bv_not(sgn); expr_ref r_sgn(m); m_simp.mk_ite(c, sgn, nsgn, r_sgn); - mk_triple(r_sgn, s, e, result); + mk_fp(r_sgn, e, s, result); } void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1027,8 +1027,8 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; - split_triple(args[0], sgn, s, e); - mk_triple(m_bv_util.mk_numeral(0, 1), s, e, result); + split_fp(args[0], sgn, e, s); + mk_fp(m_bv_util.mk_numeral(0, 1), e, s, result); } void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1038,8 +1038,8 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr * x_sgn, * x_sig, * x_exp; expr * y_sgn, * y_sig, * y_exp; - split_triple(x, x_sgn, x_sig, x_exp); - split_triple(y, y_sgn, y_sig, y_exp); + split_fp(x, x_sgn, x_exp, x_sig); + split_fp(y, y_sgn, y_exp, y_sig); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m); mk_is_zero(x, x_is_zero); @@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp); m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp); - mk_triple(r_sgn, r_sig, r_exp, result); + mk_fp(r_sgn, r_exp, r_sig, result); } void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1081,8 +1081,8 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr * x_sgn, * x_sig, * x_exp; expr * y_sgn, * y_sig, * y_exp; - split_triple(x, x_sgn, x_sig, x_exp); - split_triple(y, y_sgn, y_sig, y_exp); + split_fp(x, x_sgn, x_exp, x_sig); + split_fp(y, y_sgn, y_exp, y_sig); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m); mk_is_zero(y, y_is_zero); @@ -1114,7 +1114,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp); m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp); - mk_triple(r_sgn, r_sig, r_exp, result); + mk_fp(r_sgn, r_exp, r_sig, result); } void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1689,8 +1689,8 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a expr * x_sgn, * x_sig, * x_exp; expr * y_sgn, * y_sig, * y_exp; - split_triple(x, x_sgn, x_sig, x_exp); - split_triple(y, y_sgn, y_sig, y_exp); + split_fp(x, x_sgn, x_exp, x_sig); + split_fp(y, y_sgn, y_exp, y_sig); expr_ref x_eq_y_sgn(m), x_eq_y_exp(m), x_eq_y_sig(m); m_simp.mk_eq(x_sgn, y_sgn, x_eq_y_sgn); @@ -1725,8 +1725,8 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a expr * x_sgn, * x_sig, * x_exp; expr * y_sgn, * y_sig, * y_exp; - split_triple(x, x_sgn, x_sig, x_exp); - split_triple(y, y_sgn, y_sig, y_exp); + split_fp(x, x_sgn, x_exp, x_sig); + split_fp(y, y_sgn, y_exp, y_sig); expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m); one_1 = m_bv_util.mk_numeral(1, 1); @@ -1863,10 +1863,10 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args int sz = m_bv_util.get_bv_size(bv); SASSERT((unsigned)sz == to_sbits + to_ebits); - mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), - m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), - m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), - result); + mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv), + m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), + m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), + result); } else if (num == 2 && m_bv_util.is_bv(args[0]) && @@ -1895,7 +1895,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args SASSERT(m_bv_util.get_bv_size(args[0]) == 1); SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); - mk_triple(args[0], args[2], args[1], result); + mk_fp(args[0], args[1], args[2], result); } else if (num == 3 && m_bv_util.is_bv(args[0]) && @@ -2061,6 +2061,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << "x: " << mk_ismt2_pp(x, m) << std::endl;); SASSERT(m_util.is_float(s)); + SASSERT(au().is_real(x)); + unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); @@ -2093,11 +2095,9 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); mk_bias(unbiased_exp, e); - mk_triple(sgn, s, e, result); + mk_fp(sgn, e, s, result); } - else { - NOT_IMPLEMENTED_YET(); - + else { mpf_manager & fm = fu().fm(); bv_util & bu = m_bv_util; arith_util & au = m_arith_util; @@ -2109,44 +2109,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * two = au.mk_numeral(rational(2), false); expr_ref sgn(m), sig(m), exp(m); - sgn = m.mk_ite(au.mk_lt(x, zero), bv1, bv0); - sig = bu.mk_numeral(0, sbits + 4); - mpz const & max_normal_exponent = fm.m_powers2.m1(ebits-1); - exp = bu.mk_numeral(max_normal_exponent, ebits); - - //expr_ref cur_s(m), cur_d(m), cur_r(m), cur_s2(m), bv1_s4(m); - //bv1_s4 = bu.mk_numeral(1, sbits + 4); - //cur_s = x; - //std::string trace_name; - //for (unsigned i = 0; i < sbits + 3; i++) { - // std::stringstream dbg_name; - // dbg_name << "fpa2bv_to_float_real_sig_" << i; - // dbg_decouple(dbg_name.str().c_str(), sig); + sgn = mk_fresh_const("fpa2bv_to_fp_real_sgn", 1); + sig = mk_fresh_const("fpa2bv_to_fp_real_sig", sbits + 4); + exp = mk_fresh_const("fpa2bv_to_fp_real_exp", ebits + 2); - // cur_s = au.mk_div(cur_s, two); - // // cur_r = au.mk_rem(cur_s, two); - // cur_r = au.mk_mod(cur_s, two); - // cur_s2 = bu.mk_bv_shl(sig, bv1_s4); - // sig = m.mk_ite(au.mk_eq(cur_r, zero), - // cur_s2, - // bu.mk_bv_add(cur_s2, bv1_s4)); - //} - //dbg_decouple("fpa2bv_to_float_real_last_cur_s", cur_s); - //expr_ref inc(m); - //inc = m.mk_not(m.mk_eq(cur_s, zero)); - //dbg_decouple("fpa2bv_to_float_real_inc", inc); - //sig = m.mk_ite(inc, bu.mk_bv_add(sig, bv1_s4), sig); - - //SASSERT(bu.get_bv_size(sgn) == 1); - //SASSERT(bu.get_bv_size(sig) == sbits + 4); - //SASSERT(bu.get_bv_size(exp) == ebits + 2); + expr_ref rme(rm, m); + round(s, rme, sgn, sig, exp, result); - //dbg_decouple("fpa2bv_to_float_real_sgn", sgn); - //dbg_decouple("fpa2bv_to_float_real_sig", sig); - //dbg_decouple("fpa2bv_to_float_real_exp", exp); - - //expr_ref rmr(rm, m); - //round(s, rmr, sgn, sig, exp, result); + expr * e = m.mk_eq(m_util.mk_to_real(result), x); + m_extra_assertions.push_back(e); } SASSERT(is_well_sorted(m, result)); @@ -2208,7 +2179,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); SASSERT(num == 1); SASSERT(f->get_num_parameters() == 0); - SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FPA_FP)); expr * x = args[0]; sort * s = m.get_sort(x); @@ -2565,19 +2536,10 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; - split_triple(args[0], sgn, s, e); + split_fp(args[0], sgn, e, s); result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } -void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 3); - SASSERT(m_bv_util.get_bv_size(args[0]) == 1); - SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1); - SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); - mk_triple(args[0], args[2], args[1], result); - TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;); -} - void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); @@ -2753,6 +2715,10 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); + dbg_decouple("fpa2bv_to_sbv_sgn", sgn); + dbg_decouple("fpa2bv_to_sbv_sig", sig); + dbg_decouple("fpa2bv_to_sbv_exp", exp); + // x is of the form +- [1].[sig] * 2^(exp-lz) SASSERT(m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.get_bv_size(sig) == sbits); @@ -2777,8 +2743,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2); SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2); SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); - dbg_decouple("fpa2bv_to_ubv_shift", shift); - dbg_decouple("fpa2bv_to_ubv_shift_abs", shift_abs); + dbg_decouple("fpa2bv_to_sbv_shift", shift); + dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // [1][ ... sig ... ][r][g][ ... s ...] @@ -2861,28 +2827,43 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified() { return expr_ref(m_util.mk_internal_to_real_unspecified(), m); } -void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); - SASSERT(to_app(e)->get_num_args() == 3); - +void fpa2bv_converter::mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result) { + SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); + SASSERT(m_bv_util.is_bv(significand)); + SASSERT(m_bv_util.is_bv(exponent)); + result = m.mk_app(m_util.get_family_id(), OP_FPA_FP, sign, exponent, significand); +} + +void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 3); + SASSERT(m_bv_util.get_bv_size(args[0]) == 1); + SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2]) + 1); + SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1])); + mk_fp(args[0], args[1], args[2], result); + TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;); +} + +void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const { + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); + SASSERT(to_app(e)->get_num_args() == 3); sgn = to_app(e)->get_arg(0); exp = to_app(e)->get_arg(1); sig = to_app(e)->get_arg(2); } -void fpa2bv_converter::split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); +void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const { + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr *e_sgn, *e_sig, *e_exp; - split_triple(e, e_sgn, e_sig, e_exp); + split_fp(e, e_sgn, e_exp, e_sig); sgn = e_sgn; - sig = e_sig; exp = e_exp; + sig = e_sig; } void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); // exp == 1^n , sig != 0 expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m); @@ -2897,7 +2878,7 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref eq1(m), eq2(m), top_exp(m), zero(m); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); @@ -2921,7 +2902,7 @@ void fpa2bv_converter::mk_is_ninf(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref zero(m); @@ -2930,7 +2911,7 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); expr_ref one(m); @@ -2940,7 +2921,7 @@ void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref eq1(m), eq2(m), bot_exp(m), zero(m); mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); @@ -2951,7 +2932,7 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref e_is_zero(m), eq(m), one_1(m); mk_is_zero(e, e_is_zero); one_1 = m_bv_util.mk_numeral(1, 1); @@ -2961,7 +2942,7 @@ void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref e_is_zero(m), eq(m), nil_1(m); mk_is_zero(e, e_is_zero); nil_1 = m_bv_util.mk_numeral(0, 1); @@ -2971,7 +2952,7 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref zero(m); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)); m_simp.mk_eq(exp, zero, result); @@ -2979,7 +2960,7 @@ void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); expr_ref is_special(m), is_denormal(m), p(m); mk_is_denormal(e, is_denormal); @@ -3093,7 +3074,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { } void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) { - SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_TO_FP)); + SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)); SASSERT(to_app(e)->get_num_args() == 3); sort * srt = to_app(e)->get_decl()->get_range(); @@ -3101,7 +3082,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref unsigned sbits = m_util.get_sbits(srt); unsigned ebits = m_util.get_ebits(srt); - split_triple(e, sgn, sig, exp); + split_fp(e, sgn, exp, sig); + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(exp) == ebits); + SASSERT(m_bv_util.get_bv_size(sig) == sbits-1); expr_ref is_normal(m); mk_is_normal(e, is_normal); @@ -3134,7 +3119,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref expr_ref shift(m); m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); dbg_decouple("fpa2bv_unpack_shift", shift); - SASSERT(is_well_sorted(m, is_sig_zero)); + SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, shift)); SASSERT(m_bv_util.get_bv_size(shift) == ebits); if (ebits <= sbits) { @@ -3545,7 +3530,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & SASSERT(m_bv_util.get_bv_size(res_exp) == ebits); SASSERT(is_well_sorted(m, res_exp)); - mk_triple(res_sgn, res_sig, res_exp, result); + mk_fp(res_sgn, res_exp, res_sig, result); TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 062c56ef2..82fad6ff9 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -72,15 +72,11 @@ public: bool is_rm(sort * s) { return m_util.is_rm(s); } bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); } - void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) { - SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); - SASSERT(m_bv_util.is_bv(significand)); - SASSERT(m_bv_util.is_bv(exponent)); - result = m.mk_app(m_util.get_family_id(), OP_FPA_TO_FP, sign, exponent, significand); - } + void mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result); + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const; - void split_triple(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp) const; + void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; + void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); @@ -125,9 +121,7 @@ public: void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - - void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 75176c9c4..ed885a4cc 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -259,13 +259,13 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { unsigned ebits = m_conv.fu().get_ebits(s); unsigned sbits = m_conv.fu().get_sbits(s); new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); - m_conv.mk_triple(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), - m_conv.bu().mk_extract(ebits-1, 0, new_var), - new_exp); + m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), + m_conv.bu().mk_extract(ebits - 1, 0, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + new_exp); } else - new_exp = m().mk_var(t->get_idx(), s); + new_exp = m().mk_var(t->get_idx(), s); result = new_exp; result_pr = 0; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 9900812dd..8cf158604 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -72,7 +72,7 @@ func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) { parameter p(mk_id(v), true); SASSERT(p.is_external()); sort * s = mk_float_sort(v.get_ebits(), v.get_sbits()); - return m_manager->mk_const_decl(symbol("fpa"), s, func_decl_info(m_family_id, OP_FPA_NUM, 1, &p)); + return m_manager->mk_const_decl(symbol("fp.numeral"), s, func_decl_info(m_family_id, OP_FPA_NUM, 1, &p)); } app * fpa_decl_plugin::mk_numeral(mpf const & v) { @@ -131,6 +131,11 @@ bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) { return false; } +bool fpa_decl_plugin::is_numeral(expr * n) { + scoped_mpf v(m_fm); + return is_numeral(n, v); +} + bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) { if (is_app_of(n, m_family_id, OP_FPA_RM_NEAREST_TIES_TO_AWAY)) { val = MPF_ROUND_NEAREST_TAWAY; @@ -156,6 +161,11 @@ bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) { return 0; } +bool fpa_decl_plugin::is_rm_numeral(expr * n) { + mpf_rounding_mode t; + return is_rm_numeral(n, t); +} + void fpa_decl_plugin::del(parameter const & p) { SASSERT(p.is_external()); recycled_id(p.get_ext_id()); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 24481d348..fc1521456 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -191,10 +191,10 @@ public: mpf_manager & fm() { return m_fm; } func_decl * mk_numeral_decl(mpf const & v); app * mk_numeral(mpf const & v); - bool is_numeral(expr * n) { return is_app_of(n, m_family_id, OP_FPA_NUM); } + bool is_numeral(expr * n); bool is_numeral(expr * n, mpf & val); bool is_rm_numeral(expr * n, mpf_rounding_mode & val); - bool is_rm_numeral(expr * n) { mpf_rounding_mode t; return is_rm_numeral(n, t); } + bool is_rm_numeral(expr * n); mpf const & get_value(unsigned id) const { SASSERT(m_value_table.contains(id)); @@ -322,8 +322,7 @@ public: app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_INF, arg1); } app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); } app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); } - app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); } - app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); } + app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); } app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); } app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 915d25e50..ce7fe5ed6 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -131,7 +131,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const scoped_mpf v(m_util.fm()); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); return BR_DONE; } else if (bu.is_numeral(args[0], r1, bvs1) && @@ -268,10 +268,8 @@ br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) { result = arg1; return BR_DONE; } - result = m().mk_ite(m_util.mk_is_sign_minus(arg1), - m_util.mk_neg(arg1), - arg1); - return BR_REWRITE2; + + return BR_FAILED; } br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { @@ -565,7 +563,7 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & r1.is_one(), r3.to_mpq().numerator(), m_util.fm().unbias_exp(bvs2, biased_exp)); - TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;); + TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_util.fm().to_string(v) << std::endl;); result = m_util.mk_value(v); return BR_DONE; } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 4775e44a4..1acfcdf57 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -22,6 +22,7 @@ Revision History: #include"arith_simplifier_plugin.h" #include"array_simplifier_plugin.h" #include"datatype_simplifier_plugin.h" +#include"fpa_simplifier_plugin.h" #include"bv_simplifier_plugin.h" #include"for_each_expr.h" #include"well_sorted.h" @@ -96,7 +97,8 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params)); bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params); s.register_plugin(bvsimp); - s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp)); } void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) { diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 158622428..ac9bd5141 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -54,11 +54,11 @@ namespace smt { unsigned ebits = m_th.m_fpa_util.get_ebits(s); unsigned sbits = m_th.m_fpa_util.get_sbits(s); SASSERT(bv_sz == ebits + sbits); - m_th.m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), - m_bv_util.mk_extract(sbits - 2, 0, bv), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), - result); - + m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), + m_bv_util.mk_extract(sbits - 2, 0, bv), + result); + SASSERT(m_th.m_fpa_util.is_float(result)); m_const2bv.insert(f, result); m.inc_ref(f); m.inc_ref(result); @@ -97,62 +97,86 @@ namespace smt { } theory_fpa::~theory_fpa() - { + { ast_manager & m = get_manager(); dec_ref_map_values(m, m_conversions); dec_ref_map_values(m, m_wraps); - dec_ref_map_values(m, m_unwraps); + dec_ref_map_values(m, m_unwraps); } app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { - SASSERT(values.size() == 1); ast_manager & m = m_th.get_manager(); + TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) + tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); + mpf_manager & mpfm = m_fu.fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); - unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); - - SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits)); - + unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); app * result; - + scoped_mpz bias(mpzm); mpzm.power(mpz(2), m_ebits - 1, bias); mpzm.dec(bias); - rational all_rat(0); - scoped_mpz all_bits(mpzm); + scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm); unsigned bv_sz; - bool r = m_bu.is_numeral(values[0], all_rat, bv_sz); - SASSERT(r); - SASSERT(bv_sz == (m_ebits+m_sbits)); - SASSERT(all_rat.is_int()); - mpzm.set(all_bits, all_rat.to_mpq().numerator()); - - scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm); - mpzm.machine_div2k(all_bits, m_ebits + m_sbits - 1, sgn_z); - mpzm.mod(all_bits, mpfm.m_powers2(m_ebits + m_sbits - 1), all_bits); + if (values.size() == 1) { + SASSERT(m_bu.is_bv(values[0])); + SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits)); - mpzm.machine_div2k(all_bits, m_sbits - 1, exp_z); - mpzm.mod(all_bits, mpfm.m_powers2(m_sbits - 1), all_bits); - - mpzm.set(sig_z, all_bits); + rational all_r(0); + scoped_mpz all_z(mpzm); - TRACE("t_fpa_detail", tout << "sgn=" << mpzm.to_string(sgn_z) << " ; " << - "sig=" << mpzm.to_string(sig_z) << " ; " << - "exp=" << mpzm.to_string(exp_z) << std::endl;); + bool r = m_bu.is_numeral(values[0], all_r, bv_sz); + SASSERT(r); + SASSERT(bv_sz == (m_ebits + m_sbits)); + SASSERT(all_r.is_int()); + mpzm.set(all_z, all_r.to_mpq().numerator()); + + mpzm.machine_div2k(all_z, m_ebits + m_sbits - 1, sgn_z); + mpzm.mod(all_z, mpfm.m_powers2(m_ebits + m_sbits - 1), all_z); + + mpzm.machine_div2k(all_z, m_sbits - 1, exp_z); + mpzm.mod(all_z, mpfm.m_powers2(m_sbits - 1), all_z); + + mpzm.set(sig_z, all_z); + } + else if (values.size() == 3) { + rational sgn_r(0), exp_r(0), sig_r(0); + + bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz); + SASSERT(r && bv_sz == 1); + r = m_bu.is_numeral(values[1], exp_r, bv_sz); + SASSERT(r && bv_sz == m_ebits); + r = m_bu.is_numeral(values[2], sig_r, bv_sz); + SASSERT(r && bv_sz == m_sbits - 1); + + SASSERT(sgn_r.to_mpq().denominator() == mpz(1)); + SASSERT(exp_r.to_mpq().denominator() == mpz(1)); + SASSERT(sig_r.to_mpq().denominator() == mpz(1)); + + mpzm.set(sgn_z, sgn_r.to_mpq().numerator()); + mpzm.set(exp_z, exp_r.to_mpq().numerator()); + mpzm.set(sig_z, sig_r.to_mpq().numerator()); + } + else + UNREACHABLE(); scoped_mpz exp_u = exp_z - bias; SASSERT(mpzm.is_int64(exp_u)); - scoped_mpf f(mpfm); + scoped_mpf f(mpfm); mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), sig_z, mpzm.get_int64(exp_u)); result = m_fu.mk_value(f); TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" << - mk_ismt2_pp(values[0], m) << "] --> " << - mk_ismt2_pp(result, m_th.get_manager()) << "\n";); + mpzm.to_string(sgn_z) << "," << + mpzm.to_string(exp_z) << "," << + mpzm.to_string(sig_z) << "] --> " << + mk_ismt2_pp(result, m_th.get_manager()) << "\n";); + return result; } @@ -160,8 +184,8 @@ namespace smt { SASSERT(values.size() == 1); ast_manager & m = m_th.get_manager(); - TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: [" << - mk_ismt2_pp(values[0], m) << "]" << std::endl;); + TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) + tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); app * result = 0; sort * s = m.get_sort(values[0]); @@ -199,42 +223,44 @@ namespace smt { if (!m_wraps.find(e_srt, w)) { SASSERT(!m_wraps.contains(e_srt)); - sort * bv_srt = 0; - + sort * bv_srt; if (m_converter.is_rm(e_srt)) bv_srt = m_bv_util.mk_sort(3); else { SASSERT(m_converter.is_float(e_srt)); unsigned ebits = m_fpa_util.get_ebits(e_srt); unsigned sbits = m_fpa_util.get_sbits(e_srt); - bv_srt = m_bv_util.mk_sort(ebits + sbits); + bv_srt = m_bv_util.mk_sort(ebits + sbits); } - w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); + w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); m_wraps.insert(e_srt, w); - m.inc_ref(w); + m.inc_ref(w); } - return app_ref(m.mk_app(w, e), m); + app_ref res(m); + res = m.mk_app(w, e); + return res; } app_ref theory_fpa::unwrap(expr * e, sort * s) { SASSERT(!m_fpa_util.is_unwrap(e)); ast_manager & m = get_manager(); context & ctx = get_context(); - sort * e_srt = m.get_sort(e); + sort * bv_srt = m.get_sort(e); func_decl *u; - if (!m_unwraps.find(e_srt, u)) { - SASSERT(!m_unwraps.contains(e_srt)); - sort * bv_srt = m.get_sort(e); + if (!m_unwraps.find(bv_srt, u)) { + SASSERT(!m_unwraps.contains(bv_srt)); u = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s); - m_unwraps.insert(s, u); + m_unwraps.insert(bv_srt, u); m.inc_ref(u); } - return app_ref(m.mk_app(u, e), m); + app_ref res(m); + res = m.mk_app(u, e); + return res; } expr_ref theory_fpa::convert_atom(expr * e) { @@ -244,55 +270,30 @@ namespace smt { m_rw(e, res); m_th_rw(res, res); SASSERT(is_app(res)); - SASSERT(m.is_bool(res)); + SASSERT(m.is_bool(res)); return res; } expr_ref theory_fpa::convert_term(expr * e) { - ast_manager & m = get_manager(); - TRACE("t_fpa_detail", tout << "converting: " << mk_ismt2_pp(e, m) << " sort is: " << mk_ismt2_pp(m.get_sort(e), m) << std::endl;); + ast_manager & m = get_manager(); context & ctx = get_context(); - expr_ref ec(m), res(m); + expr_ref e_conv(m), res(m); proof_ref pr(m); - m_rw(e, ec); + m_rw(e, e_conv); - SASSERT(is_app(ec)); - app_ref eca(to_app(ec), m); - TRACE("t_fpa_detail", tout << "eca = " << mk_ismt2_pp(eca, m) << " sort is: " << mk_ismt2_pp(m.get_sort(eca), m) << std::endl;); - - if (m_fpa_util.is_rm(e)) { - expr_ref bv_rm(m); - bv_rm = eca; - TRACE("t_fpa_detail", tout << "bvrm = " << mk_ismt2_pp(bv_rm, m) << " sort is: " << mk_ismt2_pp(m.get_sort(bv_rm), m) << std::endl;); - SASSERT(is_sort_of(m.get_sort(bv_rm), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(m_bv_util.get_bv_size(bv_rm) == 3); - m_th_rw(bv_rm, res); + if (m_fpa_util.is_rm(e)) { + SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT)); + SASSERT(m_bv_util.get_bv_size(e_conv) == 3); + m_th_rw(e_conv, res); } else if (m_fpa_util.is_float(e)) { - SASSERT(eca->get_family_id() == get_family_id()); - fpa_op_kind k = (fpa_op_kind)(eca->get_decl_kind()); - SASSERT(k == OP_FPA_TO_FP || k == OP_FPA_INTERNAL_BVUNWRAP); - switch (k) { - case OP_FPA_TO_FP: { - SASSERT(eca->get_num_args() == 3); - SASSERT(is_sort_of(m.get_sort(eca->get_arg(0)), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(is_sort_of(m.get_sort(eca->get_arg(1)), m_bv_util.get_family_id(), BV_SORT)); - SASSERT(is_sort_of(m.get_sort(eca->get_arg(2)), m_bv_util.get_family_id(), BV_SORT)); - - expr *sgn, *sig, *exp; - expr_ref s_sgn(m), s_sig(m), s_exp(m); - m_converter.split_triple(eca, sgn, sig, exp); - m_th_rw(sgn, s_sgn); - m_th_rw(sig, s_sig); - m_th_rw(exp, s_exp); - - m_converter.mk_triple(s_sgn, s_sig, s_exp, res); - break; - } - default: - res = eca; - } + expr_ref sgn(m), sig(m), exp(m); + m_converter.split_fp(e_conv, sgn, exp, sig); + m_th_rw(sgn); + m_th_rw(exp); + m_th_rw(sig); + m_converter.mk_fp(sgn, exp, sig, res); } else UNREACHABLE(); @@ -310,7 +311,7 @@ namespace smt { SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e)); - m_rw(e, res); + m_rw(e, res); m_th_rw(res, res); return res; } @@ -327,12 +328,13 @@ namespace smt { SASSERT(m_fpa_util.is_float(srt)); unsigned ebits = m_fpa_util.get_ebits(srt); unsigned sbits = m_fpa_util.get_sbits(srt); - expr * bv = to_app(e)->get_arg(0); - unsigned bv_sz = m_bv_util.get_bv_size(bv); - m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), - m_bv_util.mk_extract(sbits - 2, 0, bv), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), - res); + expr_ref bv(m); + bv = to_app(e)->get_arg(0); + unsigned bv_sz = m_bv_util.get_bv_size(bv); + m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), + m_bv_util.mk_extract(sbits - 2, 0, bv), + res); } return res; } @@ -342,7 +344,7 @@ namespace smt { ast_manager & m = get_manager(); context & ctx = get_context(); expr_ref res(m); - + if (m_conversions.contains(e)) { res = m_conversions.find(e); TRACE("t_fpa_detail", tout << "cached:" << std::endl; @@ -401,11 +403,12 @@ namespace smt { void theory_fpa::assert_cnstr(expr * e) { if (get_manager().is_true(e)) return; TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); - context& ctx = get_context(); + context & ctx = get_context(); ctx.internalize(e, false); literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); - ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.mk_th_axiom(get_id(), 1, &lit); + TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); } void theory_fpa::attach_new_th_var(enode * n) { @@ -433,11 +436,10 @@ namespace smt { ctx.set_var_theory(l.var(), get_id()); expr_ref bv_atom(m); - bv_atom = convert(atom); + bv_atom = convert_atom(atom); SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - expr_ref atom_iff(m); assert_cnstr(m.mk_iff(atom, bv_atom)); return true; } @@ -447,7 +449,7 @@ namespace smt { context & ctx = get_context(); TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); SASSERT(term->get_family_id() == get_family_id()); - SASSERT(!ctx.e_internalized(term)); + SASSERT(!ctx.e_internalized(term)); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) @@ -455,7 +457,7 @@ namespace smt { enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true); - + if (is_attached_to_var(e)) return false; @@ -476,9 +478,9 @@ namespace smt { assert_cnstr(mk_side_conditions()); break; } - default: /* ignore */; + default: /* ignore */; } - + return true; } @@ -486,33 +488,33 @@ namespace smt { TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";); SASSERT(n->get_owner()->get_family_id() == get_family_id() || n->get_owner()->get_family_id() == null_theory_id); - SASSERT(s->get_family_id() == get_family_id()); + SASSERT(s->get_family_id() == get_family_id()); - if (!is_attached_to_var(n)) + if (!is_attached_to_var(n)) { attach_new_th_var(n); - ast_manager & m = get_manager(); - context & ctx = get_context(); + ast_manager & m = get_manager(); + context & ctx = get_context(); - app_ref owner(m); - sort_ref owner_sort(m); - owner = n->get_owner(); - owner_sort = m.get_sort(owner); + app_ref owner(m); + sort_ref owner_sort(m); + owner = n->get_owner(); + owner_sort = m.get_sort(owner); - if (m_fpa_util.is_rm(owner_sort)) { - // For every RM term, we need to make sure that it's - // associated bit-vector is within the valid range. - if (!m_fpa_util.is_unwrap(owner)) - { - expr_ref valid(m), limit(m); - limit = m_bv_util.mk_numeral(4, 3); - valid = m_bv_util.mk_ule(wrap(owner), limit); - assert_cnstr(valid); + if (m_fpa_util.is_rm(owner_sort)) { + // For every RM term, we need to make sure that it's + // associated bit-vector is within the valid range. + if (!m_fpa_util.is_unwrap(owner)) { + expr_ref valid(m), limit(m); + limit = m_bv_util.mk_numeral(4, 3); + valid = m_bv_util.mk_ule(wrap(owner), limit); + assert_cnstr(valid); + } } + + if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner)) + assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner)); } - - if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner)) - assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner)); } void theory_fpa::new_eq_eh(theory_var x, theory_var y) { @@ -527,36 +529,40 @@ namespace smt { bv_util & bu = m_bv_util; mpf_manager & mpfm = fu.fm(); - app * xe = get_enode(x)->get_owner(); - app * ye = get_enode(y)->get_owner(); + expr_ref xe(m), ye(m); + xe = get_enode(x)->get_owner(); + ye = get_enode(y)->get_owner(); if ((m.is_bool(xe) && m.is_bool(ye)) || (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) { - SASSERT(xe->get_decl()->get_family_id() == get_family_id()); + SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id()); return; } - + expr_ref xc(m), yc(m); xc = convert(xe); yc = convert(ye); - + + TRACE("t_fpa_detail", tout << "xc=" << mk_ismt2_pp(xc, m) << std::endl; + tout << "yc=" << mk_ismt2_pp(yc, m) << std::endl;); + expr_ref c(m); - + if (fu.is_float(xe) && fu.is_float(ye)) { expr *x_sgn, *x_sig, *x_exp; - m_converter.split_triple(xc, x_sgn, x_sig, x_exp); + m_converter.split_fp(xc, x_sgn, x_exp, x_sig); expr *y_sgn, *y_sig, *y_exp; - m_converter.split_triple(yc, y_sgn, y_sig, y_exp); + m_converter.split_fp(yc, y_sgn, y_exp, y_sig); - c = m.mk_and(m.mk_eq(x_sgn, y_sgn), - m.mk_eq(x_sig, y_sig), - m.mk_eq(x_exp, y_exp)); + c = m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig), + m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig)); } else c = m.mk_eq(xc, yc); - - assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); + + m_th_rw(c); + assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); assert_cnstr(mk_side_conditions()); return; @@ -572,12 +578,13 @@ namespace smt { context & ctx = get_context(); mpf_manager & mpfm = m_fpa_util.fm(); - app * xe = get_enode(x)->get_owner(); - app * ye = get_enode(y)->get_owner(); + expr_ref xe(m), ye(m); + xe = get_enode(x)->get_owner(); + ye = get_enode(y)->get_owner(); if ((m.is_bool(xe) && m.is_bool(ye)) || (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) { - SASSERT(xe->get_decl()->get_family_id() == get_family_id()); + SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id()); return; } @@ -590,18 +597,18 @@ namespace smt { if (m_fpa_util.is_float(xe) && m_fpa_util.is_float(ye)) { expr *x_sgn, *x_sig, *x_exp; - m_converter.split_triple(xc, x_sgn, x_sig, x_exp); + m_converter.split_fp(xc, x_sgn, x_exp, x_sig); expr *y_sgn, *y_sig, *y_exp; - m_converter.split_triple(yc, y_sgn, y_sig, y_exp); - - c = m.mk_or(m.mk_not(m.mk_eq(x_sgn, y_sgn)), - m.mk_not(m.mk_eq(x_sig, y_sig)), - m.mk_not(m.mk_eq(x_exp, y_exp))); + m_converter.split_fp(yc, y_sgn, y_exp, y_sig); + + c = m.mk_not(m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig), + m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig))); } else c = m.mk_not(m.mk_eq(xc, yc)); - assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c)); + m_th_rw(c); + assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c)); assert_cnstr(mk_side_conditions()); return; @@ -609,7 +616,7 @@ namespace smt { void theory_fpa::push_scope_eh() { theory::push_scope_eh(); - m_trail_stack.push_scope(); + m_trail_stack.push_scope(); } void theory_fpa::pop_scope_eh(unsigned num_scopes) { @@ -628,8 +635,10 @@ namespace smt { expr_ref converted(m); converted = m.mk_and(convert(e), mk_side_conditions()); - if (!is_true) converted = m.mk_not(converted); - assert_cnstr(converted); + if (is_true) + assert_cnstr(m.mk_implies(e, converted)); + else + assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted))); } void theory_fpa::relevant_eh(app * n) { @@ -664,18 +673,17 @@ namespace smt { assert_cnstr(c); } else { - c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); + c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); assert_cnstr(c); } } } else if (n->get_family_id() == get_family_id()) { - SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); // These are the conversion functions fp.to_* */ + SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); } else UNREACHABLE(); - } void theory_fpa::reset_eh() { @@ -695,6 +703,7 @@ namespace smt { final_check_status theory_fpa::final_check_eh() { TRACE("t_fpa", tout << "final_check_eh\n";); + SASSERT(m_converter.m_extra_assertions.empty()); return FC_DONE; } @@ -705,45 +714,75 @@ namespace smt { } model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { - TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";); + TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << + " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";); ast_manager & m = get_manager(); context & ctx = get_context(); - app * owner = n->get_owner(); + app_ref owner(m); + owner = n->get_owner(); // If the owner is not internalized, it doesn't have an enode associated. SASSERT(ctx.e_internalized(owner)); if (m_fpa_util.is_rm_numeral(owner) || - m_fpa_util.is_numeral(owner)) + m_fpa_util.is_numeral(owner)) { return alloc(expr_wrapper_proc, owner); + } model_value_proc * res = 0; app_ref wrapped(m); wrapped = wrap(owner); - - CTRACE("t_fpa", !ctx.e_internalized(wrapped), - tout << "Model dependency not internalized: " << - mk_ismt2_pp(wrapped, m) << - " (owner " << (!ctx.e_internalized(owner) ? "not" : "is") << - " internalized)" << std::endl;); - - if (m_fpa_util.is_rm(owner)) { - fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this); - vp->add_dependency(ctx.get_enode(wrapped)); - res = vp; - } - else if (m_fpa_util.is_float(owner)) { + SASSERT(m_bv_util.is_bv(wrapped)); + + CTRACE("t_fpa_detail", !ctx.e_internalized(wrapped), + tout << "Model dependency not internalized: " << + mk_ismt2_pp(wrapped, m) << + " (owner " << (!ctx.e_internalized(owner) ? "not" : "is") << + " internalized)" << std::endl;); + + if (is_app_of(owner, get_family_id(), OP_FPA_FP)) { + SASSERT(to_app(owner)->get_num_args() == 3); + app_ref a0(m), a1(m), a2(m); + a0 = to_app(owner->get_arg(0)); + a1 = to_app(owner->get_arg(1)); + a2 = to_app(owner->get_arg(2)); unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); - fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); - vp->add_dependency(ctx.get_enode(wrapped)); + fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); + vp->add_dependency(ctx.get_enode(a0)); + vp->add_dependency(ctx.get_enode(a1)); + vp->add_dependency(ctx.get_enode(a2)); + TRACE("t_fpa_detail", tout << "Depends on: " << + mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl << + mk_ismt2_pp(a1, m) << " eq. cls. #" << get_enode(a1)->get_root()->get_owner()->get_id() << std::endl << + mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;); res = vp; } - else - UNREACHABLE(); + else if (ctx.e_internalized(wrapped)) { + if (m_fpa_util.is_rm(owner)) { + fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this); + vp->add_dependency(ctx.get_enode(wrapped)); + res = vp; + } + else if (m_fpa_util.is_float(owner)) { + unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); + unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); + fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); + enode * en = ctx.get_enode(wrapped); + vp->add_dependency(en); + TRACE("t_fpa_detail", tout << "Depends on: " << mk_ismt2_pp(wrapped, m) << " eq. cls. #" << en->get_root()->get_owner()->get_id() << std::endl;); + res = vp; + } + } + else { + unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); + unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); + return alloc(expr_wrapper_proc, m_fpa_util.mk_pzero(ebits, sbits)); + } + SASSERT(res != 0); return res; } @@ -754,7 +793,7 @@ namespace smt { ast_manager & m = get_manager(); context & ctx = get_context(); - out << "theory variables:" << std::endl; + out << "fpa theory variables:" << std::endl; ptr_vector::const_iterator it = ctx.begin_enodes(); ptr_vector::const_iterator end = ctx.end_enodes(); for (; it != end; it++) { @@ -762,5 +801,32 @@ namespace smt { if (v != -1) out << v << " -> " << mk_ismt2_pp((*it)->get_owner(), m) << std::endl; } + + out << "bv theory variables:" << std::endl; + it = ctx.begin_enodes(); + end = ctx.end_enodes(); + for (; it != end; it++) { + theory_var v = (*it)->get_th_var(m_bv_util.get_family_id()); + if (v != -1) out << v << " -> " << + mk_ismt2_pp((*it)->get_owner(), m) << std::endl; + } + + out << "arith theory variables:" << std::endl; + it = ctx.begin_enodes(); + end = ctx.end_enodes(); + for (; it != end; it++) { + theory_var v = (*it)->get_th_var(m_arith_util.get_family_id()); + if (v != -1) out << v << " -> " << + mk_ismt2_pp((*it)->get_owner(), m) << std::endl; + } + + out << "equivalence classes:\n"; + it = ctx.begin_enodes(); + end = ctx.end_enodes(); + for (; it != end; ++it) { + expr * n = (*it)->get_owner(); + expr * r = (*it)->get_root()->get_owner(); + out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl; + } } }; diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index dfddfd12f..5c12cbd8f 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -116,7 +116,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { bv_mdl->eval(a->get_arg(1), exp, true); bv_mdl->eval(a->get_arg(2), sig, true); - SASSERT(a->is_app_of(fu.get_family_id(), OP_FPA_TO_FP)); + SASSERT(a->is_app_of(fu.get_family_id(), OP_FPA_FP)); #ifdef Z3DEBUG SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0); diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 5bc006f00..6b081f0a5 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -22,6 +22,7 @@ Notes: #include"sat_tactic.h" #include"fpa2bv_tactic.h" #include"smt_tactic.h" +#include"propagate_values_tactic.h" #include"qffp_tactic.h" @@ -30,19 +31,19 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("arith_lhs", true); simp_p.set_bool("elim_and", true); - tactic * st = cond( mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), - and_then(mk_simplify_tactic(m, simp_p), - mk_smt_tactic()), - and_then( - mk_simplify_tactic(m, p), - mk_fpa2bv_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - cond(mk_is_propositional_probe(), - mk_sat_tactic(m, p), - mk_smt_tactic(p)), - mk_fail_if_undecided_tactic())); + tactic * st = and_then(mk_simplify_tactic(m, simp_p), + mk_propagate_values_tactic(m, p), + cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + mk_smt_tactic(), + and_then( + mk_fpa2bv_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + mk_bit_blaster_tactic(m, p), + using_params(mk_simplify_tactic(m, p), simp_p), + cond(mk_is_propositional_probe(), + mk_sat_tactic(m, p), + mk_smt_tactic(p)), + mk_fail_if_undecided_tactic()))); st->updt_params(p); return st;