mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Bugfix for fp.to_ieee_bv.

Browse source 
Fixes #507.
This commit is contained in:
Christoph M. Wintersteiger 2016-03-11 12:35:41 +00:00
parent 9dd53c091a
commit b5279d1da8
2 changed files with 7 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/fpa_decl_plugin.cpp
View file

@ -593,7 +593,7 @@ func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_paramet
}
func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
if (arity != 3)
m_manager->raise_exception("invalid number of arguments to fp");
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
@ -610,7 +610,7 @@ func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, paramet
}
func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
SASSERT(m_bv_plugin);
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to fp.to_ubv");
@ -631,7 +631,7 @@ func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, par
}
func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
SASSERT(m_bv_plugin);
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to fp.to_sbv");
@ -671,9 +671,9 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters,
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
parameter ps[] = { parameter(float_sz) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
sort * bv_srt = m_bv_plugin->mk_sort(BV_SORT, 1, ps);
symbol name("to_ieee_bv");
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k));
}
func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters,

6
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -150,11 +150,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
}
br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned bv_sz = f->get_parameter(0).get_int();
bv_util bu(m());
unsigned bv_sz = bu.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0.
result = bu.mk_numeral(0, bv_sz);