mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
added internal functions to fpa2bv converter
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
4d18e24fb4
commit
01d78b7274
|
@ -2422,29 +2422,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
split_triple(args[0], sgn, s, e);
|
||||
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
|
||||
}
|
||||
void fpa2bv_converter::mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_internal", tout << "wrap ";
|
||||
for (unsigned i = 0; i < num; i++)
|
||||
tout << " " << mk_ismt2_pp(args[i], m);
|
||||
tout << std::endl;);
|
||||
SASSERT(num == 1);
|
||||
result = m.mk_app(f, num, args);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_internal", tout << "unwrap ";
|
||||
for (unsigned i = 0; i < num; i++)
|
||||
tout << " " << mk_ismt2_pp(args[i], m);
|
||||
tout << std::endl;);
|
||||
SASSERT(num == 1);
|
||||
app * a0 = to_app(args[0]);
|
||||
SASSERT(a0->get_kind() == AST_APP);
|
||||
SASSERT(is_float_family(a0->get_decl()));
|
||||
decl_kind k = a0->get_decl_kind();
|
||||
SASSERT(k == OP_FLOAT_INTERNAL_BVWRAP);
|
||||
SASSERT(a0->get_num_args() == 1);
|
||||
result = a0->get_arg(0);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 3);
|
||||
|
@ -2631,7 +2608,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
// sig is of the form [1].[sigbits]
|
||||
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
|
||||
|
@ -2646,8 +2623,8 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
for (unsigned i = sbits-2; i != (unsigned)-1; i--)
|
||||
{
|
||||
bit = m_bv_util.mk_extract(i, i, sig);
|
||||
rsig = m_arith_util.mk_mul(rsig, two);
|
||||
rsig = m_arith_util.mk_add(rsig, m.mk_ite(m.mk_eq(bit, bv1), one, zero));
|
||||
rsig = m_arith_util.mk_add(m_arith_util.mk_mul(rsig, two),
|
||||
m.mk_ite(m.mk_eq(bit, bv1), one, zero));
|
||||
}
|
||||
|
||||
const mpz & p2 = fu().fm().m_powers2(sbits-1);
|
||||
|
@ -2661,19 +2638,18 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1);
|
||||
dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg);
|
||||
exp_p = m_bv_util.mk_sign_extend(1, exp);
|
||||
exp_n = m_bv_util.mk_bv_not(m_bv_util.mk_sign_extend(1, exp));
|
||||
exp_n = m_bv_util.mk_bv_neg(exp_p);
|
||||
exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p);
|
||||
dbg_decouple("fpa2bv_to_real_exp_abs", exp);
|
||||
SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1);
|
||||
|
||||
expr_ref exp2(m), prev_bit(m);
|
||||
exp2 = zero;
|
||||
prev_bit = bv0;
|
||||
for (unsigned i = ebits; i != (unsigned)-1; i--)
|
||||
{
|
||||
bit = m_bv_util.mk_extract(i, i, exp_abs);
|
||||
exp2 = m_arith_util.mk_mul(exp2, two);
|
||||
exp2 = m_arith_util.mk_add(exp2, m.mk_ite(m.mk_eq(bit, prev_bit), zero, one));
|
||||
exp2 = m_arith_util.mk_add(m_arith_util.mk_mul(exp2, two),
|
||||
m.mk_ite(m.mk_eq(bit, bv1), one, zero));
|
||||
prev_bit = bit;
|
||||
}
|
||||
|
||||
|
|
|
@ -147,13 +147,6 @@ public:
|
|||
void dbg_decouple(const char * prefix, expr_ref & e);
|
||||
expr_ref_vector m_extra_assertions;
|
||||
|
||||
void mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void mk_internal_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_internal_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_internal_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
protected:
|
||||
void mk_is_nan(expr * e, expr_ref & result);
|
||||
void mk_is_inf(expr * e, expr_ref & result);
|
||||
|
|
|
@ -151,8 +151,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_INTERNAL_BVWRAP: m_conv.mk_internal_bvwrap(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_INTERNAL_BVUNWRAP: m_conv.mk_internal_bvunwrap(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_INTERNAL_BVWRAP:
|
||||
case OP_FLOAT_INTERNAL_BVUNWRAP:
|
||||
case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED:
|
||||
case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
|
||||
default:
|
||||
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
|
||||
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
|
||||
|
|
Loading…
Reference in a new issue