From 4be26eb5430672196df96b0fe0faa25c4bb085ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Aug 2022 04:26:14 -0700 Subject: [PATCH] #6116 handle also nan/oo/0+ as numerals --- src/ast/fpa/fpa2bv_converter.cpp | 35 +++++++++++++++++++++++++++----- 1 file changed, 30 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 862fe6929..8c1ff40cd 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -147,11 +147,36 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_external()); - unsigned p_id = f->get_parameter(0).get_ext_id(); - mpf const & v = m_plugin->get_value(p_id); - mk_numeral(f->get_range(), v, result); + sort* s = f->get_range(); + if (f->get_num_parameters() == 1) { + SASSERT(f->get_parameter(0).is_external()); + unsigned p_id = f->get_parameter(0).get_ext_id(); + mpf const& v = m_plugin->get_value(p_id); + mk_numeral(s, v, result); + return; + } + scoped_mpf v(m_mpf_manager); + unsigned ebits = m_util.get_ebits(s), sbits = m_util.get_sbits(s); + switch (f->get_decl_kind()) { + case OP_FPA_PLUS_INF: + m_util.fm().mk_pinf(ebits, sbits, v); + break; + case OP_FPA_MINUS_INF: + m_util.fm().mk_ninf(ebits, sbits, v); + break; + case OP_FPA_NAN: + m_util.fm().mk_nan(ebits, sbits, v); + break; + case OP_FPA_PLUS_ZERO: + m_util.fm().mk_pzero(ebits, sbits, v); + break; + case OP_FPA_MINUS_ZERO: + m_util.fm().mk_nzero(ebits, sbits, v); + break; + default: + UNREACHABLE(); + } + mk_numeral(s, v, result); } void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {