mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
FPA: bugfixes, naming convention, core theory additions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
f11ee40c38
commit
47325c5fd3
|
|
@ -149,7 +149,7 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_inf(c, s, negative);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_minus_inf(to_sort(s)) : ctx->float_util().mk_plus_inf(to_sort(s)));
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_ninf(to_sort(s)) : ctx->float_util().mk_pinf(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -163,6 +163,11 @@ decl_plugin * float_decl_plugin::mk_fresh() {
|
|||
}
|
||||
|
||||
sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
|
||||
if (ebits > sbits)
|
||||
m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported");
|
||||
if (ebits <= 2)
|
||||
m_manager->raise_exception("floating point sorts with ebits <= 2 are currently not supported");
|
||||
|
||||
parameter p1(ebits), p2(sbits);
|
||||
parameter ps[2] = { p1, p2 };
|
||||
sort_size sz;
|
||||
|
|
@ -841,13 +846,13 @@ app * float_util::mk_nan(unsigned ebits, unsigned sbits) {
|
|||
return mk_value(v);
|
||||
}
|
||||
|
||||
app * float_util::mk_plus_inf(unsigned ebits, unsigned sbits) {
|
||||
app * float_util::mk_pinf(unsigned ebits, unsigned sbits) {
|
||||
scoped_mpf v(fm());
|
||||
fm().mk_pinf(ebits, sbits, v);
|
||||
return mk_value(v);
|
||||
}
|
||||
|
||||
app * float_util::mk_minus_inf(unsigned ebits, unsigned sbits) {
|
||||
app * float_util::mk_ninf(unsigned ebits, unsigned sbits) {
|
||||
scoped_mpf v(fm());
|
||||
fm().mk_ninf(ebits, sbits, v);
|
||||
return mk_value(v);
|
||||
|
|
|
|||
|
|
@ -221,11 +221,11 @@ public:
|
|||
app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_ZERO); }
|
||||
|
||||
app * mk_nan(unsigned ebits, unsigned sbits);
|
||||
app * mk_plus_inf(unsigned ebits, unsigned sbits);
|
||||
app * mk_minus_inf(unsigned ebits, unsigned sbits);
|
||||
app * mk_pinf(unsigned ebits, unsigned sbits);
|
||||
app * mk_ninf(unsigned ebits, unsigned sbits);
|
||||
app * mk_nan(sort * s) { return mk_nan(get_ebits(s), get_sbits(s)); }
|
||||
app * mk_plus_inf(sort * s) { return mk_plus_inf(get_ebits(s), get_sbits(s)); }
|
||||
app * mk_minus_inf(sort * s) { return mk_minus_inf(get_ebits(s), get_sbits(s)); }
|
||||
app * mk_pinf(sort * s) { return mk_pinf(get_ebits(s), get_sbits(s)); }
|
||||
app * mk_ninf(sort * s) { return mk_ninf(get_ebits(s), get_sbits(s)); }
|
||||
|
||||
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
|
||||
bool is_value(expr * n) { return m_plugin->is_value(n); }
|
||||
|
|
@ -238,8 +238,8 @@ public:
|
|||
app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
|
||||
|
||||
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nan(v); }
|
||||
bool is_plus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); }
|
||||
bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); }
|
||||
bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); }
|
||||
bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); }
|
||||
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); }
|
||||
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); }
|
||||
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); }
|
||||
|
|
|
|||
|
|
@ -103,9 +103,9 @@ void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args
|
|||
mk_nan(f, result);
|
||||
else if (m_util.fm().is_inf(v)) {
|
||||
if (m_util.fm().sgn(v))
|
||||
mk_minus_inf(f, result);
|
||||
mk_ninf(f, result);
|
||||
else
|
||||
mk_plus_inf(f, result);
|
||||
mk_pinf(f, result);
|
||||
}
|
||||
else {
|
||||
expr_ref bv_sgn(m), bv_sig(m), e(m), biased_exp(m);
|
||||
|
|
@ -298,7 +298,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
|
|||
}
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_plus_inf(func_decl * f, expr_ref & result) {
|
||||
void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) {
|
||||
sort * srt = f->get_range();
|
||||
SASSERT(is_float(srt));
|
||||
unsigned sbits = m_util.get_sbits(srt);
|
||||
|
|
@ -311,7 +311,7 @@ void fpa2bv_converter::mk_plus_inf(func_decl * f, expr_ref & result) {
|
|||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_minus_inf(func_decl * f, expr_ref & result) {
|
||||
void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
|
||||
sort * srt = f->get_range();
|
||||
SASSERT(is_float(srt));
|
||||
unsigned sbits = m_util.get_sbits(srt);
|
||||
|
|
@ -633,8 +633,8 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
|
|||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
|
||||
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
|
||||
|
|
@ -781,8 +781,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
|
|||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
|
||||
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
|
||||
|
|
@ -927,8 +927,8 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
|
|||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
|
||||
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
|
||||
|
|
@ -1137,8 +1137,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
|
||||
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
|
||||
|
|
@ -1447,8 +1447,8 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
|
|||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
|
|
@ -1871,9 +1871,11 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
mk_triple(args[0], args[1], args[2], result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_bv_util.get_bv_size(args[0]) == 3 &&
|
||||
m_bv_util.is_bv(args[1]))
|
||||
{
|
||||
|
||||
mk_to_fp_signed(f, num, args, result);
|
||||
}
|
||||
else if (num == 3 &&
|
||||
|
|
@ -1968,8 +1970,8 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
|
||||
one1 = m_bv_util.mk_numeral(1, 1);
|
||||
expr_ref ninf(m), pinf(m);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_minus_inf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
|
||||
// NaN -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
|
|
@ -2152,38 +2154,146 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
|
||||
// This is meant to be a conversion from signed bitvector to float:
|
||||
|
||||
// This is a conversion from signed bitvector to float:
|
||||
// ; from signed machine integer, represented as a 2's complement bit vector
|
||||
// ((_ to_fp eb sb) RoundingMode(_ BitVec m) (_ FloatingPoint eb sb))
|
||||
|
||||
|
||||
// Semantics:
|
||||
//((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb)):
|
||||
// Semantics:
|
||||
// Let b in[[(_ BitVec m)]] and let n be the signed integer represented by b (in 2's complement format).
|
||||
// [[(_ to_fp eb sb)]](r, b) = +/ -infinity if n is too large / too small to be represented as a finite
|
||||
// number of [[(_ FloatingPoint eb sb)]]; [[(_ to_fp eb sb)]](r, x) = y otherwise, where y is the finite
|
||||
// number such that [[fp.to_real]](y) is closest to n according to rounding mode r.
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
// number such that [[fp.to_real]](y) is closest to n according to rounding mode r.
|
||||
|
||||
SASSERT(num == 2);
|
||||
SASSERT(m_util.is_float(f->get_range()));
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
unsigned sz = sbits + ebits;
|
||||
SASSERT(m_bv_util.get_bv_size(args[0]) == 3);
|
||||
SASSERT(m_bv_util.get_bv_size(args[1]) == sz);
|
||||
SASSERT(m_bv_util.is_bv(args[0]));
|
||||
SASSERT(m_bv_util.is_bv(args[1]));
|
||||
|
||||
expr_ref rm(m), x(m);
|
||||
rm = args[0];
|
||||
x = args[1];
|
||||
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
sgn = m_bv_util.mk_extract(sz - 1, sz - 1, x);
|
||||
sig = m_bv_util.mk_extract(sz - ebits - 2, 0, x);
|
||||
exp = m_bv_util.mk_extract(sz - 2, sz - ebits - 1, x);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_x", x);
|
||||
|
||||
round(f->get_range(), rm, sgn, sig, exp, result);
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
unsigned f_sz = sbits + ebits;
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(x);
|
||||
SASSERT(m_bv_util.get_bv_size(rm) == 3);
|
||||
|
||||
//if (bv_sz < f_sz) {
|
||||
// x = m_bv_util.mk_zero_extend(f_sz - bv_sz, x);
|
||||
// bv_sz = f_sz;
|
||||
//}
|
||||
|
||||
expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m);
|
||||
bv0_1 = m_bv_util.mk_numeral(0, 1);
|
||||
bv1_1 = m_bv_util.mk_numeral(1, 1);
|
||||
bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
|
||||
bv1_sz = m_bv_util.mk_numeral(1, bv_sz);
|
||||
|
||||
expr_ref is_zero(m), nzero(m), pzero(m), ninf(m), pinf(m);
|
||||
is_zero = m.mk_eq(x, bv0_sz);
|
||||
mk_nzero(f, nzero);
|
||||
mk_pzero(f, pzero);
|
||||
mk_ninf(f, ninf);
|
||||
mk_pinf(f, pinf);
|
||||
|
||||
// Special case: x == 0 -> p/n zero
|
||||
expr_ref c1(m), v1(m), rm_is_to_neg(m);
|
||||
c1 = is_zero;
|
||||
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
|
||||
mk_ite(rm_is_to_neg, nzero, pzero, v1);
|
||||
|
||||
// Special case: x != 0
|
||||
expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
|
||||
expr_ref is_neg(m), x_abs(m);
|
||||
is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
|
||||
is_neg = m.mk_eq(is_neg_bit, bv1_1);
|
||||
x_abs = m.mk_ite(is_neg, m_bv_util.mk_bv_neg(x), x);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg);
|
||||
// x_abs has an extra bit in the front.
|
||||
// x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2)
|
||||
// bv_sz-2 is the "1.0" bit for the rounder.
|
||||
|
||||
expr_ref lz(m), e_bv_sz(m), e_rest_sz(m);
|
||||
mk_leading_zeros(x_abs, bv_sz, lz);
|
||||
e_bv_sz = m_bv_util.mk_numeral(bv_sz, bv_sz);
|
||||
e_rest_sz = m_bv_util.mk_bv_sub(e_bv_sz, lz);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == m_bv_util.get_bv_size(e_bv_sz));
|
||||
dbg_decouple("fpa2bv_to_fp_signed_lz", lz);
|
||||
expr_ref shifted_sig(m);
|
||||
shifted_sig = m_bv_util.mk_bv_shl(x_abs, lz);
|
||||
|
||||
expr_ref sticky(m);
|
||||
// shifted_sig is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2) * 2^(-lz)
|
||||
unsigned sig_sz = sbits + 4; // we want extra rounding bits.
|
||||
if (sig_sz <= bv_sz) {
|
||||
expr_ref sig_rest(m);
|
||||
sig_4 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - sig_sz + 1, shifted_sig); // one short
|
||||
sig_rest = m_bv_util.mk_extract(bv_sz - sig_sz, 0, shifted_sig);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest);
|
||||
sig_4 = m_bv_util.mk_concat(sig_4, sticky);
|
||||
}
|
||||
else {
|
||||
unsigned extra_bits = sig_sz - bv_sz;
|
||||
expr_ref extra_zeros(m);
|
||||
extra_zeros = m_bv_util.mk_numeral(0, extra_bits);
|
||||
sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros);
|
||||
lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz),
|
||||
m_bv_util.mk_numeral(extra_bits, sig_sz));
|
||||
bv_sz = bv_sz + extra_bits;
|
||||
SASSERT(is_well_sorted(m, lz));
|
||||
}
|
||||
SASSERT(m_bv_util.get_bv_size(sig_4) == sig_sz);
|
||||
|
||||
expr_ref s_exp(m), exp_rest(m);
|
||||
s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz);
|
||||
// s_exp = (bv_sz-2) + (-lz) signed
|
||||
SASSERT(m_bv_util.get_bv_size(s_exp) == bv_sz);
|
||||
|
||||
unsigned exp_sz = ebits + 2; // (+2 for rounder)
|
||||
exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp);
|
||||
// the remaining bits are 0 if ebits is large enough.
|
||||
exp_too_large = m.mk_false(); // This is always in range.
|
||||
|
||||
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
|
||||
// exp < bv_sz (+sign bit which is [0])
|
||||
unsigned exp_worst_case_sz = (unsigned)((log(bv_sz) / log(2)) + 1);
|
||||
|
||||
if (exp_sz < exp_worst_case_sz) {
|
||||
// exp_sz < exp_worst_case_sz and exp >= 0.
|
||||
// Take the maximum legal exponent; this
|
||||
// allows us to keep the most precision.
|
||||
expr_ref max_exp(m), max_exp_bvsz(m);
|
||||
mk_max_exp(exp_sz, max_exp);
|
||||
max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp);
|
||||
|
||||
exp_too_large = m_bv_util.mk_ule(m_bv_util.mk_bv_add(
|
||||
max_exp_bvsz,
|
||||
m_bv_util.mk_numeral(1, bv_sz)),
|
||||
s_exp);
|
||||
sig_4 = m.mk_ite(exp_too_large, m_bv_util.mk_numeral(0, sig_sz), sig_4);
|
||||
exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2);
|
||||
}
|
||||
dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large);
|
||||
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
sgn = is_neg_bit;
|
||||
sig = sig_4;
|
||||
exp = exp_2;
|
||||
|
||||
dbg_decouple("fpa2bv_to_fp_signed_sgn", sgn);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_exp", exp);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == sbits + 4);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
|
||||
|
||||
expr_ref v2(m);
|
||||
round(f->get_range(), rm, sgn, sig, exp, v2);
|
||||
|
||||
mk_ite(c1, v1, v2, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
@ -2538,7 +2648,7 @@ void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) {
|
|||
|
||||
void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
|
||||
unsigned ebits = m_bv_util.get_bv_size(e);
|
||||
SASSERT(ebits >= 3);
|
||||
SASSERT(ebits >= 2);
|
||||
|
||||
expr_ref e_plus_one(m);
|
||||
e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits));
|
||||
|
|
|
|||
|
|
@ -86,8 +86,8 @@ public:
|
|||
void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_var(unsigned base_inx, sort * srt, expr_ref & result);
|
||||
|
||||
void mk_plus_inf(func_decl * f, expr_ref & result);
|
||||
void mk_minus_inf(func_decl * f, expr_ref & result);
|
||||
void mk_pinf(func_decl * f, expr_ref & result);
|
||||
void mk_ninf(func_decl * f, expr_ref & result);
|
||||
void mk_nan(func_decl * f, expr_ref & result);
|
||||
void mk_nzero(func_decl *f, expr_ref & result);
|
||||
void mk_pzero(func_decl *f, expr_ref & result);
|
||||
|
|
|
|||
|
|
@ -113,8 +113,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
case OP_FLOAT_RM_TOWARD_POSITIVE:
|
||||
case OP_FLOAT_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
|
||||
case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
|
||||
case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
|
||||
case OP_FLOAT_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
|
||||
case OP_FLOAT_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
|
||||
case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
|
||||
case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
|
||||
case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
|
||||
|
|
|
|||
|
|
@ -205,14 +205,14 @@ br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) {
|
|||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_plus_inf(arg1)) {
|
||||
if (m_util.is_pinf(arg1)) {
|
||||
// - +oo --> -oo
|
||||
result = m_util.mk_minus_inf(m().get_sort(arg1));
|
||||
result = m_util.mk_ninf(m().get_sort(arg1));
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_minus_inf(arg1)) {
|
||||
if (m_util.is_ninf(arg1)) {
|
||||
// - -oo -> +oo
|
||||
result = m_util.mk_plus_inf(m().get_sort(arg1));
|
||||
result = m_util.mk_pinf(m().get_sort(arg1));
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_neg(arg1)) {
|
||||
|
|
@ -366,22 +366,22 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_minus_inf(arg1)) {
|
||||
if (m_util.is_ninf(arg1)) {
|
||||
// -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN)
|
||||
result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
if (m_util.is_minus_inf(arg2)) {
|
||||
if (m_util.is_ninf(arg2)) {
|
||||
// arg1 < -oo --> false
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_plus_inf(arg1)) {
|
||||
if (m_util.is_pinf(arg1)) {
|
||||
// +oo < arg2 --> false
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_plus_inf(arg2)) {
|
||||
if (m_util.is_pinf(arg2)) {
|
||||
// arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
|
||||
result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
|
||||
return BR_REWRITE3;
|
||||
|
|
|
|||
|
|
@ -1492,11 +1492,11 @@ namespace nlarith {
|
|||
}
|
||||
fml = mk_and(equivs.size(), equivs.c_ptr());
|
||||
}
|
||||
void mk_plus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) {
|
||||
void mk_pinf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) {
|
||||
plus_inf_subst sub(*this);
|
||||
mk_inf_sign(sub, literals, fml, new_atoms);
|
||||
}
|
||||
void mk_minus_inf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) {
|
||||
void mk_ninf_sign(util::literal_set const& literals, app_ref& fml, app_ref_vector& new_atoms) {
|
||||
minus_inf_subst sub(*this);
|
||||
mk_inf_sign(sub, literals, fml, new_atoms);
|
||||
}
|
||||
|
|
@ -1704,10 +1704,10 @@ namespace nlarith {
|
|||
app_ref fml(m());
|
||||
app_ref_vector new_atoms(m());
|
||||
if (is_pos) {
|
||||
mk_plus_inf_sign(literals, fml, new_atoms);
|
||||
mk_pinf_sign(literals, fml, new_atoms);
|
||||
}
|
||||
else {
|
||||
mk_minus_inf_sign(literals, fml, new_atoms);
|
||||
mk_ninf_sign(literals, fml, new_atoms);
|
||||
}
|
||||
simple_branch* br = alloc(simple_branch, m(), fml);
|
||||
swap_atoms(br, literals.lits(), new_atoms);
|
||||
|
|
|
|||
|
|
@ -49,6 +49,24 @@ namespace smt {
|
|||
{
|
||||
}
|
||||
|
||||
void theory_fpa::add_extra_assertions()
|
||||
{
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
simplifier & simp = ctx.get_simplifier();
|
||||
|
||||
expr_ref_vector::iterator it = m_converter.extra_assertions.begin();
|
||||
expr_ref_vector::iterator end = m_converter.extra_assertions.end();
|
||||
for (; it != end; it++) {
|
||||
expr_ref t(m);
|
||||
proof_ref t_pr(m);
|
||||
simp(*it, t, t_pr);
|
||||
TRACE("t_fpa", tout << "extra: " << mk_ismt2_pp(t, m) << "\n";);
|
||||
ctx.internalize_assertion(t, t_pr, 0);
|
||||
}
|
||||
m_converter.extra_assertions.reset();
|
||||
}
|
||||
|
||||
void theory_fpa::mk_bv_eq(expr * x, expr * y) {
|
||||
SASSERT(get_sort(x)->get_family_id() == m_converter.bu().get_family_id());
|
||||
SASSERT(get_sort(y)->get_family_id() == m_converter.bu().get_family_id());
|
||||
|
|
@ -94,6 +112,8 @@ namespace smt {
|
|||
ctx.mk_th_axiom(get_id(), ~l, def);
|
||||
}
|
||||
|
||||
add_extra_assertions();
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -134,7 +154,7 @@ namespace smt {
|
|||
simp(a->get_arg(1), sig, pr_sig);
|
||||
simp(a->get_arg(2), exp, pr_exp);
|
||||
|
||||
m_converter.mk_triple(sgn, sig, exp, bv_term);
|
||||
m_converter.mk_triple(sgn, sig, exp, bv_term);
|
||||
}
|
||||
else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV ||
|
||||
term->get_decl_kind() == OP_FLOAT_TO_REAL) {
|
||||
|
|
@ -149,7 +169,9 @@ namespace smt {
|
|||
TRACE("t_fpa", tout << "converted: " << mk_ismt2_pp(bv_term, get_manager()) << "\n";);
|
||||
|
||||
SASSERT(!m_trans_map.contains(term));
|
||||
m_trans_map.insert(term, bv_term, 0);
|
||||
m_trans_map.insert(term, bv_term, 0);
|
||||
|
||||
add_extra_assertions();
|
||||
|
||||
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true);
|
||||
theory_var v = mk_var(e);
|
||||
|
|
@ -176,11 +198,15 @@ namespace smt {
|
|||
m_rw(owner, converted);
|
||||
simp(converted, converted, pr);
|
||||
m_trans_map.insert(owner, converted, 0);
|
||||
|
||||
add_extra_assertions();
|
||||
|
||||
sort * owner_sort = m.get_sort(owner);
|
||||
if (m_converter.is_rm(owner_sort)) {
|
||||
bv_util & bu = m_converter.bu();
|
||||
bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted)));
|
||||
expr_ref t(m);
|
||||
t = bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted)));
|
||||
ctx.internalize_assertion(t, proof_ref(m), 0);
|
||||
}
|
||||
|
||||
TRACE("t_fpa", tout << "new theory var (const): " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";);
|
||||
|
|
@ -191,7 +217,8 @@ namespace smt {
|
|||
TRACE("t_fpa", tout << "new eq: " << x << " = " << y << "\n";);
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
|
||||
float_util & fu = m_converter.fu();
|
||||
|
||||
app * ax = get_enode(x)->get_owner();
|
||||
app * ay = get_enode(y)->get_owner();
|
||||
expr * ex, *ey;
|
||||
|
|
@ -199,7 +226,7 @@ namespace smt {
|
|||
m_trans_map.get(ax, ex, px);
|
||||
m_trans_map.get(ay, ey, py);
|
||||
|
||||
if (m_converter.fu().is_float(get_enode(x)->get_owner())) {
|
||||
if (fu.is_float(get_enode(x)->get_owner())) {
|
||||
expr * sgn_x, *sig_x, *exp_x;
|
||||
expr * sgn_y, *sig_y, *exp_y;
|
||||
split_triple(ex, sgn_x, sig_x, exp_x);
|
||||
|
|
@ -209,7 +236,7 @@ namespace smt {
|
|||
mk_bv_eq(sig_x, sig_y);
|
||||
mk_bv_eq(exp_x, exp_y);
|
||||
}
|
||||
else if (m_converter.fu().is_rm(get_enode(x)->get_owner())) {
|
||||
else if (fu.is_rm(get_enode(x)->get_owner())) {
|
||||
mk_bv_eq(ex, ey);
|
||||
}
|
||||
else
|
||||
|
|
@ -220,7 +247,8 @@ namespace smt {
|
|||
TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << "\n";);
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
|
||||
float_util & fu = m_converter.fu();
|
||||
|
||||
app * ax = get_enode(x)->get_owner();
|
||||
app * ay = get_enode(y)->get_owner();
|
||||
expr * ex, *ey;
|
||||
|
|
@ -230,7 +258,7 @@ namespace smt {
|
|||
|
||||
expr_ref deq(m);
|
||||
|
||||
if (m_converter.fu().is_float(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
if (fu.is_float(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
expr * sgn_x, *sig_x, *exp_x;
|
||||
expr * sgn_y, *sig_y, *exp_y;
|
||||
split_triple(ex, sgn_x, sig_x, exp_x);
|
||||
|
|
@ -240,7 +268,7 @@ namespace smt {
|
|||
m.mk_not(m.mk_eq(sig_x, sig_y)),
|
||||
m.mk_not(m.mk_eq(exp_x, exp_y)));
|
||||
}
|
||||
else if (m_converter.fu().is_rm(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
else if (fu.is_rm(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
deq = m.mk_not(m.mk_eq(ex, ey));
|
||||
}
|
||||
else
|
||||
|
|
@ -317,67 +345,65 @@ namespace smt {
|
|||
split_triple(bv_e, bv_sgn, bv_sig, bv_exp);
|
||||
|
||||
family_id fid = m.get_family_id("bv");
|
||||
theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid);
|
||||
theory_bv * bv_th = (theory_bv*)ctx.get_theory(fid);
|
||||
|
||||
app * e_sgn, *e_sig, *e_exp;
|
||||
unsigned exp_sz = fpa_e_srt->get_parameter(0).get_int();
|
||||
unsigned ebits = fpa_e_srt->get_parameter(0).get_int();
|
||||
unsigned sbits = fpa_e_srt->get_parameter(1).get_int();
|
||||
unsigned sig_sz = fpa_e_srt->get_parameter(1).get_int() - 1;
|
||||
|
||||
rational bias = mpfm.m_powers2.m1(ebits - 1);
|
||||
rational sgn_r(0), sig_r(0), exp_r(bias);
|
||||
|
||||
e_sgn = (ctx.e_internalized(bv_sgn)) ? ctx.get_enode(bv_sgn)->get_owner() :
|
||||
m_converter.bu().mk_numeral(0, 1);
|
||||
bu.mk_numeral(0, 1);
|
||||
e_sig = (ctx.e_internalized(bv_sig)) ? ctx.get_enode(bv_sig)->get_owner() :
|
||||
m_converter.bu().mk_numeral(0, sig_sz);
|
||||
bu.mk_numeral(0, sig_sz);
|
||||
e_exp = (ctx.e_internalized(bv_exp)) ? ctx.get_enode(bv_exp)->get_owner() :
|
||||
m_converter.bu().mk_numeral(0, exp_sz);
|
||||
bu.mk_numeral(bias, ebits);
|
||||
|
||||
TRACE("t_fpa", tout << "bv rep: ["
|
||||
<< mk_ismt2_pp(e_sgn, m) << "\n"
|
||||
<< mk_ismt2_pp(e_sig, m) << "\n"
|
||||
<< mk_ismt2_pp(e_exp, m) << "]\n";);
|
||||
|
||||
rational sgn_r(0), sig_r(0), exp_r(0);
|
||||
<< mk_ismt2_pp(e_exp, m) << "]\n";);
|
||||
|
||||
if (ctx.e_internalized(bv_sgn) && ctx.get_enode(bv_sgn)->get_num_th_vars() > 0)
|
||||
bv_th->get_fixed_value(e_sgn, sgn_r); // OK to fail
|
||||
if (ctx.e_internalized(bv_sig) && ctx.get_enode(bv_sig)->get_num_th_vars() > 0)
|
||||
bv_th->get_fixed_value(e_sig, sig_r); // OK to fail
|
||||
if (ctx.e_internalized(bv_exp) && ctx.get_enode(bv_exp)->get_num_th_vars() > 0)
|
||||
bv_th->get_fixed_value(e_exp, exp_r); // OK to fail
|
||||
|
||||
TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " "
|
||||
<< sig_r.to_string() << " "
|
||||
<< exp_r.to_string() << "]\n";);
|
||||
if (!ctx.e_internalized(bv_sgn) ||
|
||||
ctx.get_enode(bv_sgn)->get_num_th_vars() == 0 ||
|
||||
!bv_th->get_fixed_value(e_sgn, sgn_r))
|
||||
sgn_r = rational(0);
|
||||
if (!ctx.e_internalized(bv_sig) ||
|
||||
ctx.get_enode(bv_sig)->get_num_th_vars() == 0 ||
|
||||
!bv_th->get_fixed_value(e_sig, sig_r))
|
||||
sig_r = rational(0);
|
||||
if (!ctx.e_internalized(bv_exp) ||
|
||||
ctx.get_enode(bv_exp)->get_num_th_vars() == 0 ||
|
||||
!bv_th->get_fixed_value(e_exp, exp_r))
|
||||
exp_r = bias;
|
||||
|
||||
// un-bias exponent
|
||||
rational exp_unbiased_r;
|
||||
exp_unbiased_r = exp_r - mpfm.m_powers2.m1(exp_sz - 1);
|
||||
exp_unbiased_r = exp_r - bias;
|
||||
|
||||
mpz sig_z; mpf_exp_t exp_z;
|
||||
mpq sig_q, exp_q;
|
||||
mpz sig_num, exp_num;
|
||||
TRACE("t_fpa", tout << "bv model: [" << sgn_r.to_string() << " "
|
||||
<< sig_r.to_string() << " "
|
||||
<< exp_unbiased_r.to_string() << "(" << exp_r.to_string() << ")]\n"; );
|
||||
|
||||
scoped_mpz sig_z(mpzm);
|
||||
mpf_exp_t exp_z;
|
||||
scoped_mpq sig_q(mpqm), exp_q(mpqm);
|
||||
scoped_mpz sig_num(mpzm), exp_num(mpzm);
|
||||
mpqm.set(sig_q, sig_r.to_mpq());
|
||||
mpzm.set(sig_num, sig_q.numerator());
|
||||
mpzm.set(sig_num, sig_q.get().numerator());
|
||||
mpqm.set(exp_q, exp_unbiased_r.to_mpq());
|
||||
mpzm.set(exp_num, exp_q.numerator());
|
||||
mpzm.set(exp_num, exp_q.get().numerator());
|
||||
mpzm.set(sig_z, sig_num);
|
||||
exp_z = mpzm.get_int64(exp_num);
|
||||
|
||||
mpf fp_val;
|
||||
mpfm.set(fp_val, exp_sz, sig_sz + 1, !sgn_r.is_zero(), sig_z, exp_z);
|
||||
scoped_mpf fp_val(mpfm);
|
||||
mpfm.set(fp_val, ebits, sbits, !sgn_r.is_zero(), sig_z, exp_z);
|
||||
|
||||
app * fp_val_e;
|
||||
fp_val_e = fu.mk_value(fp_val);
|
||||
|
||||
TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mk_ismt2_pp(fp_val_e, m) << std::endl;);
|
||||
|
||||
mpfm.del(fp_val);
|
||||
mpzm.del(sig_num);
|
||||
mpzm.del(exp_num);
|
||||
mpqm.del(sig_q);
|
||||
mpqm.del(exp_q);
|
||||
mpzm.del(sig_z);
|
||||
|
||||
res = alloc(expr_wrapper_proc, fp_val_e);
|
||||
TRACE("t_fpa", tout << mk_ismt2_pp(fpa_e, m) << " := " << mpfm.to_string(fp_val) << std::endl;);
|
||||
res = alloc(expr_wrapper_proc, m_factory->mk_value(fp_val));
|
||||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
|
@ -445,7 +471,7 @@ namespace smt {
|
|||
|
||||
void theory_fpa::reset_eh() {
|
||||
pop_scope_eh(m_trail_stack.get_num_scopes());
|
||||
m_rw.reset();
|
||||
m_rw.reset();
|
||||
m_trans_map.reset();
|
||||
m_bool_var2atom.reset();
|
||||
m_temporaries.reset();
|
||||
|
|
@ -453,6 +479,8 @@ namespace smt {
|
|||
theory::reset_eh();
|
||||
}
|
||||
|
||||
void theory_fpa::init_model(model_generator & m) {
|
||||
void theory_fpa::init_model(model_generator & m) {
|
||||
m_factory = alloc(fpa_factory, get_manager(), get_family_id());
|
||||
m.register_factory(m_factory);
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -23,9 +23,38 @@ Revision History:
|
|||
#include"trail.h"
|
||||
#include"fpa2bv_converter.h"
|
||||
#include"fpa2bv_rewriter.h"
|
||||
#include"value_factory.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class fpa_factory : public value_factory {
|
||||
float_util m_util;
|
||||
|
||||
virtual app * mk_value_core(mpf const & val, sort * s) {
|
||||
SASSERT(m_util.get_ebits(s) == val.get_ebits());
|
||||
SASSERT(m_util.get_sbits(s) == val.get_sbits());
|
||||
return m_util.mk_value(val);
|
||||
}
|
||||
|
||||
public:
|
||||
fpa_factory(ast_manager & m, family_id fid) :
|
||||
value_factory(m, fid),
|
||||
m_util(m) {
|
||||
}
|
||||
|
||||
virtual ~fpa_factory() {}
|
||||
|
||||
virtual expr * get_some_value(sort * s) { NOT_IMPLEMENTED_YET(); }
|
||||
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { NOT_IMPLEMENTED_YET(); }
|
||||
virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); }
|
||||
virtual void register_value(expr * n) { /* Ignore */ }
|
||||
|
||||
app * mk_value(mpf const & x) {
|
||||
return m_util.mk_value(x);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
class theory_fpa : public theory {
|
||||
class th_trail_stack : public trail_stack<theory_fpa> {
|
||||
public:
|
||||
|
|
@ -60,6 +89,7 @@ namespace smt {
|
|||
bool_var2atom m_bool_var2atom;
|
||||
enode_vector m_temporaries;
|
||||
int_vector m_tvars;
|
||||
fpa_factory * m_factory;
|
||||
|
||||
virtual final_check_status final_check_eh() { return FC_DONE; }
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
|
|
@ -78,7 +108,6 @@ namespace smt {
|
|||
void assign_eh(bool_var v, bool is_true);
|
||||
virtual void relevant_eh(app * n);
|
||||
virtual void init_model(model_generator & m);
|
||||
|
||||
public:
|
||||
theory_fpa(ast_manager& m);
|
||||
virtual ~theory_fpa();
|
||||
|
|
@ -91,7 +120,8 @@ namespace smt {
|
|||
sig = to_app(e)->get_arg(1);
|
||||
exp = to_app(e)->get_arg(2);
|
||||
}
|
||||
|
||||
|
||||
void add_extra_assertions();
|
||||
void mk_bv_eq(expr * x, expr * y);
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue