mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

FPA updates and bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-18 13:42:28 +01:00
parent 4610acca0f
commit 7af410e6d6
10 changed files with 308 additions and 188 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_fpa.cpp
View file

@ -121,6 +121,16 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative) {
Z3_TRY;
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_nzero(to_sort(s)) : ctx->float_util().mk_pzero(to_sort(s)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_double(Z3_context c, double v, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_fpa_double(c, v, ty);
@ -361,7 +371,7 @@ extern "C" {
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(ctx->float_util().mk_to_ieee_bv(to_expr(t)));
Z3_ast r = of_ast(ctx->float_util().mk_float_to_ieee_bv(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}

33
src/api/z3_fpa.h
View file

@ -109,12 +109,25 @@ extern "C" {
\param s target sort
\param negative indicates whether the result should be negative
When \c negative is true, -Inf will be generated instead of +Inf.
When \c negative is true, -oo will be generated instead of +oo.
def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
*/
Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
/**
\brief Create a floating point zero of sort s.
\param c logical context.
\param s target sort
\param negative indicates whether the result should be negative
When \c negative is true, -zero will be generated instead of +zero.
def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
*/
Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
/**
\brief Create a numeral of floating point sort.
@ -133,6 +146,24 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty);
/**
\brief Create a numeral of floating point sort.
This function can be use to create numerals that fit in a double value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\params c logical context.
\params v value.
\params ty sort.
ty must be a floating point sort
\sa Z3_mk_numeral
def_API('Z3_mk_fpa_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_fpa_double(__in Z3_context c, __in double v, __in Z3_sort ty);
/**
\brief Floating-point absolute value

326
src/ast/float_decl_plugin.cpp
View file

@ -40,11 +40,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin.
m_manager->inc_ref(m_int_sort);
if (m_manager->has_plugin(symbol("bv"))) {
// bv plugin is optional, so m_bv_plugin may be 0
m_bv_fid = m_manager->mk_family_id("bv");
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
// BV is not optional anymore.
SASSERT(m_manager->has_plugin(symbol("bv")));
m_bv_fid = m_manager->mk_family_id("bv");
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
float_decl_plugin::~float_decl_plugin() {
@ -103,6 +102,18 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
m_fm.mk_nan(ebits, sbits, val);
return true;
}
else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) {
unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
m_fm.mk_pzero(ebits, sbits, val);
return true;
}
else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_ZERO)) {
unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
m_fm.mk_nzero(ebits, sbits, val);
return true;
}
return false;
}
@ -156,7 +167,7 @@ sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
parameter ps[2] = { p1, p2 };
sort_size sz;
sz = sort_size::mk_very_big(); // TODO: refine
return m_manager->mk_sort(symbol("FP"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
}
sort * float_decl_plugin::mk_rm_sort() {
@ -176,6 +187,14 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
case ROUNDING_MODE_SORT:
return mk_rm_sort();
case FLOAT16_SORT:
return mk_float_sort(5, 11);
case FLOAT32_SORT:
return mk_float_sort(8, 24);
case FLOAT64_SORT:
return mk_float_sort(11, 53);
case FLOAT128_SORT:
return mk_float_sort(15, 133);
default:
m_manager->raise_exception("unknown floating point theory sort");
return 0;
@ -229,17 +248,18 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
unsigned ebits = s->get_parameter(0).get_int();
unsigned sbits = s->get_parameter(1).get_int();
scoped_mpf val(m_fm);
if (k == OP_FLOAT_NAN) {
m_fm.mk_nan(ebits, sbits, val);
switch (k)
{
case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val);
SASSERT(m_fm.is_nan(val));
break;
case OP_FLOAT_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break;
case OP_FLOAT_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break;
case OP_FLOAT_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break;
case OP_FLOAT_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break;
}
else if (k == OP_FLOAT_MINUS_INF) {
m_fm.mk_ninf(ebits, sbits, val);
}
else {
SASSERT(k == OP_FLOAT_PLUS_INF);
m_fm.mk_pinf(ebits, sbits, val);
}
return mk_value_decl(val);
}
@ -251,11 +271,11 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_EQ: name = "=="; break;
case OP_FLOAT_LT: name = "<"; break;
case OP_FLOAT_GT: name = ">"; break;
case OP_FLOAT_LE: name = "<="; break;
case OP_FLOAT_GE: name = ">="; break;
case OP_FLOAT_EQ: name = "fp.eq"; break;
case OP_FLOAT_LT: name = "fp.lt"; break;
case OP_FLOAT_GT: name = "fp.gt"; break;
case OP_FLOAT_LE: name = "fp.lte"; break;
case OP_FLOAT_GE: name = "fp.gte"; break;
default:
UNREACHABLE();
break;
@ -273,14 +293,15 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_IS_ZERO: name = "isZero"; break;
case OP_FLOAT_IS_NZERO: name = "isNZero"; break;
case OP_FLOAT_IS_PZERO: name = "isPZero"; break;
case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break;
case OP_FLOAT_IS_NAN: name = "isNaN"; break;
case OP_FLOAT_IS_INF: name = "isInfinite"; break;
case OP_FLOAT_IS_NORMAL: name = "isNormal"; break;
case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break;
case OP_FLOAT_IS_ZERO: name = "fp.isZero"; break;
case OP_FLOAT_IS_NZERO: name = "fp.isNZero"; break;
case OP_FLOAT_IS_PZERO: name = "fp.isPZero"; break;
case OP_FLOAT_IS_NEGATIVE: name = "fp.isNegative"; break;
case OP_FLOAT_IS_POSITIVE: name = "fp.isPositive"; break;
case OP_FLOAT_IS_NAN: name = "fp.isNaN"; break;
case OP_FLOAT_IS_INF: name = "fp.isInfinite"; break;
case OP_FLOAT_IS_NORMAL: name = "fp.isNormal"; break;
case OP_FLOAT_IS_SUBNORMAL: name = "fp.isSubnormal"; break;
default:
UNREACHABLE();
break;
@ -296,8 +317,8 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_ABS: name = "abs"; break;
case OP_FLOAT_UMINUS: name = "-"; break;
case OP_FLOAT_ABS: name = "fp.abs"; break;
case OP_FLOAT_NEG: name = "fp.neg"; break;
default:
UNREACHABLE();
break;
@ -313,9 +334,9 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_REM: name = "remainder"; break;
case OP_FLOAT_MIN: name = "min"; break;
case OP_FLOAT_MAX: name = "max"; break;
case OP_FLOAT_REM: name = "fp.rem"; break;
case OP_FLOAT_MIN: name = "fp.min"; break;
case OP_FLOAT_MAX: name = "fp.max"; break;
default:
UNREACHABLE();
break;
@ -331,10 +352,10 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_ADD: name = "+"; break;
case OP_FLOAT_SUB: name = "-"; break;
case OP_FLOAT_MUL: name = "*"; break;
case OP_FLOAT_DIV: name = "/"; break;
case OP_FLOAT_ADD: name = "fp.add"; break;
case OP_FLOAT_SUB: name = "fp.sub"; break;
case OP_FLOAT_MUL: name = "fp.mul"; break;
case OP_FLOAT_DIV: name = "fp.div"; break;
default:
UNREACHABLE();
break;
@ -350,8 +371,8 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
m_manager->raise_exception("sort mismatch");
symbol name;
switch (k) {
case OP_FLOAT_SQRT: name = "squareRoot"; break;
case OP_FLOAT_ROUND_TO_INTEGRAL: name = "roundToIntegral"; break;
case OP_FLOAT_SQRT: name = "fp.sqrt"; break;
case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral"; break;
default:
UNREACHABLE();
break;
@ -359,13 +380,13 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
}
func_decl * float_decl_plugin::mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 4)
m_manager->raise_exception("invalid number of arguments to fused_ma operator");
if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1]))
m_manager->raise_exception("sort mismatch");
symbol name("fusedMA");
symbol name("fp.fma");
return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
}
@ -375,12 +396,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
is_sort_of(domain[0], m_bv_fid, BV_SORT) &&
is_sort_of(domain[1], m_bv_fid, BV_SORT) &&
is_sort_of(domain[2], m_bv_fid, BV_SORT)) {
// When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float!
// 3 BVs -> 1 FP
sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
symbol name("asFloat");
symbol name("fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
// 1 BV -> 1 FP
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to to_fp");
if (!parameters[0].is_int() || !parameters[1].is_int())
@ -389,28 +411,56 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
int sbits = parameters[1].get_int();
sort * fp = mk_float_sort(ebits, sbits);
symbol name("asFloat");
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 {
// .. Otherwise we only know how to convert rationals/reals.
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
m_manager->raise_exception("expecting two integer parameters to asFloat");
if (arity != 2 && arity != 3)
m_manager->raise_exception("invalid number of arguments to asFloat operator");
if (arity == 3 && domain[2] != m_int_sort)
m_manager->raise_exception("sort mismatch");
else if (m_bv_plugin && arity == 2 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_bv_fid, BV_SORT)) {
// Rounding + 1 BV -> 1 FP
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to to_fp");
if (!parameters[0].is_int() || !parameters[1].is_int())
m_manager->raise_exception("invalid parameter type to to_fp");
int ebits = parameters[0].get_int();
int sbits = parameters[1].get_int();
sort * fp = mk_float_sort(ebits, sbits);
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 == 2 &&
is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
is_sort_of(domain[1], m_family_id, FLOAT_SORT)) {
// Rounding + 1 FP -> 1 FP
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to to_fp");
if (!parameters[0].is_int() || !parameters[1].is_int())
m_manager->raise_exception("invalid parameter type to to_fp");
int ebits = parameters[0].get_int();
int sbits = parameters[1].get_int();
if (!is_rm_sort(domain[0]) ||
!(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT)))
!is_sort_of(domain[1], m_family_id, FLOAT_SORT))
m_manager->raise_exception("sort mismatch");
}
else {
// 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");
if (arity != 2 && arity != 3)
m_manager->raise_exception("invalid number of arguments to to_fp operator");
if (arity == 3 && domain[2] != m_int_sort)
m_manager->raise_exception("sort mismatch");
if (domain[1] != m_real_sort)
m_manager->raise_exception("sort mismatch");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("asFloat");
symbol name("to_fp");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
}
}
func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (!m_bv_plugin)
m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support");
@ -443,7 +493,7 @@ func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters,
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
}
func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (!m_bv_plugin)
m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support");
@ -455,15 +505,10 @@ func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_param
m_manager->raise_exception("sort mismtach");
sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
symbol name("to_fp_unsigned");
symbol name("fp.t_ubv");
return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
}
func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
NOT_IMPLEMENTED_YET();
}
func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
NOT_IMPLEMENTED_YET();
@ -498,14 +543,15 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_FLOAT_IS_ZERO:
case OP_FLOAT_IS_NZERO:
case OP_FLOAT_IS_PZERO:
case OP_FLOAT_IS_SIGN_MINUS:
case OP_FLOAT_IS_NEGATIVE:
case OP_FLOAT_IS_POSITIVE:
case OP_FLOAT_IS_NAN:
case OP_FLOAT_IS_INF:
case OP_FLOAT_IS_NORMAL:
case OP_FLOAT_IS_SUBNORMAL:
return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_ABS:
case OP_FLOAT_UMINUS:
case OP_FLOAT_NEG:
return mk_unary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_REM:
case OP_FLOAT_MIN:
@ -517,20 +563,18 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_SUB:
if (arity == 1)
return mk_unary_decl(OP_FLOAT_UMINUS, num_parameters, parameters, arity, domain, range);
return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range);
else
return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_SQRT:
case OP_FLOAT_ROUND_TO_INTEGRAL:
return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_FUSED_MA:
return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
case OP_TO_IEEE_BV:
return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_FMA:
return mk_fma(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_IEEE_BV:
return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_FP:
return mk_from3bv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_FP_UNSIGNED:
return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_UBV:
return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_TO_SBV:
@ -544,8 +588,11 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
}
void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF));
op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF));
// These are the operators from the final draft of the SMT FloatingPoint standard
op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
op_names.push_back(builtin_name("+zero", OP_FLOAT_PLUS_ZERO));
op_names.push_back(builtin_name("-zero", OP_FLOAT_MINUS_ZERO));
op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN));
op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN));
@ -553,22 +600,66 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("roundTowardPositive", OP_RM_TOWARD_POSITIVE));
op_names.push_back(builtin_name("roundTowardNegative", OP_RM_TOWARD_NEGATIVE));
op_names.push_back(builtin_name("roundTowardZero", OP_RM_TOWARD_ZERO));
op_names.push_back(builtin_name("+", OP_FLOAT_ADD));
op_names.push_back(builtin_name("-", OP_FLOAT_SUB));
op_names.push_back(builtin_name("/", OP_FLOAT_DIV));
op_names.push_back(builtin_name("*", OP_FLOAT_MUL));
op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("remainder", OP_FLOAT_REM));
op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA));
op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE));
op_names.push_back(builtin_name("RTN", OP_RM_TOWARD_NEGATIVE));
op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO));
op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG));
op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD));
op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB));
op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL));
op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV));
op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FMA));
op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM));
op_names.push_back(builtin_name("fp.roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE));
op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT));
op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE));
op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT));
op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO));
op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF));
op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
op_names.push_back(builtin_name("fp.isNegative", OP_FLOAT_IS_NEGATIVE));
op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE));
op_names.push_back(builtin_name("to_fp", OP_FLOAT_FP));
if (m_bv_plugin) {
op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
}
// We also support the names of operators in older drafts.
op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF));
op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF));
op_names.push_back(builtin_name("+", OP_FLOAT_ADD));
op_names.push_back(builtin_name("-", OP_FLOAT_SUB));
op_names.push_back(builtin_name("/", OP_FLOAT_DIV));
op_names.push_back(builtin_name("*", OP_FLOAT_MUL));
op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("remainder", OP_FLOAT_REM));
op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FMA));
op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
op_names.push_back(builtin_name("==", OP_FLOAT_EQ));
op_names.push_back(builtin_name("<", OP_FLOAT_LT));
op_names.push_back(builtin_name(">", OP_FLOAT_GT));
op_names.push_back(builtin_name("<", OP_FLOAT_LT));
op_names.push_back(builtin_name(">", OP_FLOAT_GT));
op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
@ -579,65 +670,30 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_NEGATIVE));
op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
// Disabled min/max, clashes with user-defined min/max functions
// op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
// op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
if (m_bv_plugin)
op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
// These are the operators from the final draft of the SMT FloatingPoints standard
op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE));
op_names.push_back(builtin_name("RTN", OP_RM_TOWARD_NEGATIVE));
op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO));
op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS));
op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD));
op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB));
op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL));
op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV));
op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA));
op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM));
op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE));
op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT));
op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE));
op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT));
op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO));
op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF));
op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));
if (m_bv_plugin) {
op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
}
// op_names.push_back(builtin_name("fp.toReal", ?));
if (m_bv_plugin)
op_names.push_back(builtin_name("asIEEEBV", OP_FLOAT_TO_IEEE_BV));
}
void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
// Old draft sort names.
sort_names.push_back(builtin_name("FP", FLOAT_SORT));
sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
// In the SMT FPA final draft, FP is called FloatingPoint
// In the final draft, FP is called FloatingPoint ...
sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
// ... and it supports three common FloatingPoint sorts
sort_names.push_back(builtin_name("Float16", FLOAT16_SORT));
sort_names.push_back(builtin_name("Float32", FLOAT32_SORT));
sort_names.push_back(builtin_name("Float64", FLOAT64_SORT));
sort_names.push_back(builtin_name("Float128", FLOAT128_SORT));
}
expr * float_decl_plugin::get_some_value(sort * s) {
@ -661,6 +717,8 @@ bool float_decl_plugin::is_value(app * e) const {
case OP_FLOAT_VALUE:
case OP_FLOAT_PLUS_INF:
case OP_FLOAT_MINUS_INF:
case OP_FLOAT_PLUS_ZERO:
case OP_FLOAT_MINUS_ZERO:
case OP_FLOAT_NAN:
return true;
case OP_TO_FLOAT:

42
src/ast/float_decl_plugin.h
View file

@ -27,7 +27,11 @@ Revision History:
enum float_sort_kind {
FLOAT_SORT,
ROUNDING_MODE_SORT
ROUNDING_MODE_SORT,
FLOAT16_SORT,
FLOAT32_SORT,
FLOAT64_SORT,
FLOAT128_SORT
};
enum float_op_kind {
@ -37,22 +41,23 @@ enum float_op_kind {
OP_RM_TOWARD_NEGATIVE,
OP_RM_TOWARD_ZERO,
OP_FLOAT_VALUE,
OP_FLOAT_PLUS_INF,
OP_FLOAT_MINUS_INF,
OP_FLOAT_NAN,
OP_FLOAT_PLUS_ZERO,
OP_FLOAT_MINUS_ZERO,
OP_FLOAT_ADD,
OP_FLOAT_SUB,
OP_FLOAT_UMINUS,
OP_FLOAT_NEG,
OP_FLOAT_MUL,
OP_FLOAT_DIV,
OP_FLOAT_REM,
OP_FLOAT_ABS,
OP_FLOAT_MIN,
OP_FLOAT_MAX,
OP_FLOAT_FUSED_MA, // x*y + z
OP_FLOAT_FMA, // x*y + z
OP_FLOAT_SQRT,
OP_FLOAT_ROUND_TO_INTEGRAL,
@ -68,13 +73,14 @@ enum float_op_kind {
OP_FLOAT_IS_SUBNORMAL,
OP_FLOAT_IS_PZERO,
OP_FLOAT_IS_NZERO,
OP_FLOAT_IS_SIGN_MINUS,
OP_FLOAT_IS_NEGATIVE,
OP_FLOAT_IS_POSITIVE,
OP_TO_FLOAT,
OP_TO_IEEE_BV,
OP_FLOAT_TO_IEEE_BV,
OP_FLOAT_FP,
OP_FLOAT_TO_FP_UNSIGNED,
OP_FLOAT_TO_FP,
OP_FLOAT_TO_UBV,
OP_FLOAT_TO_SBV,
OP_FLOAT_TO_REAL,
@ -125,16 +131,14 @@ class float_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -243,7 +247,7 @@ public:
app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); }
app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_UMINUS, arg1); }
app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_NEG, arg1); }
app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); }
app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); }
app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); }
@ -252,7 +256,7 @@ public:
app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); }
app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
expr * args[4] = { arg1, arg2, arg3, arg4 };
return m().mk_app(m_fid, OP_FLOAT_FUSED_MA, 4, args);
return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args);
}
app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); }
@ -268,11 +272,13 @@ public:
app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }
app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_POSITIVE, arg1); }
app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); }
bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); }
app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); }
app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); }
};
#endif

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

@ -1844,11 +1844,19 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
mk_is_denormal(args[0], result);
}
void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_neg(args[0], result);
}
void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr_ref t1(m), t2(m);
mk_is_nan(args[0], t1);
mk_is_pos(args[0], t2);
result = m.mk_and(m.mk_not(t1), t2);
}
void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; );
@ -2141,10 +2149,6 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
mk_triple(args[0], args[2], args[1], result);
}
void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
NOT_IMPLEMENTED_YET();
}
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
NOT_IMPLEMENTED_YET();
}

3
src/ast/fpa/fpa2bv_converter.h
View file

@ -114,7 +114,8 @@ public:
void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

14
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -115,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
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_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;
case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
case OP_FLOAT_NEG: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
case OP_FLOAT_FMA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
@ -140,11 +142,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(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_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
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;

37
src/ast/rewriter/float_rewriter.cpp
View file

@ -36,17 +36,17 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
br_status st = BR_FAILED;
SASSERT(f->get_family_id() == get_fid());
switch (f->get_decl_kind()) {
case OP_TO_FLOAT: st = mk_to_float(f, num_args, args, result); break;
case OP_TO_FLOAT: st = mk_to_fp(f, num_args, args, result); break;
case OP_FLOAT_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
case OP_FLOAT_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
case OP_FLOAT_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
case OP_FLOAT_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
case OP_FLOAT_MUL: SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break;
case OP_FLOAT_DIV: SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break;
case OP_FLOAT_REM: SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break;
case OP_FLOAT_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
case OP_FLOAT_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
case OP_FLOAT_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
case OP_FLOAT_FUSED_MA: SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break;
case OP_FLOAT_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
case OP_FLOAT_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
@ -62,10 +62,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break;
case OP_FLOAT_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
case OP_FLOAT_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
case OP_FLOAT_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break;
case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break;
case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
@ -73,7 +73,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
return st;
}
br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
@ -188,7 +188,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref
return BR_FAILED;
}
br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) {
if (m_util.is_nan(arg1)) {
// -nan --> nan
result = arg1;
@ -284,7 +284,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
return BR_REWRITE_FULL;
}
br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_value(arg1, rm)) {
scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
@ -480,7 +480,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
scoped_mpf v(m_util.fm());
if (m_util.is_value(arg1, v)) {
result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false();
@ -490,6 +490,17 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
scoped_mpf v(m_util.fm());
if (m_util.is_value(arg1, v)) {
result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true();
return BR_DONE;
}
return BR_FAILED;
}
// This the SMT =
br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_util.fm()), v2(m_util.fm());
@ -532,10 +543,6 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref
return BR_FAILED;
}
br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) {
return BR_FAILED;
}
br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) {
return BR_FAILED;
}

11
src/ast/rewriter/float_rewriter.h
View file

@ -44,18 +44,17 @@ public:
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_uminus(expr * arg1, expr_ref & result);
br_status mk_neg(expr * arg1, expr_ref & result);
br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_abs(expr * arg1, expr_ref & result);
br_status mk_min(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
@ -70,10 +69,12 @@ public:
br_status mk_is_inf(expr * arg1, expr_ref & result);
br_status mk_is_normal(expr * arg1, expr_ref & result);
br_status mk_is_subnormal(expr * arg1, expr_ref & result);
br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
br_status mk_is_negative(expr * arg1, expr_ref & result);
br_status mk_is_positive(expr * arg1, expr_ref & result);
br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);

4
src/smt/theory_fpa.cpp
View file

@ -132,7 +132,7 @@ namespace smt {
m_converter.mk_triple(sgn, sig, exp, bv_term);
}
else if (term->get_decl_kind() == OP_TO_IEEE_BV) {
else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) {
SASSERT(is_app(t));
expr_ref bv_e(m);
proof_ref bv_pr(m);
@ -424,7 +424,7 @@ namespace smt {
ctx.mark_as_relevant(bv_sig);
ctx.mark_as_relevant(bv_exp);
}
else if (n->get_decl()->get_decl_kind() == OP_TO_IEEE_BV) {
else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) {
expr_ref eq(m);
app * ex_a = to_app(ex);
if (n->get_id() > ex_a->get_id())