From ca89b120d3b2c1ebb83eb996f022425c701768db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 11 Jun 2014 16:44:12 +0100 Subject: [PATCH] improve FPA theory implementation Signed-off-by: Christoph M. Wintersteiger --- src/smt/theory_fpa.cpp | 239 ++++++++++++++++++++++++++++------------- src/smt/theory_fpa.h | 7 +- 2 files changed, 170 insertions(+), 76 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index bd95d78f1..e606857e5 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -19,27 +19,32 @@ Revision History: #include"ast_smt2_pp.h" #include"smt_context.h" #include"theory_fpa.h" +#include"theory_bv.h" #include"smt_model_generator.h" namespace smt { - theory_fpa::theory_fpa(ast_manager & m) : - theory(m.mk_family_id("float")), - m_converter(m), + theory_fpa::theory_fpa(ast_manager & m) : + theory(m.mk_family_id("float")), + m_converter(m), m_rw(m, m_converter, params_ref()), m_trans_map(m), m_trail_stack(*this) { } + theory_fpa::~theory_fpa() + { + } + bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) { - TRACE("fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); + TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); SASSERT(atom->get_family_id() == get_family_id()); NOT_IMPLEMENTED_YET(); } bool theory_fpa::internalize_term(app * term) { - TRACE("fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); + TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); SASSERT(term->get_family_id() == get_family_id()); SASSERT(!get_context().e_internalized(term)); @@ -55,7 +60,7 @@ namespace smt { m_rw(term, res); SASSERT(is_app(res) && to_app(res)->get_num_args() == 3); app * a = to_app(res); - TRACE("fpa", tout << "converted: " << mk_ismt2_pp(res, get_manager()) << "\n";); + TRACE("t_fpa", tout << "converted: " << mk_ismt2_pp(res, get_manager()) << "\n";); expr_ref sgn(m), sig(m), exp(m); proof_ref pr_sgn(m), pr_sig(m), pr_exp(m); @@ -63,20 +68,34 @@ namespace smt { simp(a->get_arg(1), sig, pr_sig); simp(a->get_arg(2), exp, pr_exp); - ctx.internalize(sgn, false); - ctx.internalize(sig, false); - ctx.internalize(exp, false); + expr_ref bv_v_sgn(m), bv_v_sig(m), bv_v_exp(m); + bv_v_sgn = m.mk_fresh_const("fpa2bv", m.get_sort(sgn)); + bv_v_sig = m.mk_fresh_const("fpa2bv", m.get_sort(sig)); + bv_v_exp = m.mk_fresh_const("fpa2bv", m.get_sort(exp)); + expr_ref e1(m), e2(m), e3(m); + e1 = m.mk_eq(bv_v_sgn, sgn); + e2 = m.mk_eq(bv_v_sig, sig); + e3 = m.mk_eq(bv_v_exp, exp); + ctx.internalize(e1, false); + ctx.internalize(e2, false); + ctx.internalize(e3, false); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e1)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e2)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e3)); + ctx.mark_as_relevant(e1); + ctx.mark_as_relevant(e2); + ctx.mark_as_relevant(e3); expr_ref s_term(m); - m_converter.mk_triple(sgn, sig, exp, s_term); + m_converter.mk_triple(bv_v_sgn, bv_v_sig, bv_v_exp, s_term); SASSERT(!m_trans_map.contains(term)); m_trans_map.insert(term, s_term, 0); enode * e = ctx.mk_enode(term, false, false, true); - theory_var v = mk_var(e); + theory_var v = mk_var(e); ctx.attach_th_var(e, this, v); - TRACE("fpa", tout << "new theory var: " << mk_ismt2_pp(term, get_manager()) << " := " << v << "\n";); + 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; @@ -84,6 +103,7 @@ namespace smt { 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(); @@ -96,7 +116,12 @@ namespace smt { m_trans_map.insert(owner, converted, 0); if (m_converter.is_rm_sort(m.get_sort(owner))) { - ctx.internalize(converted, false); + expr_ref bv_v(m), eq(m); + bv_v = m.mk_fresh_const("fpa2bv", m.get_sort(converted)); + eq = m.mk_eq(bv_v, converted); + ctx.internalize(eq, false); + literal l = ctx.get_literal(eq); + ctx.mk_th_axiom(get_id(), 1, &l); } else { app * a = to_app(converted); @@ -109,14 +134,32 @@ namespace smt { ctx.internalize(sgn, false); ctx.internalize(sig, false); ctx.internalize(exp, false); + + expr_ref bv_v_sgn(m), bv_v_sig(m), bv_v_exp(m); + bv_v_sgn = m.mk_fresh_const("fpa2bv", m.get_sort(sgn)); + bv_v_sig = m.mk_fresh_const("fpa2bv", m.get_sort(sig)); + bv_v_exp = m.mk_fresh_const("fpa2bv", m.get_sort(exp)); + expr_ref e1(m), e2(m), e3(m); + e1 = m.mk_eq(bv_v_sgn, sgn); + e2 = m.mk_eq(bv_v_sig, sig); + e3 = m.mk_eq(bv_v_exp, exp); + ctx.internalize(e1, true); + ctx.internalize(e2, true); + ctx.internalize(e3, true); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e1)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e2)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e3)); + ctx.mark_as_relevant(e1); + ctx.mark_as_relevant(e2); + ctx.mark_as_relevant(e3); } - TRACE("fpa", tout << "new const: " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";); + 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("fpa", tout << "new eq: " << x << " = " << y << "\n";); + TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";); ast_manager & m = get_manager(); context & ctx = get_context(); app * ax = get_enode(x)->get_owner(); @@ -132,9 +175,6 @@ namespace smt { split_triple(ex, sgn_x, sig_x, exp_x); split_triple(ey, sgn_y, sig_y, exp_y); - literal_vector lits; - lits.push_back(mk_eq(ax, ay, true)); - expr_ref e1(m), e2(m), e3(m); e1 = m.mk_eq(sgn_x, sgn_y); e2 = m.mk_eq(sig_x, sig_y); @@ -142,15 +182,16 @@ namespace smt { ctx.internalize(e1, true); ctx.internalize(e2, true); ctx.internalize(e3, true); - lits.push_back(ctx.get_literal(e1)); - lits.push_back(ctx.get_literal(e2)); - lits.push_back(ctx.get_literal(e3)); - - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e1)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e2)); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e3)); + ctx.mark_as_relevant(e1); + ctx.mark_as_relevant(e2); + ctx.mark_as_relevant(e3); } void theory_fpa::new_diseq_eh(theory_var x, theory_var y) { - TRACE("fpa", tout << "new eq: " << x << " = " << y << "\n";); + TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";); ast_manager & m = get_manager(); context & ctx = get_context(); app * ax = get_enode(x)->get_owner(); @@ -166,9 +207,13 @@ namespace smt { split_triple(ex, sgn_x, sig_x, exp_x); split_triple(ex, sgn_y, sig_y, exp_y); - ctx.internalize(m.mk_not(m.mk_eq(sgn_x, sgn_y)), true); - ctx.internalize(m.mk_not(m.mk_eq(sig_x, sig_y)), true); - ctx.internalize(m.mk_not(m.mk_eq(exp_x, exp_y)), true); + expr_ref e1(m), e2(m), e3(m); + e1 = m.mk_not(m.mk_eq(sgn_x, sgn_y)); + e2 = m.mk_or(e1, m.mk_not(m.mk_eq(sig_x, sig_y))); + e3 = m.mk_or(e2, m.mk_not(m.mk_eq(exp_x, exp_y))); + ctx.internalize(e3, true); + ctx.mk_th_axiom(get_id(), 1, &ctx.get_literal(e3)); + ctx.mark_as_relevant(e3); } void theory_fpa::push_scope_eh() { @@ -186,13 +231,14 @@ namespace smt { context & ctx = get_context(); bv_util & bu = m_converter.bu(); float_util & fu = m_converter.fu(); - unsynch_mpz_manager & mpzm = fu.fm().mpz_manager(); - unsynch_mpq_manager & mpqm = fu.fm().mpq_manager(); + 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("fpa", tout << "mk_value for: " << mk_ismt2_pp(fpa_e, m) << "\n";); + TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(fpa_e, m) << "\n";); expr * bv_e; proof * bv_pr; @@ -204,17 +250,14 @@ namespace smt { SASSERT(ctx.e_internalized(bv_e)); sort * s = m.get_sort(bv_e); family_id fid = s->get_family_id(); - theory * bv_th = ctx.get_theory(fid); - - enode * ev = ctx.get_enode(bv_e); - ptr_vector pve; - app_ref mv(m); - mv = ((expr_wrapper_proc*)bv_th->mk_value(ev, mg))->mk_value(mg, pve); - - rational val(0); - unsigned sz = 0; - if (bu.is_numeral(mv, val, sz)) { - app_ref fp_val_e(m); + theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid); + rational val; + if (!bv_th->get_fixed_value(ctx.get_enode(bv_e)->get_owner(), val)) { + NOT_IMPLEMENTED_YET(); + } + else + { + app * fp_val_e; SASSERT(val.is_uint64()); switch (val.get_uint64()) { @@ -226,9 +269,8 @@ namespace smt { default: fp_val_e = fu.mk_round_toward_zero(); } - TRACE("fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;); + 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); - m.inc_ref(fp_val_e); } } else { @@ -241,53 +283,100 @@ namespace smt { enode * e_sgn = ctx.get_enode(bv_sgn); enode * e_sig = ctx.get_enode(bv_sig); - enode * e_exp = ctx.get_enode(bv_exp); + enode * e_exp = ctx.get_enode(bv_exp); + + TRACE("t_fpa", tout << "bv rep: [" << mk_ismt2_pp(e_sgn->get_owner(), m) << " " + << mk_ismt2_pp(e_sig->get_owner(), m) << " " + << mk_ismt2_pp(e_exp->get_owner(), m) << "]\n";); sort * s = m.get_sort(e_sgn->get_owner()); family_id fid = s->get_family_id(); - theory * bv_th = ctx.get_theory(fid); + theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid); - expr_wrapper_proc * mv_sgn = (expr_wrapper_proc*)bv_th->mk_value(e_sgn, mg); - expr_wrapper_proc * mv_sig = (expr_wrapper_proc*)bv_th->mk_value(e_sig, mg); - expr_wrapper_proc * mv_exp = (expr_wrapper_proc*)bv_th->mk_value(e_exp, mg); + SASSERT(bv_th->is_attached_to_var(e_sgn)); + SASSERT(bv_th->is_attached_to_var(e_sig)); + SASSERT(bv_th->is_attached_to_var(e_exp)); - ptr_vector pve; - app_ref bvm_sgn(m), bvm_sig(m), bvm_exp(m); - bvm_sgn = mv_sgn->mk_value(mg, pve); - bvm_sig = mv_sig->mk_value(mg, pve); - bvm_exp = mv_exp->mk_value(mg, pve); + unsigned sig_sz, exp_sz; + sig_sz = bu.get_bv_size(e_sig->get_owner()); + exp_sz = bu.get_bv_size(e_exp->get_owner()); - TRACE("fpa", tout << "bv model: [" << mk_ismt2_pp(bvm_sgn, get_manager()) << " " - << mk_ismt2_pp(bvm_sig, get_manager()) << " " - << mk_ismt2_pp(bvm_exp, get_manager()) << "]\n";); + rational sgn_r(0), sig_r(0), exp_r(0); + + if (!bv_th->get_fixed_value(e_sgn->get_owner(), sgn_r) || + !bv_th->get_fixed_value(e_sig->get_owner(), sig_r) || + !bv_th->get_fixed_value(e_exp->get_owner(), exp_r)) { + NOT_IMPLEMENTED_YET(); + } + else { + TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " " + << sig_r.to_string() << " " + << exp_r.to_string() << "]\n";); - unsigned sgn_sz, sig_sz, exp_sz; - rational sgn_q(0), sig_q(0), exp_q(0); - if (bvm_sgn) bu.is_numeral(bvm_sgn, sgn_q, sgn_sz); - if (bvm_sig) bu.is_numeral(bvm_sig, sig_q, sig_sz); - if (bvm_exp) bu.is_numeral(bvm_exp, exp_q, exp_sz); + // un-bias exponent + rational exp_unbiased_r; + exp_unbiased_r = exp_r - mpfm.m_powers2.m1(exp_sz - 1); - // un-bias exponent - rational exp_unbiased_q; - exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(exp_sz - 1); + mpz sig_z; mpf_exp_t exp_z; + mpq sig_q, exp_q; + mpz sig_num, exp_num; + mpqm.set(sig_q, sig_r.to_mpq()); + mpzm.set(sig_num, sig_q.numerator()); + mpqm.set(exp_q, exp_unbiased_r.to_mpq()); + mpzm.set(exp_num, exp_q.numerator()); + mpzm.set(sig_z, sig_num); + exp_z = mpzm.get_int64(exp_num); - mpz sig_z; mpf_exp_t exp_z; - mpzm.set(sig_z, sig_q.to_mpq().numerator()); - exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); + mpf fp_val; + mpfm.set(fp_val, exp_sz, sig_sz + 1, !sgn_r.is_zero(), sig_z, exp_z); - mpf fp_val; - fu.fm().set(fp_val, exp_sz, sig_sz+1, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); + app * fp_val_e; + fp_val_e = fu.mk_value(fp_val); - app_ref fp_val_e(m); - fp_val_e = fu.mk_value(fp_val); - mpzm.del(sig_z); + TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;); - TRACE("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); - m.inc_ref(fp_val_e); + res = alloc(expr_wrapper_proc, fp_val_e); + } } return res; } + + void theory_fpa::assign_eh(bool_var v, bool is_true) { + TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << ")\n";); + UNREACHABLE(); + } + + void theory_fpa::relevant_eh(app * n) { + ast_manager & m = get_manager(); + context & ctx = get_context(); + float_util & fu = m_converter.fu(); + if (ctx.e_internalized(n)) { + SASSERT(m_trans_map.contains(n)); + expr * ex; + proof * px; + m_trans_map.get(n, ex, px); + + if (fu.is_rm(m.get_sort(n))) { + ctx.mark_as_relevant(ex); + } + else { + expr * bv_sgn, *bv_sig, *bv_exp; + split_triple(ex, bv_sgn, bv_sig, bv_exp); + + ctx.mark_as_relevant(bv_sgn); + ctx.mark_as_relevant(bv_sig); + ctx.mark_as_relevant(bv_exp); + } + } + else + NOT_IMPLEMENTED_YET(); + } }; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 51e0ff0d5..4a465ada2 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -44,9 +44,12 @@ namespace smt { virtual char const * get_name() const { return "fpa"; } virtual model_value_proc * mk_value(enode * n, model_generator & mg); - + + void assign_eh(bool_var v, bool is_true); + virtual void relevant_eh(app * n); public: theory_fpa(ast_manager& m); + virtual ~theory_fpa(); protected: void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { @@ -56,6 +59,8 @@ namespace smt { sig = to_app(e)->get_arg(1); exp = to_app(e)->get_arg(2); } + + void ensure_bv_var(expr_ref const & n); }; };