mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
FPA theory support for conversion functions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
621be0f47f
commit
05121e25d4
|
@ -655,6 +655,45 @@ func_decl * float_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_p
|
|||
return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * float_decl_plugin::mk_internal_to_ubv_unspecified(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified");
|
||||
if (num_parameters != 1)
|
||||
m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1");
|
||||
if (!parameters[0].is_int())
|
||||
m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer");
|
||||
|
||||
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
|
||||
return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * float_decl_plugin::mk_internal_to_sbv_unspecified(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
m_manager->raise_exception("invalid number of arguments to internal_to_sbv_unspecified");
|
||||
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT))
|
||||
m_manager->raise_exception("sort mismatch, expected argument of bitvector sort");
|
||||
if (!is_sort_of(range, m_bv_fid, BV_SORT))
|
||||
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
|
||||
|
||||
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
|
||||
return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * float_decl_plugin::mk_internal_to_real_unspecified(
|
||||
decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 0)
|
||||
m_manager->raise_exception("invalid number of arguments to internal_to_real_unspecified");
|
||||
if (!is_sort_of(range, m_arith_fid, REAL_SORT))
|
||||
m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort");
|
||||
|
||||
return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
|
||||
func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
|
@ -726,6 +765,12 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
|
|||
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_INTERNAL_BVUNWRAP:
|
||||
return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED:
|
||||
return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED:
|
||||
return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range);
|
||||
default:
|
||||
m_manager->raise_exception("unsupported floating point operator");
|
||||
return 0;
|
||||
|
@ -864,7 +909,8 @@ bool float_decl_plugin::is_unique_value(app* e) const {
|
|||
float_util::float_util(ast_manager & m):
|
||||
m_manager(m),
|
||||
m_fid(m.mk_family_id("float")),
|
||||
m_a_util(m) {
|
||||
m_a_util(m),
|
||||
m_bv_util(m) {
|
||||
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m_fid));
|
||||
}
|
||||
|
||||
|
@ -916,3 +962,19 @@ app * float_util::mk_nzero(unsigned ebits, unsigned sbits) {
|
|||
return mk_value(v);
|
||||
}
|
||||
|
||||
app * float_util::mk_internal_to_ubv_unspecified(unsigned width) {
|
||||
parameter ps[] = { parameter(width) };
|
||||
sort * range = m_bv_util.mk_sort(width);
|
||||
return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range);
|
||||
}
|
||||
|
||||
app * float_util::mk_internal_to_sbv_unspecified(unsigned width) {
|
||||
parameter ps[] = { parameter(width) };
|
||||
sort * range = m_bv_util.mk_sort(width);
|
||||
return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range);
|
||||
}
|
||||
|
||||
app * float_util::mk_internal_to_real_unspecified() {
|
||||
sort * range = m_a_util.mk_real();
|
||||
return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range);
|
||||
}
|
|
@ -47,7 +47,7 @@ enum float_op_kind {
|
|||
OP_FLOAT_NAN,
|
||||
OP_FLOAT_PLUS_ZERO,
|
||||
OP_FLOAT_MINUS_ZERO,
|
||||
|
||||
|
||||
OP_FLOAT_ADD,
|
||||
OP_FLOAT_SUB,
|
||||
OP_FLOAT_NEG,
|
||||
|
@ -70,7 +70,7 @@ enum float_op_kind {
|
|||
OP_FLOAT_IS_INF,
|
||||
OP_FLOAT_IS_ZERO,
|
||||
OP_FLOAT_IS_NORMAL,
|
||||
OP_FLOAT_IS_SUBNORMAL,
|
||||
OP_FLOAT_IS_SUBNORMAL,
|
||||
OP_FLOAT_IS_PZERO,
|
||||
OP_FLOAT_IS_NZERO,
|
||||
OP_FLOAT_IS_NEGATIVE,
|
||||
|
@ -85,10 +85,13 @@ enum float_op_kind {
|
|||
|
||||
/* Extensions */
|
||||
OP_FLOAT_TO_IEEE_BV,
|
||||
|
||||
|
||||
/* Internal use only */
|
||||
OP_FLOAT_INTERNAL_BVWRAP,
|
||||
OP_FLOAT_INTERNAL_BVUNWRAP,
|
||||
OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED,
|
||||
OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED,
|
||||
OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED,
|
||||
|
||||
LAST_FLOAT_OP
|
||||
};
|
||||
|
@ -155,9 +158,15 @@ class float_decl_plugin : public decl_plugin {
|
|||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
virtual void set_manager(ast_manager * m, family_id id);
|
||||
unsigned mk_id(mpf const & v);
|
||||
|
@ -203,6 +212,7 @@ class float_util {
|
|||
float_decl_plugin * m_plugin;
|
||||
family_id m_fid;
|
||||
arith_util m_a_util;
|
||||
bv_util m_bv_util;
|
||||
public:
|
||||
float_util(ast_manager & m);
|
||||
~float_util();
|
||||
|
@ -292,6 +302,10 @@ public:
|
|||
bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); }
|
||||
|
||||
app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); }
|
||||
|
||||
app * mk_internal_to_ubv_unspecified(unsigned width);
|
||||
app * mk_internal_to_sbv_unspecified(unsigned width);
|
||||
app * mk_internal_to_real_unspecified();
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -2487,10 +2487,13 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
|
|||
mk_is_neg(x, x_is_neg);
|
||||
mk_is_nzero(x, x_is_nzero);
|
||||
|
||||
expr_ref undef(m);
|
||||
undef = m_util.mk_internal_to_ubv_unspecified(bv_sz);
|
||||
|
||||
// NaN, Inf, or negative (except -0) -> undefined
|
||||
expr_ref c1(m), v1(m);
|
||||
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
|
||||
v1 = mk_fresh_const(0, bv_sz);
|
||||
v1 = undef;
|
||||
dbg_decouple("fpa2bv_to_ubv_c1", c1);
|
||||
|
||||
// +-Zero -> 0
|
||||
|
@ -2546,9 +2549,10 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
|
|||
dbg_decouple("fpa2bv_to_ubv_shifted_sig", shifted_sig);
|
||||
|
||||
expr_ref rounded(m);
|
||||
rounded = shifted_sig; // TODO.
|
||||
// TODO: Rounding.
|
||||
rounded = shifted_sig;
|
||||
|
||||
result = m.mk_ite(c_in_limits, rounded, mk_fresh_const(0, bv_sz));
|
||||
result = m.mk_ite(c_in_limits, rounded, undef);
|
||||
result = m.mk_ite(c2, v2, result);
|
||||
result = m.mk_ite(c1, v1, result);
|
||||
|
||||
|
@ -2658,7 +2662,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
|
||||
|
||||
expr_ref undef(m);
|
||||
undef = m.mk_fresh_const(0, rs);
|
||||
undef = m_util.mk_internal_to_real_unspecified();
|
||||
|
||||
result = m.mk_ite(x_is_zero, zero, res);
|
||||
result = m.mk_ite(x_is_inf, undef, result);
|
||||
|
|
|
@ -149,6 +149,10 @@ public:
|
|||
|
||||
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);
|
||||
|
|
|
@ -291,7 +291,7 @@ namespace smt {
|
|||
SASSERT(m_bv_util.get_bv_size(res) == 3);
|
||||
ctx.internalize(res, false);
|
||||
}
|
||||
else {
|
||||
else if (m_float_util.is_float(e)) {
|
||||
SASSERT(to_app(res)->get_family_id() == get_family_id());
|
||||
decl_kind k = to_app(res)->get_decl_kind();
|
||||
if (k == OP_FLOAT_TO_FP) {
|
||||
|
@ -314,6 +314,9 @@ namespace smt {
|
|||
SASSERT(is_sort_of(m.get_sort(res), m_bv_util.get_family_id(), BV_SORT));
|
||||
}
|
||||
}
|
||||
else {
|
||||
/* ignore; these are the conversion functions fp.to_* */
|
||||
}
|
||||
|
||||
TRACE("t_fpa_detail", tout << "converted term:" << std::endl;
|
||||
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
|
||||
|
@ -339,6 +342,8 @@ namespace smt {
|
|||
res = convert_atom(e);
|
||||
else if (m_float_util.is_float(e) || m_float_util.is_rm(e))
|
||||
res = convert_term(e);
|
||||
else if (m_arith_util.is_real(e))
|
||||
res = convert_term(e);
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
|
@ -508,12 +513,10 @@ namespace smt {
|
|||
|
||||
c = m.mk_and(m.mk_eq(x_sgn, y_sgn),
|
||||
m.mk_eq(x_sig, y_sig),
|
||||
m.mk_eq(x_exp, y_exp));
|
||||
m.mk_eq(x_exp, y_exp));
|
||||
}
|
||||
else if (fu.is_rm(xe) && fu.is_rm(ye))
|
||||
c = m.mk_eq(xc, yc);
|
||||
else
|
||||
UNREACHABLE();
|
||||
c = m.mk_eq(xc, yc);
|
||||
|
||||
// assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
|
||||
assert_cnstr(c);
|
||||
|
@ -556,12 +559,10 @@ namespace smt {
|
|||
|
||||
c = m.mk_or(m.mk_not(m.mk_eq(x_sgn, y_sgn)),
|
||||
m.mk_not(m.mk_eq(x_sig, y_sig)),
|
||||
m.mk_not(m.mk_eq(x_exp, y_exp)));
|
||||
m.mk_not(m.mk_eq(x_exp, y_exp)));
|
||||
}
|
||||
else if (m_float_util.is_rm(xe) && m_float_util.is_rm(ye))
|
||||
c = m.mk_not(m.mk_eq(xc, yc));
|
||||
else
|
||||
UNREACHABLE();
|
||||
c = m.mk_not(m.mk_eq(xc, yc));
|
||||
|
||||
// assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
|
||||
assert_cnstr(c);
|
||||
|
@ -638,6 +639,9 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
// These are the conversion functions fp.to_* */
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::reset_eh() {
|
||||
|
|
Loading…
Reference in a new issue