From cf4b7219e10c4fdb1a6533eaab0fe6b7ec892afc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 21 Dec 2014 18:45:36 +0000 Subject: [PATCH] new theory_fpa. plenty of bugs remain. Signed-off-by: Christoph M. Wintersteiger --- src/smt/theory_fpa.cpp | 824 +++++++++++++++++++++++++---------------- src/smt/theory_fpa.h | 86 ++++- 2 files changed, 563 insertions(+), 347 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7552e276b..354dc7596 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -22,7 +22,7 @@ Revision History: #include"theory_bv.h" #include"smt_model_generator.h" -namespace smt { +namespace smt { class fpa_atom_trail : public trail { bool_var m_var; @@ -36,11 +36,60 @@ namespace smt { } }; + void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) { + SASSERT(f->get_family_id() == null_family_id); + SASSERT(f->get_arity() == 0); + expr * r; + if (m_const2bv.find(f, r)) { + result = r; + } + else { + sort * s = f->get_range(); + func_decl *w, *u; + m_th.get_wrap(s, w, u); + expr_ref bv(m); + bv = m.mk_app(w, m.mk_const(f)); + unsigned bv_sz = m_th.m_converter.bu().get_bv_size(bv); + unsigned ebits = m_th.m_converter.fu().get_ebits(f->get_range()); + unsigned sbits = m_th.m_converter.fu().get_sbits(f->get_range()); + 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_const2bv.insert(f, result); + m.inc_ref(f); + m.inc_ref(result); + } + } + + void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) { + SASSERT(f->get_family_id() == null_family_id); + SASSERT(f->get_arity() == 0); + expr * r; + if (m_rm_const2bv.find(f, r)) { + result = r; + } + else { + SASSERT(is_rm(f->get_range())); + + sort * s = f->get_range(); + func_decl *w, *u; + m_th.get_wrap(s, w, u); + result = m.mk_app(w, m.mk_const(f)); + + m_rm_const2bv.insert(f, result); + m.inc_ref(f); + m.inc_ref(result); + } + } + theory_fpa::theory_fpa(ast_manager & m) : theory(m.mk_family_id("float")), - m_converter(m), + m_converter(m, this), m_rw(m, m_converter, params_ref()), - m_trans_map(m), + m_th_rw(m), m_trail_stack(*this) { } @@ -49,45 +98,277 @@ namespace smt { { } - void theory_fpa::add_extra_assertions() + app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { + TRACE("t_fpa", tout << "fpa_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";); + ast_manager & m = m_th.get_manager(); + context & ctx = m_th.get_context(); + theory_id bv_id = m.mk_family_id("bv"); + theory_bv * th_bv = dynamic_cast(ctx.get_theory(bv_id)); + SASSERT(th_bv != 0); + + float_util & fu = m_th.m_converter.fu(); + bv_util & bu = m_th.m_converter.bu(); + mpf_manager & mpfm = fu.fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); + + sort * s = m.get_sort(m_a); + unsigned ebits = fu.get_ebits(s); + unsigned sbits = fu.get_sbits(s); + + scoped_mpz bias(mpzm); + mpzm.power(mpz(2), ebits - 1, bias); + mpzm.dec(bias); + + app * result; + float_op_kind k = (float_op_kind) to_app(m_a)->get_decl_kind(); + switch (k) + { + case -1: { + func_decl *w, *u; + m_th.get_wrap(s, w, u); + rational bv_val(0); + scoped_mpz sgn(mpzm), sig(mpzm), exp(bias); + app_ref bv_w(m); + bv_w = m.mk_app(w, m_a); + + if (!th_bv->get_fixed_value(bv_w, bv_val)) + result = fu.mk_nan(ebits, sbits); + else { + scoped_mpz all_bits(mpzm); + all_bits = bv_val.to_mpq().numerator(); + SASSERT(mpzm.is_one(bv_val.to_mpq().denominator())); + + mpzm.machine_div2k(all_bits, ebits + sbits - 1, sgn); + + scoped_mpz tmp_p(mpzm); + mpzm.power(mpz(2), ebits + sbits - 1, tmp_p); + + if (mpzm.is_one(sgn)) mpzm.sub(all_bits, tmp_p, all_bits); + + mpzm.machine_div2k(all_bits, sbits - 1, exp); + scoped_mpz exp_u(mpzm); + mpzm.sub(exp, bias, exp_u); + SASSERT(mpzm.is_int64(exp_u)); + + mpzm.power(mpz(2), sbits - 1, tmp_p); + mpzm.mod(all_bits, tmp_p, sig); + + scoped_mpf f(mpfm); + mpfm.set(f, ebits, sbits, mpzm.is_one(sgn), sig, mpzm.get_int64(exp_u)); + result = fu.mk_value(f); + } + break; + } + case OP_FLOAT_FP: { + bool is_internalized = ctx.e_internalized(m_a); + if (is_internalized) { + SASSERT(m_a->get_num_args() == 3); + app_ref a_sgn(m), a_sig(m), a_exp(m); + a_sgn = to_app(m_a->get_arg(0)); + a_exp = to_app(m_a->get_arg(1)); + a_sig = to_app(m_a->get_arg(2)); + + scoped_mpz bias(mpzm); + mpzm.power(mpz(2), ebits - 1, bias); + mpzm.dec(bias); + + rational sgn(0), sig(0), exp(bias); + th_bv->get_fixed_value(a_sgn, sgn); + th_bv->get_fixed_value(a_sig, sig); + th_bv->get_fixed_value(a_exp, exp); + + TRACE("t_fpa", tout << "sgn=" << sgn.to_string() << " ; " << + "sig=" << sig.to_string() << " ; " << + "exp=" << exp.to_string() << std::endl;); + + rational exp_u = exp - rational(bias); + SASSERT(exp_u.is_int64()); + + scoped_mpf f(mpfm); + scoped_mpq sig_q(mpqm); + sig_q = sig.to_mpq(); + mpfm.set(f, ebits, sbits, sgn.is_one(), sig_q.get().numerator(), exp_u.get_int64()); + result = fu.mk_value(f); + } + else { + result = fu.mk_nan(ebits, sbits); + } + break; + } + default: + NOT_IMPLEMENTED_YET(); + } + + TRACE("t_fpa", tout << "fpa_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";); + return result; + } + + app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector & values) { + TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";); + ast_manager & m = m_th.get_manager(); + context & ctx = m_th.get_context(); + theory_id bv_id = m.mk_family_id("bv"); + theory_bv * th_bv = dynamic_cast(ctx.get_theory(bv_id)); + + app * result = 0; + mpf_rounding_mode rm; + if (m_th.m_converter.fu().is_rm_value(m_a, rm)) { + result = m_a.get(); + } + else { + sort * s = m.get_sort(m_a); + func_decl *w, *u; + m_th.get_wrap(s, w, u); + + app_ref bv_w(m); + bv_w = m.mk_app(w, m_a); + + rational val(0); + if (ctx.e_internalized(bv_w)) + if (!th_bv->get_fixed_value(bv_w, val)) + val = rational(0); + + switch (val.get_uint64()) + { + case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break; + case BV_RM_TIES_TO_EVEN: result = m_fu.mk_round_nearest_ties_to_even(); break; + case BV_RM_TO_NEGATIVE: result = m_fu.mk_round_toward_negative(); break; + case BV_RM_TO_POSITIVE: result = m_fu.mk_round_toward_positive(); break; + case BV_RM_TO_ZERO: + default: result = m_fu.mk_round_toward_zero(); + } + } + + TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";); + return result; + } + + void theory_fpa::get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap) + { + if (!m_wraps.find(s, wrap) || !m_unwraps.find(s, unwrap)) { + SASSERT(!m_wraps.contains(s)); + ast_manager & m = get_manager(); + sort * bv_srt = 0; + + if (m_converter.is_rm(s)) + bv_srt = m_converter.bu().mk_sort(3); + else { + SASSERT(m_converter.is_float(s)); + unsigned ebits = m_converter.fu().get_ebits(s); + unsigned sbits = m_converter.fu().get_sbits(s); + bv_srt = m_converter.bu().mk_sort(ebits + sbits); + } + + wrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &s, bv_srt); + unwrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s); + m_wraps.insert(s, wrap); + m_unwraps.insert(s, unwrap); + get_context().push_trail(insert_obj_map(m_wraps, s)); + get_context().push_trail(insert_obj_map(m_unwraps, s)); + } + } + + expr_ref theory_fpa::convert_atom(expr * e) { + ast_manager & m = get_manager(); + expr_ref res(m); + proof_ref pr(m); + m_rw(e, res); + + TRACE("t_fpa", tout << "converted atom:" << std::endl; + tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << + mk_ismt2_pp(res, m) << std::endl;); + return res; + } + + expr_ref theory_fpa::convert_term(expr * e) { + ast_manager & m = get_manager(); + expr_ref res(m); + proof_ref pr(m); + m_rw(e, res); + + SASSERT(is_app(res)); + + if (m_converter.fu().is_rm(e)) { + SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT)); + SASSERT(m_converter.bu().get_bv_size(res) == 3); + } + else { + SASSERT(to_app(res)->get_family_id() == get_family_id()); + decl_kind k = to_app(res)->get_decl_kind(); + if (k == OP_FLOAT_TO_FP) { + SASSERT(to_app(res)->get_num_args() == 3); + SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(0)), m_converter.bu().get_family_id(), BV_SORT)); + SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(1)), m_converter.bu().get_family_id(), BV_SORT)); + SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(2)), m_converter.bu().get_family_id(), BV_SORT)); + + expr *sgn, *sig, *exp; + expr_ref s_sgn(m), s_sig(m), s_exp(m); + m_converter.split_triple(res, 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); + } + else { + SASSERT(is_sort_of(m.get_sort(e), get_family_id(), ROUNDING_MODE_SORT)); + SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT)); + } + } + + TRACE("t_fpa", tout << "converted term:" << std::endl; + tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << + mk_ismt2_pp(res, m) << std::endl;); + return res; + } + + expr_ref theory_fpa::mk_side_conditions() { ast_manager & m = get_manager(); context & ctx = get_context(); simplifier & simp = ctx.get_simplifier(); + + expr_ref res(m), t(m); + proof_ref t_pr(m); + res = m.mk_true(); - expr_ref_vector::iterator it = m_converter.extra_assertions.begin(); - expr_ref_vector::iterator end = m_converter.extra_assertions.end(); + expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin(); + expr_ref_vector::iterator end = m_converter.m_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); + simp(*it, t, t_pr); + res = m.mk_and(res, t); } - m_converter.extra_assertions.reset(); + m_converter.m_extra_assertions.reset(); + + TRACE("t_fpa", if (!m.is_true(res)) tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";); + return res; } - 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()); - ast_manager & m = get_manager(); + void theory_fpa::assert_cnstr(expr * e) { + if (get_manager().is_true(e)) return; + TRACE("t_fpa", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); + 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); + } + + void theory_fpa::attach_new_th_var(enode * n) { context & ctx = get_context(); - theory_id bv_tid = ctx.get_theory(m.get_sort(x)->get_family_id())->get_id(); - literal l = mk_eq(x, y, false); - ctx.mk_th_axiom(bv_tid, 1, &l); - ctx.mark_as_relevant(l); + theory_var v = mk_var(n); + ctx.attach_th_var(n, this, v); + m_tvars.push_back(v); + TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";); } bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) { - TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); - SASSERT(atom->get_family_id() == get_family_id()); + TRACE("t_fpa_detail", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); + SASSERT(atom->get_family_id() == get_family_id()); ast_manager & m = get_manager(); context & ctx = get_context(); - simplifier & simp = ctx.get_simplifier(); - bv_util & bu = m_converter.bu(); - expr_ref bv_atom(m); - proof_ref pr(m); if (ctx.b_internalized(atom)) return true; @@ -96,187 +377,157 @@ namespace smt { for (unsigned i = 0; i < num_args; i++) ctx.internalize(atom->get_arg(i), false); - m_rw(atom, bv_atom); - simp(bv_atom, bv_atom, pr); - - ctx.internalize(bv_atom, gate_ctx); - literal def = ctx.get_literal(bv_atom); literal l(ctx.mk_bool_var(atom)); ctx.set_var_theory(l.var(), get_id()); - pred_atom * a = new (get_region()) pred_atom(l, def); - insert_bv2a(l.var(), a); - m_trail_stack.push(fpa_atom_trail(l.var())); + + expr_ref bv_atom(m); + bv_atom = convert_atom(atom); + bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - if (!ctx.relevancy()) { - ctx.mk_th_axiom(get_id(), l, ~def); - ctx.mk_th_axiom(get_id(), ~l, def); - } - - add_extra_assertions(); - + expr_ref atom_iff(m); + assert_cnstr(m.mk_iff(atom, bv_atom)); return true; } bool theory_fpa::internalize_term(app * term) { - TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); + TRACE("t_fpa_detail", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); SASSERT(term->get_family_id() == get_family_id()); SASSERT(!get_context().e_internalized(term)); - + ast_manager & m = get_manager(); context & ctx = get_context(); - simplifier & simp = ctx.get_simplifier(); - bv_util & bu = m_converter.bu(); - sort * term_sort = m.get_sort(term); - expr_ref t(m), bv_term(m); - proof_ref pr(m); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) ctx.internalize(term->get_arg(i), false); + + enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : + ctx.mk_enode(term, false, false, true); - m_rw(term, t); - simp(t, t, pr); + if (is_attached_to_var(e)) + return false; - if (m_converter.is_rm(term_sort)) { - SASSERT(is_app(t)); - expr_ref bv_rm(m); - proof_ref bv_pr(m); - simp(t, bv_rm, bv_pr); + attach_new_th_var(e); + TRACE("t_fpa", tout << "internalized? " << (ctx.e_internalized(term)?"yes":"no") << std::endl;); + return true; + } - bv_term = bv_rm; - } - else if (m_converter.is_float(term_sort)) { - SASSERT(is_app(t) && to_app(t)->get_num_args() == 3); - app * a = to_app(t); - expr_ref sgn(m), sig(m), exp(m); - proof_ref pr_sgn(m), pr_sig(m), pr_exp(m); - simp(a->get_arg(0), sgn, pr_sgn); - simp(a->get_arg(1), sig, pr_sig); - simp(a->get_arg(2), exp, pr_exp); + void theory_fpa::apply_sort_cnstr(enode * n, sort * s) { + 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()); + ast_manager & m = get_manager(); - 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) { - SASSERT(is_app(t)); - expr_ref bv_e(m); - proof_ref bv_pr(m); - simp(t, bv_term, bv_pr); - } - else - NOT_IMPLEMENTED_YET(); - - 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); - - 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); - ctx.attach_th_var(e, this, v); - m_tvars.push_back(v); - TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(term, get_manager()) << " := " << v << "\n";); - SASSERT(e->get_th_var(get_id()) != null_theory_var); - return v != null_theory_var; - } - - void theory_fpa::apply_sort_cnstr(enode * n, sort * s) { - if (!is_attached_to_var(n)) { - TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";); - context & ctx = get_context(); - ast_manager & m = get_manager(); - simplifier & simp = ctx.get_simplifier(); - app * owner = n->get_owner(); - expr_ref converted(m); - proof_ref pr(m); - - theory_var v = mk_var(n); - ctx.attach_th_var(n, this, v); - m_tvars.push_back(v); - m_rw(owner, converted); - simp(converted, converted, pr); - m_trans_map.insert(owner, converted, 0); - - add_extra_assertions(); + if (!is_attached_to_var(n)) + attach_new_th_var(n); - sort * owner_sort = m.get_sort(owner); - if (m_converter.is_rm(owner_sort)) { - bv_util & bu = m_converter.bu(); - 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); + app * owner = n->get_owner(); + sort * owner_sort = m.get_sort(owner); + if (m_converter.is_rm(owner_sort)) { + bv_util & bu = m_converter.bu(); + func_decl *wrap, *unwrap; + get_wrap(owner_sort, wrap, unwrap); + if (owner->get_decl() != unwrap) + { + expr_ref converted(m), t(m); + m_rw(owner, converted); + t = bu.mk_ule(converted, bu.mk_numeral(4, 3)); + assert_cnstr(t); } - - TRACE("t_fpa", tout << "new theory var (const): " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";); } } void theory_fpa::new_eq_eh(theory_var x, theory_var y) { - TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";); ast_manager & m = get_manager(); + + TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl; + tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " = " << + mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl; ); + context & ctx = get_context(); float_util & fu = m_converter.fu(); + bv_util & bu = m_converter.bu(); + mpf_manager & mpfm = fu.fm(); - app * ax = get_enode(x)->get_owner(); - app * ay = get_enode(y)->get_owner(); - expr * ex, *ey; - proof * px, *py; - m_trans_map.get(ax, ex, px); - m_trans_map.get(ay, ey, py); + app * xe = get_enode(x)->get_owner(); + app * ye = get_enode(y)->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); - split_triple(ey, sgn_y, sig_y, exp_y); + if (fu.is_float(xe) && fu.is_float(ye)) + { + expr_ref xc(m), yc(m); + xc = convert_term(xe); + yc = convert_term(ye); - mk_bv_eq(sgn_x, sgn_y); - mk_bv_eq(sig_x, sig_y); - mk_bv_eq(exp_x, exp_y); + expr *x_sgn, *x_sig, *x_exp; + m_converter.split_triple(xc, x_sgn, x_sig, x_exp); + expr *y_sgn, *y_sig, *y_exp; + m_converter.split_triple(yc, y_sgn, y_sig, y_exp); + + expr_ref c(m); + 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)); + assert_cnstr(c); + assert_cnstr(mk_side_conditions()); } - else if (fu.is_rm(get_enode(x)->get_owner())) { - mk_bv_eq(ex, ey); + else if (fu.is_rm(xe) && fu.is_rm(ye)) { + expr_ref xc(m), yc(m); + xc = convert_term(xe); + yc = convert_term(ye); + expr_ref c(m); + c = m.mk_eq(xc, yc); + assert_cnstr(c); + assert_cnstr(mk_side_conditions()); } - else - UNREACHABLE(); + + return; } void theory_fpa::new_diseq_eh(theory_var x, theory_var y) { - TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << "\n";); ast_manager & m = get_manager(); + + TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl; + tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " << + mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;); + context & ctx = get_context(); float_util & fu = m_converter.fu(); + bv_util & bu = m_converter.bu(); + mpf_manager & mpfm = fu.fm(); - app * ax = get_enode(x)->get_owner(); - app * ay = get_enode(y)->get_owner(); - expr * ex, *ey; - proof * px, *py; - m_trans_map.get(ax, ex, px); - m_trans_map.get(ay, ey, py); + app * xe = get_enode(x)->get_owner(); + app * ye = get_enode(y)->get_owner(); - expr_ref deq(m); + if (fu.is_float(xe) && fu.is_float(ye)) + { + expr_ref xc(m), yc(m); + xc = convert_term(xe); + yc = convert_term(ye); - 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); - split_triple(ex, sgn_y, sig_y, exp_y); - - deq = m.mk_or(m.mk_not(m.mk_eq(sgn_x, sgn_y)), - m.mk_not(m.mk_eq(sig_x, sig_y)), - m.mk_not(m.mk_eq(exp_x, exp_y))); - } - else if (fu.is_rm(m.get_sort(get_enode(x)->get_owner()))) { - deq = m.mk_not(m.mk_eq(ex, ey)); + expr *x_sgn, *x_sig, *x_exp; + m_converter.split_triple(xc, x_sgn, x_sig, x_exp); + expr *y_sgn, *y_sig, *y_exp; + m_converter.split_triple(yc, y_sgn, y_sig, y_exp); + + expr_ref c(m); + 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))); + assert_cnstr(c); + assert_cnstr(mk_side_conditions()); } - else - UNREACHABLE(); - - ctx.internalize(deq, true); - ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(deq)); - ctx.mark_as_relevant(deq); + else if (fu.is_rm(xe) && fu.is_rm(ye)) { + expr_ref xc(m), yc(m); + xc = convert_term(xe); + yc = convert_term(ye); + expr_ref c(m); + c = m.mk_not(m.mk_eq(xc, yc)); + assert_cnstr(c); + assert_cnstr(mk_side_conditions()); + } + + return; } void theory_fpa::push_scope_eh() { @@ -289,198 +540,117 @@ namespace smt { m_trail_stack.pop_scope(num_scopes); unsigned num_old_vars = get_old_num_vars(num_scopes); for (unsigned i = num_old_vars; i < get_num_vars(); i++) { - m_trans_map.erase(get_enode(m_tvars[i])->get_owner()); + // m_trans_map.erase(get_enode(m_tvars[i])->get_owner()); } m_tvars.shrink(num_old_vars); theory::pop_scope_eh(num_scopes); - } - - model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { - ast_manager & m = get_manager(); - context & ctx = get_context(); - bv_util & bu = m_converter.bu(); - float_util & fu = m_converter.fu(); - mpf_manager & mpfm = fu.fm(); - unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); - unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); - - theory_var v = n->get_th_var(get_id()); - SASSERT(v != null_theory_var); - expr * fpa_e = get_enode(v)->get_owner(); - TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(fpa_e, m) << "\n";); - - expr * bv_e; - proof * bv_pr; - m_trans_map.get(fpa_e, bv_e, bv_pr); - sort * fpa_e_srt = m.get_sort(fpa_e); - expr_wrapper_proc * res = 0; - - if (fu.is_rm(fpa_e_srt)) { - if (!ctx.e_internalized(bv_e)) - res = alloc(expr_wrapper_proc, fu.mk_round_nearest_ties_to_away()); - else - { - theory_bv * bv_th = (theory_bv*)ctx.get_theory(m.get_family_id("bv")); - rational val; - - bv_th->get_fixed_value(ctx.get_enode(bv_e)->get_owner(), val); // OK to fail - app * fp_val_e; - SASSERT(val.is_uint64()); - switch (val.get_uint64()) - { - case BV_RM_TIES_TO_AWAY: fp_val_e = fu.mk_round_nearest_ties_to_away(); break; - case BV_RM_TIES_TO_EVEN: fp_val_e = fu.mk_round_nearest_ties_to_even(); break; - case BV_RM_TO_NEGATIVE: fp_val_e = fu.mk_round_toward_negative(); break; - case BV_RM_TO_POSITIVE: fp_val_e = fu.mk_round_toward_positive(); break; - case BV_RM_TO_ZERO: - default: fp_val_e = fu.mk_round_toward_zero(); - } - - TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;); - res = alloc(expr_wrapper_proc, fp_val_e); - } - } - else if (fu.is_float(fpa_e_srt)) { - expr * bv_sgn, *bv_sig, *bv_exp; - 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); - - app * e_sgn, *e_sig, *e_exp; - 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() : - bu.mk_numeral(0, 1); - e_sig = (ctx.e_internalized(bv_sig)) ? ctx.get_enode(bv_sig)->get_owner() : - bu.mk_numeral(0, sig_sz); - e_exp = (ctx.e_internalized(bv_exp)) ? ctx.get_enode(bv_exp)->get_owner() : - 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";); - - 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 - bias; - - 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.get().numerator()); - mpqm.set(exp_q, exp_unbiased_r.to_mpq()); - mpzm.set(exp_num, exp_q.get().numerator()); - mpzm.set(sig_z, sig_num); - exp_z = mpzm.get_int64(exp_num); - - scoped_mpf fp_val(mpfm); - mpfm.set(fp_val, ebits, sbits, !sgn_r.is_zero(), sig_z, exp_z); - - 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(); - - return res; - } + } void theory_fpa::assign_eh(bool_var v, bool is_true) { - TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << ")\n";); - /* CMW: okay to ignore? */ - theory::assign_eh(v, is_true); + ast_manager & m = get_manager(); + context & ctx = get_context(); + expr * e = ctx.bool_var2expr(v); + + TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";); + + expr_ref converted(m); + m_rw(e, converted); + converted = m.mk_and(converted, mk_side_conditions()); + if (!is_true) converted = m.mk_not(converted); + assert_cnstr(converted); } void theory_fpa::relevant_eh(app * n) { TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, get_manager()) << "\n";); + + NOT_IMPLEMENTED_YET(); + ast_manager & m = get_manager(); - context & ctx = get_context(); + + if (m.is_bool(n)) + return; + float_util & fu = m_converter.fu(); bv_util & bu = m_converter.bu(); + mpf_manager & mpfm = fu.fm(); - if (m.is_bool(n)) { - bool_var v = ctx.get_bool_var(n); - atom * a = get_bv2a(v); - pred_atom * pa = static_cast(a); - ctx.mark_as_relevant(pa->m_def); - ctx.mk_th_axiom(get_id(), pa->m_var, ~pa->m_def); - ctx.mk_th_axiom(get_id(), ~pa->m_var, pa->m_def); - } - else if (ctx.e_internalized(n)) { - SASSERT(m_trans_map.contains(n)); - expr * ex; - proof * px; - m_trans_map.get(n, ex, px); - sort * n_srt = m.get_sort(n); + if (bu.is_bv(n)) + return; - if (fu.is_rm(n_srt)) { - ctx.mark_as_relevant(ex); - } - else if (fu.is_float(n_srt)) { - expr * bv_sgn, *bv_sig, *bv_exp; - split_triple(ex, bv_sgn, bv_sig, bv_exp); + sort * s = m.get_sort(n); + func_decl *wrap, *unwrap; + get_wrap(s, wrap, unwrap); - ctx.mark_as_relevant(bv_sgn); - ctx.mark_as_relevant(bv_sig); - ctx.mark_as_relevant(bv_exp); - } - else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV || - n->get_decl()->get_decl_kind() == OP_FLOAT_TO_REAL) { - expr_ref eq(m); - app * ex_a = to_app(ex); - if (n->get_id() > ex_a->get_id()) - std::swap(n, ex_a); - eq = m.mk_eq(n, ex_a); - ctx.internalize(eq, false); - literal l = ctx.get_literal(eq); - ctx.mk_th_axiom(get_id(), 1, &l); - ctx.mark_as_relevant(l); + if (n->get_decl() != unwrap) { + expr * wrapped = m.mk_app(wrap, n); + mpf_rounding_mode rm; + scoped_mpf val(mpfm); + if (fu.is_rm_value(n, rm)) + assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rm, 3))); + else if (fu.is_value(n, val)) { + unsigned sz = val.get().get_ebits() + val.get().get_sbits(); + scoped_mpq q(fu.fm().mpq_manager()); + mpfm.to_rational(val, q); + assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rational(q), sz))); } else - NOT_IMPLEMENTED_YET(); + assert_cnstr(m.mk_eq(m.mk_app(unwrap, wrapped), n)); } - else - UNREACHABLE(); } void theory_fpa::reset_eh() { + TRACE("t_fpa", tout << "reset_eh for: " << "\n";); pop_scope_eh(m_trail_stack.get_num_scopes()); m_rw.reset(); - m_trans_map.reset(); m_bool_var2atom.reset(); m_temporaries.reset(); m_tvars.reset(); theory::reset_eh(); } - void theory_fpa::init_model(model_generator & m) { + void theory_fpa::init_model(model_generator & mg) { + TRACE("t_fpa", tout << "initializing model" << std::endl;); m_factory = alloc(fpa_factory, get_manager(), get_family_id()); - m.register_factory(m_factory); + mg.register_factory(m_factory); + TRACE("t_fpa", display(tout);); + } + + 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";); + + ast_manager & m = get_manager(); + float_util & fu = m_converter.fu(); + + expr * owner = n->get_owner(); + sort * o_srt = m.get_sort(owner); + + mpf_rounding_mode rm; + + if (fu.is_rm_value(n->get_owner(), rm)) + return alloc(expr_wrapper_proc, n->get_owner()); + else if (fu.is_value(n->get_owner())) + return alloc(expr_wrapper_proc, n->get_owner()); + else if (fu.is_rm(owner)) + return alloc(fpa_rm_value_proc, this, app_ref(to_app(owner), m)); + else if (fu.is_float(owner)) + return alloc(fpa_value_proc, this, app_ref(to_app(owner), m)); + + UNREACHABLE(); + return 0; + } + + void theory_fpa::finalize_model(model_generator & mg) {} + + void theory_fpa::display(std::ostream & out) const + { + ast_manager & m = get_manager(); + context & ctx = get_context(); + + out << "theory variables:" << std::endl; + ptr_vector::const_iterator it = ctx.begin_enodes(); + ptr_vector::const_iterator end = ctx.end_enodes(); + for (; it != end; it++) + out << (*it)->get_th_var(get_family_id()) << " -> " << + mk_ismt2_pp((*it)->get_owner(), m) << std::endl; } }; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 7b29b82de..0c472be33 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -23,7 +23,9 @@ Revision History: #include"trail.h" #include"fpa2bv_converter.h" #include"fpa2bv_rewriter.h" +#include"th_rewriter.h" #include"value_factory.h" +#include"smt_model_generator.h" namespace smt { @@ -52,8 +54,7 @@ namespace smt { app * mk_value(mpf const & x) { return m_util.mk_value(x); } - }; - + }; class theory_fpa : public theory { class th_trail_stack : public trail_stack { @@ -62,6 +63,45 @@ namespace smt { virtual ~th_trail_stack() {} }; + class fpa2bv_converter_wrapped : public fpa2bv_converter { + public: + theory_fpa & m_th; + fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) : + fpa2bv_converter(m), + m_th(*th) {} + virtual ~fpa2bv_converter_wrapped() {} + virtual void mk_const(func_decl * f, expr_ref & result); + virtual void mk_rm_const(func_decl * f, expr_ref & result); + }; + + class fpa_value_proc : public model_value_proc { + protected: + theory_fpa & m_th; + app_ref m_a; + svector m_dependencies; + public: + fpa_value_proc(theory_fpa * th, app_ref & a) : m_th(*th), m_a(a) {} + void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); } + virtual ~fpa_value_proc() {} + virtual void get_dependencies(buffer & result) { + result.append(m_dependencies.size(), m_dependencies.c_ptr()); + } + virtual app * mk_value(model_generator & mg, ptr_vector & values); + }; + + class fpa_rm_value_proc : public fpa_value_proc { + float_util & m_fu; + bv_util & m_bu; + public: + fpa_rm_value_proc(theory_fpa * th, app_ref & a) : + fpa_value_proc(th, a), + m_fu(th->m_converter.fu()), + m_bu(th->m_converter.bu()) {} + void add_dependency(enode * n) { fpa_value_proc::add_dependency(n); } + virtual ~fpa_rm_value_proc() {} + virtual app * mk_value(model_generator & mg, ptr_vector & values); + }; + public: class atom { public: @@ -79,17 +119,20 @@ namespace smt { void insert_bv2a(bool_var bv, pred_atom * a) { m_bool_var2atom.setx(bv, a, 0); } void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = 0; } pred_atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); } - region & get_region() { return m_trail_stack.get_region(); } + region & get_region() { return m_trail_stack.get_region(); } protected: - fpa2bv_converter m_converter; - fpa2bv_rewriter m_rw; - expr_map m_trans_map; - th_trail_stack m_trail_stack; - bool_var2atom m_bool_var2atom; - enode_vector m_temporaries; - int_vector m_tvars; - fpa_factory * m_factory; + fpa2bv_converter_wrapped m_converter; + fpa2bv_rewriter m_rw; + th_rewriter m_th_rw; + th_trail_stack m_trail_stack; + bool_var2atom m_bool_var2atom; + enode_vector m_temporaries; + vector m_tvars; + fpa_factory * m_factory; + obj_map m_wraps; + obj_map m_unwraps; + float_decl_plugin m_flt_plugin; virtual final_check_status final_check_eh() { return FC_DONE; } virtual bool internalize_atom(app * atom, bool gate_ctx); @@ -108,21 +151,24 @@ namespace smt { void assign_eh(bool_var v, bool is_true); virtual void relevant_eh(app * n); virtual void init_model(model_generator & m); + virtual void finalize_model(model_generator & mg); + public: theory_fpa(ast_manager& m); virtual ~theory_fpa(); - protected: - void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { - SASSERT(is_app_of(e, get_family_id(), OP_FLOAT_TO_FP)); - SASSERT(to_app(e)->get_num_args() == 3); - sgn = to_app(e)->get_arg(0); - sig = to_app(e)->get_arg(1); - exp = to_app(e)->get_arg(2); - } + virtual void display(std::ostream & out) const; + + protected: + expr_ref mk_side_conditions(); + expr_ref convert_atom(expr * e); + expr_ref convert_term(expr * e); + void get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap); + void add_trail(ast * a); - void add_extra_assertions(); void mk_bv_eq(expr * x, expr * y); + void attach_new_th_var(enode * n); + void assert_cnstr(expr * e); }; };