From df81ab72f53a92ce07ab1d628d4d80a292680d00 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 17 May 2016 16:35:45 +0100 Subject: [PATCH] Bug and performance fixes for FP UFs. --- src/ast/rewriter/fpa_rewriter.cpp | 48 +++++++++++++-- src/ast/rewriter/fpa_rewriter.h | 3 + src/smt/theory_fpa.cpp | 39 +++++++++++- src/smt/theory_fpa.h | 1 + src/tactic/fpa/fpa2bv_model_converter.cpp | 73 ++++++++++++----------- 5 files changed, 122 insertions(+), 42 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 619d5ffbf..6c199fcd8 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -100,18 +100,17 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); st = BR_FAILED; break; case OP_FPA_INTERNAL_RM: - SASSERT(num_args == 1); st = mk_rm(args[0], result); break; + SASSERT(num_args == 1); SASSERT(num_args == 1); st = mk_rm(args[0], result); break; case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: st = BR_FAILED; - - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: - st = BR_FAILED; break; + case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; + case OP_FPA_INTERNAL_BVUNWRAP: SASSERT(num_args == 1); st = mk_bvunwrap(args[0], result); break; + default: NOT_IMPLEMENTED_YET(); } @@ -892,3 +891,42 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { return BR_FAILED; } + + +br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) { + if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) { + bv_util bu(m()); + SASSERT(to_app(arg)->get_num_args() == 3); + sort_ref fpsrt(m()); + fpsrt = to_app(arg)->get_decl()->get_range(); + expr_ref a0(m()), a1(m()), a2(m()); + a0 = to_app(arg)->get_arg(0); + a1 = to_app(arg)->get_arg(1); + a2 = to_app(arg)->get_arg(2); + if (bu.is_extract(a0) && bu.is_extract(a1) && bu.is_extract(a2)) { + unsigned w0 = bu.get_extract_high(a0) - bu.get_extract_low(a0) + 1; + unsigned w1 = bu.get_extract_high(a1) - bu.get_extract_low(a1) + 1; + unsigned w2 = bu.get_extract_high(a2) - bu.get_extract_low(a2) + 1; + unsigned cw = w0 + w1 + w2; + if (cw == m_util.get_ebits(fpsrt) + m_util.get_sbits(fpsrt)) { + expr_ref aa0(m()), aa1(m()), aa2(m()); + aa0 = to_app(a0)->get_arg(0); + aa1 = to_app(a1)->get_arg(0); + aa2 = to_app(a2)->get_arg(0); + if (aa0 == aa1 && aa1 == aa2 && bu.get_bv_size(aa0) == cw) { + result = aa0; + return BR_DONE; + } + } + } + } + + return BR_FAILED; +} + +br_status fpa_rewriter::mk_bvunwrap(expr * arg, expr_ref & result) { + if (is_app_of(arg, m_util.get_family_id(), OP_FPA_INTERNAL_BVWRAP)) + result = to_app(arg)->get_arg(0); + + return BR_FAILED; +} diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 3afc31a9f..f42d7c719 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -89,6 +89,9 @@ public: br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result); + + br_status mk_bvwrap(expr * arg, expr_ref & result); + br_status mk_bvunwrap(expr * arg, expr_ref & result); }; #endif diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 543b1348e..4911af5ec 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -84,6 +84,28 @@ namespace smt { } } + void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result) { + if (m_util.is_float(rng)) { + unsigned ebits = m_util.get_ebits(rng); + unsigned sbits = m_util.get_sbits(rng); + unsigned bv_sz = ebits + sbits; + + app_ref na(m); + na = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); + mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na), + m_bv_util.mk_extract(sbits - 2, 0, na), + result); + } + else if (m_util.is_rm(rng)) { + app_ref na(m); + na = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); + mk_rm(na, result); + } + else + result = m.mk_app(fbv, new_args.size(), new_args.c_ptr()); + } + void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { // TODO: This introduces temporary func_decls that should be filtered in the end. @@ -93,11 +115,13 @@ namespace smt { expr_ref_buffer new_args(m); for (unsigned i = 0; i < num; i++) { + TRACE("t_fpa", tout << "UF arg[" << i << "]: " << mk_ismt2_pp(args[i], m) << std::endl; ); if (is_float(args[i]) || is_rm(args[i])) { expr_ref ai(m), wrapped(m); - ai = args[i]; + ai = args[i]; wrapped = m_th.wrap(ai); new_args.push_back(wrapped); + TRACE("t_fpa", tout << "UF wrap ai: " << mk_ismt2_pp(ai, m) << " --> " << mk_ismt2_pp(wrapped, m) << std::endl; ); m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai)); } else @@ -105,8 +129,10 @@ namespace smt { } func_decl * fd; - if (m_uf2bvuf.find(f, fd)) + if (m_uf2bvuf.find(f, fd)) { + TRACE("t_fpa", tout << "UF reused: " << mk_ismt2_pp(fd, m) << std::endl; ); mk_uninterpreted_output(f->get_range(), fd, new_args, result); + } else { sort_ref_buffer new_domain(m); @@ -372,6 +398,10 @@ namespace smt { res = m.mk_app(w, e); } + + TRACE("t_fpa", tout << "e: " << mk_ismt2_pp(e, m) << "\n"; + tout << "r: " << mk_ismt2_pp(res, m) << "\n";); + return res; } @@ -415,6 +445,9 @@ namespace smt { proof_ref pr(m); m_rw(e, e_conv); + TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << "\n"; + tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << "\n";); + if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { if (!m_fpa_util.is_float(e_conv)) m_th_rw(e_conv, res); @@ -844,7 +877,7 @@ namespace smt { void theory_fpa::init_model(model_generator & mg) { TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout);); m_factory = alloc(fpa_value_factory, get_manager(), get_family_id()); - mg.register_factory(m_factory); + mg.register_factory(m_factory); } model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index d693e3ede..38001b5a6 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -83,6 +83,7 @@ namespace smt { 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); + void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result); virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 627e33a7b..fe9fc2a0f 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -322,50 +322,55 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { sort * rng = f->get_range(); if (arity > 0) { - func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); + func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); - func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); - SASSERT(bv_fi->args_are_values()); + if (bv_fi != 0) { + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); - for (unsigned i = 0; i < bv_fi->num_entries(); i++) { - func_entry const * bv_fe = bv_fi->get_entry(i); - expr * const * bv_args = bv_fe->get_args(); - expr_ref_buffer new_args(m); + for (unsigned i = 0; i < bv_fi->num_entries(); i++) { + func_entry const * bv_fe = bv_fi->get_entry(i); + expr * const * bv_args = bv_fe->get_args(); + expr_ref_buffer new_args(m); - for (unsigned j = 0; j < arity; j++) { - sort * dj = f->get_domain(j); - expr * aj = bv_args[j]; - if (fu.is_float(dj)) - new_args.push_back(convert_bv2fp(bv_mdl, dj, aj)); - else if (fu.is_rm(dj)) { - expr_ref fv(m); - fv = convert_bv2rm(aj); - new_args.push_back(fv); + for (unsigned j = 0; j < arity; j++) { + sort * dj = f->get_domain(j); + expr * aj = bv_args[j]; + expr_ref saj(m); + bv_mdl->eval(aj, saj, true); + + if (fu.is_float(dj)) + new_args.push_back(convert_bv2fp(bv_mdl, dj, saj)); + else if (fu.is_rm(dj)) { + expr_ref fv(m); + fv = convert_bv2rm(saj); + new_args.push_back(fv); + } + else + new_args.push_back(saj); } - else - new_args.push_back(aj); + + expr_ref ret(m); + ret = bv_fe->get_result(); + bv_mdl->eval(ret, ret); + if (fu.is_float(rng)) + ret = convert_bv2fp(bv_mdl, rng, ret); + else if (fu.is_rm(rng)) + ret = convert_bv2rm(ret); + + flt_fi->insert_new_entry(new_args.c_ptr(), ret); } - expr_ref ret(m); - ret = bv_fe->get_result(); + expr_ref els(m); + els = bv_fi->get_else(); if (fu.is_float(rng)) - ret = convert_bv2fp(bv_mdl, rng, ret); + els = convert_bv2fp(bv_mdl, rng, els); else if (fu.is_rm(rng)) - ret = convert_bv2rm(ret); + els = convert_bv2rm(els); - flt_fi->insert_new_entry(new_args.c_ptr(), ret); + flt_fi->set_else(els); + + float_mdl->register_decl(f, flt_fi); } - - expr_ref els(m); - els = bv_fi->get_else(); - if (fu.is_float(rng)) - els = convert_bv2fp(bv_mdl, rng, els); - else if (fu.is_rm(rng)) - els = convert_bv2rm(els); - - flt_fi->set_else(els); - - float_mdl->register_decl(f, flt_fi); } else { func_decl * bvf = it->m_value;