diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 6df96b700..e49701a33 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -26,7 +26,6 @@ Revision History: #include "smt/smt_model_generator.h" #include "smt/proto_model/proto_model.h" #include "model/model_v2_pp.h" -#include "smt/theory_fpa.h" namespace smt { @@ -133,11 +132,6 @@ namespace smt { root2proc.insert(r, proc); } } - - theory * fpa_th = m_context->get_theory(m.mk_family_id("fpa")); - if (fpa_th) { - static_cast(fpa_th)->register_fpa2bv_processors(*this, root2proc, roots, procs); - } } model_value_proc* model_generator::mk_model_value(enode* r) { @@ -376,22 +370,18 @@ namespace smt { enode * child = d.get_enode(); TRACE(mg_top_sort, tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";); - child = child->get_root(); - app * child_val = nullptr; - m_root2value.find(child, child_val); - CTRACE("mg", !child_val, - tout << "null dependency value for: " << mk_pp(child->get_expr(), m) << "\n";); - dependency_values.push_back(child_val); - } - } - val = proc->mk_value(*this, dependency_values); - } - register_value(val); - m_asts.push_back(val); - m_root2value.insert(n, val); - } - } - // send model + child = child->get_root(); + dependency_values.push_back(m_root2value[child]); + } + } + val = proc->mk_value(*this, dependency_values); + } + register_value(val); + m_asts.push_back(val); + m_root2value.insert(n, val); + } + } + // send model for (enode * n : m_context->enodes()) { if (is_uninterp_const(n->get_expr()) && m_context->is_relevant(n)) { func_decl * d = n->get_expr()->get_decl(); @@ -413,9 +403,7 @@ namespace smt { } app * model_generator::get_value(enode * n) const { - app * val = nullptr; - m_root2value.find(n->get_root(), val); - return val; + return m_root2value[n->get_root()]; } /** diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 3e5c7d2d7..962e44d27 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -472,6 +472,22 @@ namespace smt { wu = m.mk_eq(m_converter.unwrap(wrapped, n->get_sort()), n); TRACE(t_fpa, tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;); assert_cnstr(wu); + + // For non-FPA-family terms (e.g. datatype accessors like + // get-fp), mk_uf creates a separate BV UF that is not + // linked to bvwrap. Assert wrap(n) == concat(conv_components) + // to close the constraint gap (same pattern as numerals above). + if (n->get_family_id() != get_family_id()) { + expr_ref conv_e = convert(n); + if (m_fpa_util.is_fp(conv_e) && to_app(conv_e)->get_num_args() == 3) { + app_ref conv_a(m); + conv_a = to_app(conv_e.get()); + expr_ref cc(m); + cc = m_bv_util.mk_concat({conv_a->get_arg(0), conv_a->get_arg(1), conv_a->get_arg(2)}); + assert_cnstr(m.mk_eq(wrapped, cc)); + assert_cnstr(mk_side_conditions()); + } + } } } } @@ -647,101 +663,6 @@ namespace smt { } } - app * theory_fpa::fpa2bv_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) { - ast_manager & m = m_th.get_manager(); - fpa_util & fu = m_th.m_fpa_util; - bv_util & bu = m_th.m_bv_util; - context & ctx = m_th.get_context(); - - app * fpa_val = (values.empty() || !values[0]) ? nullptr : to_app(values[0]); - if (!fpa_val) { - if (!mg.get_root2value().find(m_fpa_n, fpa_val)) { - datatype_util dt(m); - expr * expr_n = m_fpa_n->get_expr(); - if (is_app(expr_n) && to_app(expr_n)->get_num_args() == 1) { - func_decl * f = to_app(expr_n)->get_decl(); - if (dt.is_accessor(f)) { - enode * arg_n = m_fpa_n->get_arg(0)->get_root(); - app * arg_val = nullptr; - if (mg.get_root2value().find(arg_n, arg_val)) { - if (dt.is_constructor(arg_val)) { - ptr_vector const * accessors = dt.get_constructor_accessors(arg_val->get_decl()); - if (accessors) { - for (unsigned i = 0; i < accessors->size(); ++i) { - if ((*accessors)[i] == f) { - expr * acc_val = arg_val->get_arg(i); - if (m.is_value(acc_val)) { - fpa_val = to_app(acc_val); - } - else if (is_app(acc_val) && ctx.e_internalized(acc_val)) { - enode * acc_n = ctx.get_enode(acc_val)->get_root(); - mg.get_root2value().find(acc_n, fpa_val); - } - break; - } - } - } - } - } - } - } - } - } - - if (!fpa_val) { - TRACE("fpa", tout << "fpa2bv_value_proc: defaulting to +0.0 for " << mk_pp(m_fpa_n->get_expr(), m) << "\n";); - fpa_val = fu.mk_pzero(m_ebits, m_sbits); - } - - scoped_mpf v(fu.fm()); - if (fu.is_numeral(fpa_val, v)) { - expr_ref result_fp(m); - m_th.m_converter.mk_numeral(fpa_val->get_sort(), v, result_fp); - if (fu.is_fp(result_fp)) { - expr * sgn = to_app(result_fp)->get_arg(0); - expr * exp = to_app(result_fp)->get_arg(1); - expr * sig = to_app(result_fp)->get_arg(2); - return bu.mk_concat(bu.mk_concat(sgn, exp), sig); - } - } - return bu.mk_numeral(0, m_ebits + m_sbits); - } - - void theory_fpa::register_fpa2bv_processors(model_generator & mg, obj_map & root2proc, ptr_vector & roots, ptr_vector & procs) { - for (auto const& kv : m_conversions) { - expr * fpa_expr = kv.m_key; - expr * bv_expr = kv.m_value; - if (ctx.e_internalized(fpa_expr) && ctx.e_internalized(bv_expr) && m_fpa_util.is_float(fpa_expr)) { - app_ref owner(m); - owner = get_ite_value(fpa_expr); - if (!owner || owner->get_family_id() == get_family_id()) - continue; - - enode * fpa_n = ctx.get_enode(fpa_expr)->get_root(); - enode * bv_n = ctx.get_enode(bv_expr)->get_root(); - - // if (!root2proc.contains(fpa_n)) - // continue; - - if (root2proc.contains(bv_n)) { - if (dynamic_cast(root2proc[bv_n])) - continue; - } - - unsigned ebits = m_fpa_util.get_ebits(fpa_expr->get_sort()); - unsigned sbits = m_fpa_util.get_sbits(fpa_expr->get_sort()); - model_value_proc * proc = alloc(fpa2bv_value_proc, this, ebits, sbits, fpa_n); - procs.push_back(proc); - - bool is_new = !root2proc.contains(bv_n); - root2proc.insert(bv_n, proc); - if (is_new) { - roots.push_back(bv_n); - } - } - } - } - void theory_fpa::display(std::ostream & out) const { diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index a142c56bf..badce4e2a 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -56,22 +56,6 @@ namespace smt { app * mk_value(model_generator & mg, expr_ref_vector const & values) override; }; - class fpa2bv_value_proc : public model_value_proc { - theory_fpa & m_th; - unsigned m_ebits; - unsigned m_sbits; - enode * m_fpa_n; - public: - fpa2bv_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits, enode * fpa_n) : - m_th(*th), m_ebits(ebits), m_sbits(sbits), m_fpa_n(fpa_n) {} - - void get_dependencies(buffer & result) override { - result.push_back(model_value_dependency(m_fpa_n)); - } - - app * mk_value(model_generator & mg, expr_ref_vector const & values) override; - }; - class fpa_rm_value_proc : public model_value_proc { theory_fpa & m_th; ast_manager & m; @@ -126,7 +110,6 @@ namespace smt { public: theory_fpa(context& ctx); - void register_fpa2bv_processors(model_generator & mg, obj_map & root2proc, ptr_vector & roots, ptr_vector & procs); ~theory_fpa() override; void display(std::ostream & out) const override; @@ -144,3 +127,4 @@ namespace smt { }; }; +