mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

to_fp_real marked as NIY for now

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-08 17:23:13 +00:00
parent 7fe9ad5cb4
commit cad841cff4
1 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2064,7 +2064,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
if (false && m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) {
if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) {
rational tmp_rat; unsigned sz;
m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz);
SASSERT(tmp_rat.is_int32());
@ -2096,6 +2096,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_triple(sgn, s, e, result);
}
else {
NOT_IMPLEMENTED_YET();
mpf_manager & fm = fu().fm();
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2135,16 +2137,16 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
//dbg_decouple("fpa2bv_to_float_real_inc", inc);
//sig = m.mk_ite(inc, bu.mk_bv_add(sig, bv1_s4), sig);
SASSERT(bu.get_bv_size(sgn) == 1);
SASSERT(bu.get_bv_size(sig) == sbits + 4);
SASSERT(bu.get_bv_size(exp) == ebits + 2);
//SASSERT(bu.get_bv_size(sgn) == 1);
//SASSERT(bu.get_bv_size(sig) == sbits + 4);
//SASSERT(bu.get_bv_size(exp) == ebits + 2);
dbg_decouple("fpa2bv_to_float_real_sgn", sgn);
dbg_decouple("fpa2bv_to_float_real_sig", sig);
dbg_decouple("fpa2bv_to_float_real_exp", exp);
//dbg_decouple("fpa2bv_to_float_real_sgn", sgn);
//dbg_decouple("fpa2bv_to_float_real_sig", sig);
//dbg_decouple("fpa2bv_to_float_real_exp", exp);
expr_ref rmr(rm, m);
round(s, rmr, sgn, sig, exp, result);
//expr_ref rmr(rm, m);
//round(s, rmr, sgn, sig, exp, result);
}
SASSERT(is_well_sorted(m, result));