From f11ee40c38928d84e54ca5fcee404a8cc619f6aa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 14 Dec 2014 19:09:17 +0000 Subject: [PATCH] FPA: bug and leak fixes Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 75 ++++++++++++++++++++++++----- src/ast/float_decl_plugin.h | 2 +- src/ast/fpa/fpa2bv_converter.cpp | 50 +++++++++++++++++++ src/ast/fpa/fpa2bv_converter.h | 8 +-- src/ast/rewriter/float_rewriter.cpp | 19 ++++++-- src/ast/rewriter/float_rewriter.h | 1 + src/smt/theory_fpa.cpp | 11 +++-- 7 files changed, 142 insertions(+), 24 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 1ae8a2a2c..625ed9ade 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -457,22 +457,47 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa sort * fp = mk_float_sort(ebits, sbits); symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } - else { - // 1 Real -> 1 FP - if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) - m_manager->raise_exception("expecting two integer parameters to to_fp"); - if (arity != 2 && arity != 3) - m_manager->raise_exception("invalid number of arguments to to_fp operator"); - if (arity == 3 && domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch, expected third argument of Int sort"); - if (domain[1] != m_real_sort) - m_manager->raise_exception("sort mismatch, expected second argument of Real sort"); - + } + else if (arity == 3 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_arith_fid, REAL_SORT) && + is_sort_of(domain[2], m_arith_fid, INT_SORT)) + { + // Rounding + 1 Real + 1 Int -> 1 FP + if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) + m_manager->raise_exception("expecting two integer parameters to to_fp"); + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } + else if (arity == 1 && + is_sort_of(domain[0], m_arith_fid, REAL_SORT)) + { + // 1 Real -> 1 FP + if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) + m_manager->raise_exception("expecting two integer parameters to to_fp"); + if (domain[1] != m_real_sort) + m_manager->raise_exception("sort mismatch, expected one argument of Real sort"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } + else if (arity == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_arith_fid, REAL_SORT)) + { + // Rounding + 1 Real -> 1 FP + if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) + m_manager->raise_exception("expecting two integer parameters to to_fp"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } + else + NOT_IMPLEMENTED_YET(); } func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -759,6 +784,32 @@ bool float_decl_plugin::is_value(app * e) const { } } +bool float_decl_plugin::is_unique_value(app* e) const { + if (e->get_family_id() != m_family_id) + return false; + switch (e->get_decl_kind()) { + case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: + case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: + case OP_FLOAT_RM_TOWARD_POSITIVE: + case OP_FLOAT_RM_TOWARD_NEGATIVE: + case OP_FLOAT_RM_TOWARD_ZERO: + return true; + case OP_FLOAT_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */ + case OP_FLOAT_MINUS_INF: /* Nol -oo == fp #b1 #b11 #b00) */ + case OP_FLOAT_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ + case OP_FLOAT_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ + case OP_FLOAT_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ + case OP_FLOAT_VALUE: /* above */ + return false; + case OP_FLOAT_FP: + return m_manager->is_unique_value(e->get_arg(0)) && + m_manager->is_unique_value(e->get_arg(1)) && + m_manager->is_unique_value(e->get_arg(2)); + default: + return false; + } +} + float_util::float_util(ast_manager & m): m_manager(m), m_fid(m.mk_family_id("float")), diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index dbd3dda2e..bd180c45c 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -170,7 +170,7 @@ public: virtual void get_sort_names(svector & sort_names, symbol const & logic); virtual expr * get_some_value(sort * s); virtual bool is_value(app* e) const; - virtual bool is_unique_value(app* e) const { return is_value(e); } + virtual bool is_unique_value(app* e) const; mpf_manager & fm() { return m_fm; } func_decl * mk_value_decl(mpf const & v); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 5fd96eace..afad59dff 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1870,6 +1870,12 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 2 && + m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[1])) + { + mk_to_fp_signed(f, num, args, result); + } else if (num == 3 && m_bv_util.is_bv(args[0]) && m_arith_util.is_numeral(args[1]) && @@ -2143,6 +2149,50 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args SASSERT(is_well_sorted(m, result)); } +void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); + + // This is meant to be a conversion from signed bitvector to float: + // ; from signed machine integer, represented as a 2's complement bit vector + // ((_ to_fp eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb)) + + + // Semantics: + //((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)): + // Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format). + // [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite + // number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite + // number such that [[fp.to_real]](y) is closest to n according to rounding mode r. + + NOT_IMPLEMENTED_YET(); + + SASSERT(m_util.is_float(f->get_range())); + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned sz = sbits + ebits; + SASSERT(m_bv_util.get_bv_size(args[0]) == 3); + SASSERT(m_bv_util.get_bv_size(args[1]) == sz); + + expr_ref rm(m), x(m); + rm = args[0]; + x = args[1]; + + expr_ref sgn(m), sig(m), exp(m); + sgn = m_bv_util.mk_extract(sz - 1, sz - 1, x); + sig = m_bv_util.mk_extract(sz - ebits - 2, 0, x); + exp = m_bv_util.mk_extract(sz - 2, sz - ebits - 1, x); + + round(f->get_range(), rm, sgn, sig, exp, result); +} + +void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_fp_unsigned", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); + + NOT_IMPLEMENTED_YET(); +} + void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr * sgn, * s, * e; diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index caad0875c..e83754e38 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -121,11 +121,13 @@ public: void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 42a4e5660..583268c34 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -37,6 +37,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c SASSERT(f->get_family_id() == get_fid()); switch (f->get_decl_kind()) { case OP_FLOAT_TO_FP: st = mk_to_fp(f, num_args, args, result); break; + case OP_FLOAT_TO_FP_UNSIGNED: st = mk_to_fp_unsigned(f, num_args, args, result); break; case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break; case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break; case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break; @@ -86,10 +87,10 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons return BR_FAILED; rational q; - mpf q_mpf; + scoped_mpf q_mpf(m_util.fm()); if (m_util.au().is_numeral(args[1], q)) { TRACE("fp_rewriter", tout << "q: " << q << std::endl; ); - mpf v; + scoped_mpf v(m_util.fm()); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); result = m_util.mk_value(v); m_util.fm().del(v); @@ -98,7 +99,7 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons } else if (m_util.is_value(args[1], q_mpf)) { TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); - mpf v; + scoped_mpf v(m_util.fm()); m_util.fm().set(v, ebits, sbits, rm, q_mpf); result = m_util.mk_value(v); m_util.fm().del(v); @@ -126,7 +127,7 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons return BR_FAILED; TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";); - mpf v; + scoped_mpf v(m_util.fm()); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); result = m_util.mk_value(v); m_util.fm().del(v); @@ -137,6 +138,16 @@ br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * cons } } +br_status float_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(1).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + + return BR_FAILED; +} + br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_value(arg1, rm)) { diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 4d8cec856..31c571f32 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -75,6 +75,7 @@ public: br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 3c6b18349..26ee88226 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -336,10 +336,13 @@ namespace smt { << mk_ismt2_pp(e_exp, m) << "]\n";); rational sgn_r(0), sig_r(0), exp_r(0); - - bv_th->get_fixed_value(e_sgn, sgn_r); // OK to fail - bv_th->get_fixed_value(e_sig, sig_r); // OK to fail - bv_th->get_fixed_value(e_exp, exp_r); // OK to fail + + 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); // OK to fail + 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); // OK to fail + 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); // OK to fail TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " " << sig_r.to_string() << " "