From c377fec7a4153b6b5fffc2267cb55aef83451506 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 20 May 2015 17:57:27 +0100 Subject: [PATCH 1/3] Made fp.* comparison chainable. --- src/ast/fpa_decl_plugin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index e559ee179..0b28c4277 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -289,7 +289,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (arity != 2) + if (arity < 2) m_manager->raise_exception("invalid number of arguments to floating point relation"); if (domain[0] != domain[1] || !is_float_sort(domain[0])) m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments"); @@ -306,7 +306,7 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter } func_decl_info finfo(m_family_id, k); finfo.set_chainable(true); - return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo); + return m_manager->mk_func_decl(name, domain[0], domain[1], m_manager->mk_bool_sort(), finfo); } func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, From 1e3952406c4b217dad6f40c17bc54a82ebb66f93 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 20 May 2015 18:14:38 +0100 Subject: [PATCH 2/3] disabled debug output --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ed3a66515..6d07092ea 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3351,7 +3351,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG - // return; + return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); From 51040d3e19dae7046225405c27a6ef977167d4f5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 20 May 2015 18:32:40 +0100 Subject: [PATCH 3/3] Bugfix for fp.isNormal --- src/ast/fpa/fpa2bv_converter.cpp | 4 +++- src/util/mpf.cpp | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6d07092ea..83ba843ac 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3132,14 +3132,16 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split_fp(e, sgn, exp, sig); - expr_ref is_special(m), is_denormal(m), p(m); + expr_ref is_special(m), is_denormal(m), p(m), is_zero(m); mk_is_denormal(e, is_denormal); + mk_is_zero(e, is_zero); unsigned ebits = m_bv_util.get_bv_size(exp); p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits); m_simp.mk_eq(exp, p, is_special); expr_ref or_ex(m); m_simp.mk_or(is_special, is_denormal, or_ex); + m_simp.mk_or(is_zero, or_ex, or_ex); m_simp.mk_not(or_ex, result); } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 683140129..1dab7b995 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1428,7 +1428,7 @@ bool mpf_manager::is_ninf(mpf const & x) { } bool mpf_manager::is_normal(mpf const & x) { - return !(has_top_exp(x) || is_denormal(x)); + return !(has_top_exp(x) || is_denormal(x) || is_zero(x)); } bool mpf_manager::is_denormal(mpf const & x) {