diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 3eeacab247e..3e8376c250b 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -51,11 +51,10 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) : for (auto const& kv : conv.m_uf2bvuf) { m_uf2bvuf.insert(kv.m_key, kv.m_value); m.inc_ref(kv.m_key); - m.inc_ref(kv.m_value.first); - m.inc_ref(kv.m_value.second); + m.inc_ref(kv.m_value); } for (auto const& kv : conv.m_min_max_ufs) { - m_specials.insert(kv.m_key, kv.m_value); + m_min_max_specials.insert(kv.m_key, kv.m_value); m.inc_ref(kv.m_key); m.inc_ref(kv.m_value.first); m.inc_ref(kv.m_value.second); @@ -67,16 +66,15 @@ bv2fpa_converter::~bv2fpa_converter() { dec_ref_map_key_values(m, m_rm_const2bv); for (auto const& kv : m_uf2bvuf) { m.dec_ref(kv.m_key); - m.dec_ref(kv.m_value.first); - m.dec_ref(kv.m_value.second); + m.dec_ref(kv.m_value); } - for (auto const& kv : m_specials) { + for (auto const& kv : m_min_max_specials) { m.dec_ref(kv.m_key); m.dec_ref(kv.m_value.first); m.dec_ref(kv.m_value.second); } m_uf2bvuf.reset(); - m_specials.reset(); + m_min_max_specials.reset(); } expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) { @@ -191,7 +189,7 @@ expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, expr * val) { expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) { expr_ref result(m); - TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for "; + TRACE("bv2fpa_rebuild", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for "; if (e) tout << mk_ismt2_pp(e, m); else tout << "nil"; tout << std::endl; ); @@ -288,13 +286,23 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * expr_ref ft_fres = rebuild_floats(mc, rng, to_app(bv_fres)); m_th_rw(ft_fres); TRACE("bv2fpa", + tout << "func_interp entry #" << i << ":" << std::endl; + tout << "(" << bv_f->get_name(); + for (unsigned i = 0; i < bv_f->get_arity(); i++) + tout << " " << mk_ismt2_pp(bv_args[i], m); + tout << ") = " << mk_ismt2_pp(bv_fres, m) << std::endl; + tout << " --> " << std::endl; + tout << "(" << f->get_name(); for (unsigned i = 0; i < new_args.size(); i++) - tout << mk_ismt2_pp(bv_args[i], m) << " == " << - mk_ismt2_pp(new_args[i], m) << std::endl; - tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;); + tout << " " << mk_ismt2_pp(new_args[i], m); + tout << ") = " << mk_ismt2_pp(ft_fres, m) << std::endl;); func_entry * fe = result->get_entry(new_args.c_ptr()); - if (fe == nullptr) - result->insert_new_entry(new_args.c_ptr(), ft_fres); + if (fe == nullptr) { + // Avoid over-specification of a partially interpreted theory function + if (f->get_family_id() != m_fpa_util.get_family_id() || + m_fpa_util.is_considered_uninterpreted(f, new_args.size(), new_args.c_ptr())) + result->insert_new_entry(new_args.c_ptr(), ft_fres); + } else { // The BV model may have multiple equivalent entries using different // representations of NaN. We can only keep one and we check that @@ -309,6 +317,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * if (bv_els) { expr_ref ft_els = rebuild_floats(mc, rng, bv_els); m_th_rw(ft_els); + TRACE("bv2fpa", tout << "else=" << mk_ismt2_pp(ft_els, m) << std::endl;); result->set_else(ft_els); } } @@ -398,7 +407,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo } void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable & seen) { - for (auto const& kv : m_specials) { + for (auto const& kv : m_min_max_specials) { func_decl * f = kv.m_key; app * pn_cnst = kv.m_value.first; app * np_cnst = kv.m_value.second; @@ -432,8 +441,7 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable & seen) { for (auto const& kv : m_uf2bvuf) { func_decl * f = kv.m_key; - func_decl* f_uf = kv.m_value.first; - expr* f_def = kv.m_value.second; + func_decl * f_uf = kv.m_value; seen.insert(f_uf); if (f->get_arity() == 0) @@ -454,29 +462,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode } } else if (f->get_family_id() == m_fpa_util.get_fid()) { - if (f_def) { - func_interp* fi = alloc(func_interp, m, f->get_arity()); - expr_ref def = rebuild_floats(mc, f->get_range(), to_app(f_def)); - fi->set_else(def); - SASSERT(m.get_sort(def) == f->get_range()); - target_model->register_decl(f, fi); - func_interp* fj = mc->get_func_interp(f_uf); - if (fj) { - target_model->register_decl(f_uf, fj->copy()); - } - continue; - } - + // kv.m_value contains the model for the unspecified cases of kv.m_key in terms of bit-vectors. + // convert_func_interp rebuilds a func_interp on floats. // f is a floating point function: f(x,y) : Float // f_uf is a bit-vector function: f_uf(xB,yB) : BitVec // then there is f_def: f_Bv(xB, yB) := if(range(xB),.., f_uf(xB,yB)) // f(x,y) := to_float(if(range(to_bv(x)), ... f_uf(to_bv(xB), to_bv(yB)))) - not practical - // := if(range_fp(x), ...., to_float(f_uf(...)) - approach - - target_model->register_decl(f, convert_func_interp(mc, f, f_uf)); + // := if(range_fp(x), ...., to_float(f_uf(...)) - approach (via fpa_util::is_considered_uninterpreted) + + func_interp *fi = convert_func_interp(mc, f, f_uf); + if (fi->num_entries() > 0 || fi->get_else() != nullptr) + target_model->register_decl(f, fi); } } + + TRACE("bv2fpa", tout << "Target model: " << *target_model; ); } void bv2fpa_converter::display(std::ostream & out) { @@ -496,9 +497,9 @@ void bv2fpa_converter::display(std::ostream & out) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; unsigned indent = n.size() + 4; - out << mk_ismt2_pp(kv.m_value.first, m, indent) << ")"; + out << mk_ismt2_pp(kv.m_value, m, indent) << ")"; } - for (auto const& kv : m_specials) { + for (auto const& kv : m_min_max_specials) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; unsigned indent = n.size() + 4; @@ -525,22 +526,19 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) { } for (auto const& kv : m_uf2bvuf) { func_decl * k = translator(kv.m_key); - func_decl * v = translator(kv.m_value.first); - expr* d = translator(kv.m_value.second); - res->m_uf2bvuf.insert(k, std::make_pair(v, d)); + func_decl * v = translator(kv.m_value); + res->m_uf2bvuf.insert(k, v); translator.to().inc_ref(k); translator.to().inc_ref(v); - translator.to().inc_ref(d); } - for (auto const& kv : m_specials) { + for (auto const& kv : m_min_max_specials) { func_decl * k = translator(kv.m_key); app * v1 = translator(kv.m_value.first); app * v2 = translator(kv.m_value.second); - res->m_specials.insert(k, std::pair(v1, v2)); + res->m_min_max_specials.insert(k, std::pair(v1, v2)); translator.to().inc_ref(k); translator.to().inc_ref(v1); translator.to().inc_ref(v2); } return res; } - diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h index 778aa10847d..5a16f6d595d 100644 --- a/src/ast/fpa/bv2fpa_converter.h +++ b/src/ast/fpa/bv2fpa_converter.h @@ -34,8 +34,8 @@ class bv2fpa_converter { obj_map m_const2bv; obj_map m_rm_const2bv; - obj_map> m_uf2bvuf; - obj_map > m_specials; + obj_map m_uf2bvuf; + obj_map > m_min_max_specials; public: bv2fpa_converter(ast_manager & m); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f5468af698c..4044e05a315 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3203,7 +3203,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); - unsigned ebits = m_util.get_ebits(xs); unsigned sbits = m_util.get_sbits(xs); @@ -4166,8 +4165,7 @@ void fpa2bv_converter::reset() { dec_ref_map_key_values(m, m_rm_const2bv); for (auto const& kv : m_uf2bvuf) { m.dec_ref(kv.m_key); - m.dec_ref(kv.m_value.first); - m.dec_ref(kv.m_value.second); + m.dec_ref(kv.m_value); } for (auto const& kv : m_min_max_ufs) { m.dec_ref(kv.m_key); @@ -4180,36 +4178,13 @@ void fpa2bv_converter::reset() { } func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) { - std::pair res; + func_decl* res; if (!m_uf2bvuf.find(f, res)) { - res.first = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range); - res.second = nullptr; + res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range); m.inc_ref(f); - m.inc_ref(res.first); + m.inc_ref(res); m_uf2bvuf.insert(f, res); - TRACE("fpa2bv", tout << "New UF func_decl: " << res.first->get_id() << std::endl << mk_ismt2_pp(res.first, m) << std::endl;); + TRACE("fpa2bv", tout << "New UF func_decl: " << res->get_id() << std::endl << mk_ismt2_pp(res, m) << std::endl;); } - return res.first; -} - -expr* fpa2bv_converter::get_bv_def(func_decl* f) { - std::pair res(nullptr, nullptr); - m_uf2bvuf.find(f, res); - TRACE("fpa2bv", tout << "get_bv_def " << mk_ismt2_pp(res.first, m) << " " << res.second << std::endl;); - return res.second; -} - -/** - \brief expand the definition of bit-vector function f - as an expression of what is defined and what is not - defined. -*/ -void fpa2bv_converter::set_bv_def(func_decl* f, expr* def) { - auto res = m_uf2bvuf[f]; - SASSERT(res.first); - SASSERT(!res.second); - res.second = def; - m.inc_ref(def); - m_uf2bvuf.insert(f, res); - + return res; } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 85a866bc083..1eb2de136e7 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -35,7 +35,7 @@ class fpa2bv_converter { public: typedef obj_map > special_t; typedef obj_map const2bv_t; - typedef obj_map > uf2bvuf_t; + typedef obj_map uf2bvuf_t; protected: ast_manager & m; @@ -219,8 +219,6 @@ class fpa2bv_converter { void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range); - void set_bv_def(func_decl * f, expr* def); - expr* get_bv_def(func_decl * f); expr_ref nan_wrap(expr * n); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 1e693b29a85..daf197806b8 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -19,6 +19,7 @@ Revision History: #include "ast/fpa_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "ast/ast_smt2_pp.h" fpa_decl_plugin::fpa_decl_plugin(): m_values(m_fm), @@ -68,6 +69,10 @@ void fpa_decl_plugin::recycled_id(unsigned id) { m_fm.del(m_values[id]); } +bool fpa_decl_plugin::is_considered_uninterpreted(func_decl * f) { + return false; +} + func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) { sort * s = mk_float_sort(v.get_ebits(), v.get_sbits()); func_decl * r = nullptr; @@ -1044,3 +1049,44 @@ bool fpa_util::contains_floats(ast * a) { return false; } + +bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) { + TRACE("fpa_util", expr_ref t(m().mk_app(f, n, args), m()); tout << mk_ismt2_pp(t, m()) << std::endl; ); + + family_id ffid = plugin().get_family_id(); + if (f->get_family_id() != ffid) + return false; + + if (is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV)) { + SASSERT(n == 1); + expr* x = args[0]; + return is_nan(x); + } + else if (is_decl_of(f, ffid, OP_FPA_TO_SBV) || + is_decl_of(f, ffid, OP_FPA_TO_UBV)) { + SASSERT(n == 2); + SASSERT(f->get_num_parameters() == 1); + bool is_signed = f->get_decl_kind() == OP_FPA_TO_SBV; + expr* rm = args[0]; + expr* x = args[1]; + unsigned bv_sz = f->get_parameter(0).get_int(); + mpf_rounding_mode rmv; + mpf v; + if (!is_rm_numeral(rm, rmv) || !is_numeral(x, v)) return false; + if (is_nan(x) || is_inf(x)) return true; + unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager(); + scoped_mpq r(mpqm); + plugin().fm().to_sbv_mpq(rmv, v, r); + if (is_signed) + return mpqm.bitsize(r) >= bv_sz; + else + return mpqm.is_neg(r) || mpqm.bitsize(r) > bv_sz; + } + else if (is_decl_of(f, ffid, OP_FPA_TO_REAL)) { + SASSERT(n == 1); + expr* x = args[0]; + return is_nan(x) || is_inf(x); + } + + return plugin().is_considered_uninterpreted(f); +} diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index dbd2faf35a9..d4b877a3ac6 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -163,8 +163,6 @@ class fpa_decl_plugin : public decl_plugin { unsigned mk_id(mpf const & v); void recycled_id(unsigned id); - bool is_considered_uninterpreted(func_decl * f) override { return false; } - public: fpa_decl_plugin(); @@ -199,6 +197,8 @@ class fpa_decl_plugin : public decl_plugin { void del(parameter const & p) override; parameter translate(parameter const & p, decl_plugin & target) override; + + bool is_considered_uninterpreted(func_decl * f) override; }; class fpa_util { @@ -358,6 +358,8 @@ class fpa_util { bool contains_floats(ast * a); + bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args); + MATCH_TERNARY(is_fp); }; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index c06edd1e51e..237a8c5a19e 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -53,6 +53,7 @@ struct evaluator_cfg : public default_rewriter_cfg { seq_rewriter m_seq_rw; array_util m_ar; arith_util m_au; + fpa_util m_fpau; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; @@ -78,6 +79,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_seq_rw(m), m_ar(m), m_au(m), + m_fpau(m), m_pinned(m) { bool flat = true; m_b_rw.set_flat(flat); @@ -132,9 +134,9 @@ struct evaluator_cfg : public default_rewriter_cfg { return false; } - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -148,7 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg { family_id fid = f->get_family_id(); bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); br_status st = BR_FAILED; - TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";); + TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";); if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f) expr * val = m_model.get_const_interp(f); if (val != nullptr) { @@ -195,8 +197,8 @@ struct evaluator_cfg : public default_rewriter_cfg { result = m.mk_false(); st = BR_DONE; } - TRACE("model_evaluator", - tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " " + TRACE("model_evaluator", + tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " " << mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";); if (st != BR_FAILED) return st; @@ -324,7 +326,14 @@ struct evaluator_cfg : public default_rewriter_cfg { result = nullptr; result_pr = nullptr; + if (f->get_family_id() == m_fpau.get_family_id() && + !m_fpau.is_considered_uninterpreted(f, num, args)) { + // cwinter: should this be unreachable? + return BR_FAILED; + } + func_interp * fi = m_model.get_func_interp(f); + if (fi) { if (fi->is_partial()) fi->set_else(m.get_some_value(f->get_range())); @@ -338,6 +347,10 @@ struct evaluator_cfg : public default_rewriter_cfg { result = m_au.mk_numeral(rational(0), f->get_range()); return BR_DONE; } + else if (m_fpau.is_considered_uninterpreted(f, num, args)) { + result = m.get_some_value(f->get_range()); + return BR_DONE; + } return BR_FAILED; } @@ -524,7 +537,7 @@ struct evaluator_cfg : public default_rewriter_cfg { func_decl* f = m_ar.get_as_array_func_decl(to_app(a)); func_interp* g = m_model.get_func_interp(f); - if (!g) return false; + if (!g) return false; else_case = g->get_else(); if (!else_case) { TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);