mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

More FPA exponent/siginficand order consistency

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-05 18:05:21 +00:00
parent 1610e4fbd0
commit de3cb7e5dc
6 changed files with 246 additions and 218 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
examples/c/test_capi.c
View file

@ -2758,17 +2758,17 @@ void fpa_example() {
Z3_solver_push(ctx, s);
c1 = Z3_mk_fpa_fp(ctx,
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)),
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)));
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)));
c2 = Z3_mk_fpa_to_fp_bv(ctx,
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
Z3_mk_fpa_sort(ctx, 11, 53));
c3 = Z3_mk_fpa_to_fp_int_real(ctx,
c3 = Z3_mk_fpa_to_fp_int_real(ctx,
Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */
Z3_mk_fpa_sort(ctx, 11, 53));
c4 = Z3_mk_fpa_to_fp_real(ctx,
c4 = Z3_mk_fpa_to_fp_real(ctx,
Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
Z3_mk_fpa_sort(ctx, 11, 53));

2
src/api/api_fpa.cpp
View file

@ -1077,8 +1077,8 @@ extern "C" {
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!fu.is_rm(to_expr(rm)) ||
!ctx->autil().is_real(to_expr(sig)) ||
!ctx->autil().is_int(to_expr(exp)) ||
!ctx->autil().is_real(to_expr(sig)) ||
!fu.is_float(to_sort(s))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;

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

@ -2490,12 +2490,12 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr * bv_rm = to_app(args[0])->get_arg(0);
rational q;
if (!m_arith_util.is_numeral(args[1], q))
rational e;
if (!m_arith_util.is_numeral(args[1], e))
UNREACHABLE();
rational e;
if (!m_arith_util.is_numeral(args[2], e))
rational q;
if (!m_arith_util.is_numeral(args[2], q))
UNREACHABLE();
SASSERT(e.is_int64());

22
src/ast/fpa_decl_plugin.cpp
View file

@ -490,11 +490,24 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (arity == 3 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
is_sort_of(domain[2], m_arith_fid, INT_SORT))
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_arith_fid, REAL_SORT) &&
is_sort_of(domain[2], m_arith_fid, INT_SORT))
{
// Rounding + 1 Real + 1 Int -> 1 FP
// Rounding + 1 Real + 1 Int -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (arity == 3 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_arith_fid, INT_SORT) &&
is_sort_of(domain[2], m_arith_fid, REAL_SORT))
{
// Rounding + 1 Int + 1 Real -> 1 FP
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to to_fp");
@ -545,6 +558,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
"(Real), "
"(RoundingMode (_ BitVec (eb+sb))), "
"(RoundingMode (_ FloatingPoint eb' sb')), "
"(RoundingMode Int Real), "
"(RoundingMode Real Int), "
"(RoundingMode Int), and "
"(RoundingMode Real)."

4
src/ast/fpa_decl_plugin.h
View file

@ -286,9 +286,9 @@ public:
expr * args[] = { rm, t };
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 2, args);
}
app * mk_to_fp(sort * s, expr * rm, expr * sig, expr * exp) {
app * mk_to_fp(sort * s, expr * rm, expr * exp, expr * sig) {
SASSERT(is_float(s) && s->get_num_parameters() == 2);
expr * args[] = { rm, sig, exp };
expr * args[] = { rm, exp, sig};
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 3, args);
}
app * mk_to_fp_unsigned(sort * s, expr * rm, expr * t) {

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

@ -271,6 +271,20 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
result = m_util.mk_value(v);
return BR_DONE;
}
else if (m_util.is_rm_numeral(args[0], rmv) &&
m_util.au().is_int(args[1]) &&
m_util.au().is_real(args[2])) {
// rm + int + real -> float
if (!m_util.is_rm_numeral(args[0], rmv) ||
!m_util.au().is_numeral(args[1], r1) ||
!m_util.au().is_numeral(args[2], r2))
return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq().numerator(), r2.to_mpq());
result = m_util.mk_value(v);
return BR_DONE;
}
else if (bu.is_numeral(args[0], r1, bvs1) &&
bu.is_numeral(args[1], r2, bvs2) &&
bu.is_numeral(args[2], r3, bvs3)) {