mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
FPA API: Renaming for consistency with final SMT standard.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
3418f1875e
commit
657595818e
|
@ -88,6 +88,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_sort(c, ebits, sbits);
|
||||
|
@ -105,18 +106,34 @@ extern "C" {
|
|||
return Z3_mk_fpa_sort(c, 5, 11);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 5, 11);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 8, 24);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 8, 24);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 11, 53);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 11, 53);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 15, 113);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c) {
|
||||
return Z3_mk_fpa_sort(c, 15, 113);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_nan(c, s);
|
||||
|
@ -373,22 +390,12 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_convert(c, s, rm, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
api::context * ctx = mk_c(c);
|
||||
expr * args [2] = { to_expr(rm), to_expr(t) };
|
||||
Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_TO_FLOAT,
|
||||
Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_FLOAT_TO_FP,
|
||||
to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(),
|
||||
2, args));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t) {
|
||||
Z3_TRY;
|
||||
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_float_to_ieee_bv(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
};
|
||||
|
|
|
@ -117,6 +117,19 @@ extern "C" {
|
|||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the half-precision (16-bit) floating point sort.
|
||||
|
||||
\param c logical context.
|
||||
\param ebits number of exponent bits
|
||||
\param sbits number of significand bits
|
||||
|
||||
\remark ebits must be larger than 1 and sbits must be larger than 2.
|
||||
|
||||
def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the single-precision (32-bit) floating point sort.
|
||||
|
||||
|
@ -130,6 +143,19 @@ extern "C" {
|
|||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the single-precision (32-bit) floating point sort.
|
||||
|
||||
\param c logical context.
|
||||
\param ebits number of exponent bits
|
||||
\param sbits number of significand bits
|
||||
|
||||
\remark ebits must be larger than 1 and sbits must be larger than 2.
|
||||
|
||||
def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the double-precision (64-bit) floating point sort.
|
||||
|
||||
|
@ -143,6 +169,19 @@ extern "C" {
|
|||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the double-precision (64-bit) floating point sort.
|
||||
|
||||
\param c logical context.
|
||||
\param ebits number of exponent bits
|
||||
\param sbits number of significand bits
|
||||
|
||||
\remark ebits must be larger than 1 and sbits must be larger than 2.
|
||||
|
||||
def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort__64(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the quadruple-precision (128-bit) floating point sort.
|
||||
|
||||
|
@ -156,6 +195,18 @@ extern "C" {
|
|||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the quadruple-precision (128-bit) floating point sort.
|
||||
|
||||
\param c logical context.
|
||||
\param ebits number of exponent bits
|
||||
\param sbits number of significand bits
|
||||
|
||||
\remark ebits must be larger than 1 and sbits must be larger than 2.
|
||||
|
||||
def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a NaN of sort s.
|
||||
|
@ -504,18 +555,6 @@ extern "C" {
|
|||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating point term to a bit-vector term in IEEE754 format.
|
||||
|
||||
\param c logical context.
|
||||
\param t floating-point term.
|
||||
|
||||
t must have floating point sort. The size of the resulting bit-vector is automatically determined.
|
||||
|
||||
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
||||
|
|
|
@ -118,23 +118,23 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
|
|||
}
|
||||
|
||||
bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
|
||||
if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
|
||||
if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_AWAY)) {
|
||||
val = MPF_ROUND_NEAREST_TAWAY;
|
||||
return true;
|
||||
}
|
||||
else if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_EVEN)) {
|
||||
else if (is_app_of(n, m_family_id, OP_FLOAT_RM_NEAREST_TIES_TO_EVEN)) {
|
||||
val = MPF_ROUND_NEAREST_TEVEN;
|
||||
return true;
|
||||
}
|
||||
else if (is_app_of(n, m_family_id, OP_RM_TOWARD_NEGATIVE)) {
|
||||
else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_NEGATIVE)) {
|
||||
val = MPF_ROUND_TOWARD_NEGATIVE;
|
||||
return true;
|
||||
}
|
||||
else if (is_app_of(n, m_family_id, OP_RM_TOWARD_POSITIVE)) {
|
||||
else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_POSITIVE)) {
|
||||
val = MPF_ROUND_TOWARD_POSITIVE;
|
||||
return true;
|
||||
}
|
||||
else if (is_app_of(n, m_family_id, OP_RM_TOWARD_ZERO)) {
|
||||
else if (is_app_of(n, m_family_id, OP_FLOAT_RM_TOWARD_ZERO)) {
|
||||
val = MPF_ROUND_TOWARD_ZERO;
|
||||
return true;
|
||||
}
|
||||
|
@ -210,15 +210,15 @@ func_decl * float_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_parame
|
|||
sort * s = mk_rm_sort();
|
||||
func_decl_info finfo(m_family_id, k);
|
||||
switch (k) {
|
||||
case OP_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN:
|
||||
return m_manager->mk_const_decl(symbol("roundNearestTiesToEven"), s, finfo);
|
||||
case OP_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY:
|
||||
return m_manager->mk_const_decl(symbol("roundNearestTiesToAway"), s, finfo);
|
||||
case OP_RM_TOWARD_POSITIVE:
|
||||
case OP_FLOAT_RM_TOWARD_POSITIVE:
|
||||
return m_manager->mk_const_decl(symbol("roundTowardPositive"), s, finfo);
|
||||
case OP_RM_TOWARD_NEGATIVE:
|
||||
case OP_FLOAT_RM_TOWARD_NEGATIVE:
|
||||
return m_manager->mk_const_decl(symbol("roundTowardNegative"), s, finfo);
|
||||
case OP_RM_TOWARD_ZERO:
|
||||
case OP_FLOAT_RM_TOWARD_ZERO:
|
||||
return m_manager->mk_const_decl(symbol("roundTowardZero"), s, finfo);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
@ -471,20 +471,6 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_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 (arity != 1)
|
||||
m_manager->raise_exception("invalid number of arguments to asIEEEBV");
|
||||
if (!is_float_sort(domain[0]))
|
||||
m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
|
||||
|
||||
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
|
||||
parameter ps[] = { parameter(float_sz) };
|
||||
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
|
||||
symbol name("asIEEEBV");
|
||||
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
if (arity != 3)
|
||||
|
@ -528,17 +514,19 @@ func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_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) {
|
||||
switch (k) {
|
||||
case OP_TO_FLOAT:
|
||||
case OP_FLOAT_TO_FP:
|
||||
return mk_to_float(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_MINUS_INF:
|
||||
case OP_FLOAT_PLUS_INF:
|
||||
case OP_FLOAT_NAN:
|
||||
case OP_FLOAT_MINUS_ZERO:
|
||||
case OP_FLOAT_PLUS_ZERO:
|
||||
return mk_float_const_decl(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_RM_TOWARD_POSITIVE:
|
||||
case OP_RM_TOWARD_NEGATIVE:
|
||||
case OP_RM_TOWARD_ZERO:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_FLOAT_RM_TOWARD_POSITIVE:
|
||||
case OP_FLOAT_RM_TOWARD_NEGATIVE:
|
||||
case OP_FLOAT_RM_TOWARD_ZERO:
|
||||
return mk_rm_const_decl(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FLOAT_EQ:
|
||||
case OP_FLOAT_LT:
|
||||
|
@ -577,8 +565,6 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
|
|||
return mk_rm_unary_decl(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_UBV:
|
||||
|
@ -601,17 +587,17 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
|
|||
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));
|
||||
op_names.push_back(builtin_name("roundNearestTiesToAway", OP_RM_NEAREST_TIES_TO_AWAY));
|
||||
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("roundNearestTiesToEven", OP_FLOAT_RM_NEAREST_TIES_TO_EVEN));
|
||||
op_names.push_back(builtin_name("roundNearestTiesToAway", OP_FLOAT_RM_NEAREST_TIES_TO_AWAY));
|
||||
op_names.push_back(builtin_name("roundTowardPositive", OP_FLOAT_RM_TOWARD_POSITIVE));
|
||||
op_names.push_back(builtin_name("roundTowardNegative", OP_FLOAT_RM_TOWARD_NEGATIVE));
|
||||
op_names.push_back(builtin_name("roundTowardZero", OP_FLOAT_RM_TOWARD_ZERO));
|
||||
|
||||
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("RNE", OP_FLOAT_RM_NEAREST_TIES_TO_EVEN));
|
||||
op_names.push_back(builtin_name("RNA", OP_FLOAT_RM_NEAREST_TIES_TO_AWAY));
|
||||
op_names.push_back(builtin_name("RTP", OP_FLOAT_RM_TOWARD_POSITIVE));
|
||||
op_names.push_back(builtin_name("RTN", OP_FLOAT_RM_TOWARD_NEGATIVE));
|
||||
op_names.push_back(builtin_name("RTZ", OP_FLOAT_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));
|
||||
|
@ -643,7 +629,8 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
|
|||
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("to_fp", OP_TO_FLOAT));
|
||||
op_names.push_back(builtin_name("to_fp", OP_FLOAT_TO_FP));
|
||||
op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
|
||||
}
|
||||
|
||||
void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
|
||||
|
@ -670,11 +657,11 @@ bool float_decl_plugin::is_value(app * e) const {
|
|||
if (e->get_family_id() != m_family_id)
|
||||
return false;
|
||||
switch (e->get_decl_kind()) {
|
||||
case OP_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_RM_TOWARD_POSITIVE:
|
||||
case OP_RM_TOWARD_NEGATIVE:
|
||||
case OP_RM_TOWARD_ZERO:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_FLOAT_RM_TOWARD_POSITIVE:
|
||||
case OP_FLOAT_RM_TOWARD_NEGATIVE:
|
||||
case OP_FLOAT_RM_TOWARD_ZERO:
|
||||
case OP_FLOAT_VALUE:
|
||||
case OP_FLOAT_PLUS_INF:
|
||||
case OP_FLOAT_MINUS_INF:
|
||||
|
@ -682,7 +669,7 @@ bool float_decl_plugin::is_value(app * e) const {
|
|||
case OP_FLOAT_MINUS_ZERO:
|
||||
case OP_FLOAT_NAN:
|
||||
return true;
|
||||
case OP_TO_FLOAT:
|
||||
case OP_FLOAT_TO_FP:
|
||||
return m_manager->is_value(e->get_arg(0));
|
||||
default:
|
||||
return false;
|
||||
|
|
|
@ -35,11 +35,11 @@ enum float_sort_kind {
|
|||
};
|
||||
|
||||
enum float_op_kind {
|
||||
OP_RM_NEAREST_TIES_TO_EVEN,
|
||||
OP_RM_NEAREST_TIES_TO_AWAY,
|
||||
OP_RM_TOWARD_POSITIVE,
|
||||
OP_RM_TOWARD_NEGATIVE,
|
||||
OP_RM_TOWARD_ZERO,
|
||||
OP_FLOAT_RM_NEAREST_TIES_TO_EVEN,
|
||||
OP_FLOAT_RM_NEAREST_TIES_TO_AWAY,
|
||||
OP_FLOAT_RM_TOWARD_POSITIVE,
|
||||
OP_FLOAT_RM_TOWARD_NEGATIVE,
|
||||
OP_FLOAT_RM_TOWARD_ZERO,
|
||||
|
||||
OP_FLOAT_VALUE,
|
||||
OP_FLOAT_PLUS_INF,
|
||||
|
@ -76,11 +76,9 @@ enum float_op_kind {
|
|||
OP_FLOAT_IS_NEGATIVE,
|
||||
OP_FLOAT_IS_POSITIVE,
|
||||
|
||||
OP_TO_FLOAT,
|
||||
OP_FLOAT_TO_IEEE_BV,
|
||||
|
||||
OP_FLOAT_FP,
|
||||
OP_FLOAT_TO_FP,
|
||||
OP_FLOAT_TO_FP,
|
||||
OP_FLOAT_TO_FP_UNSIGNED,
|
||||
OP_FLOAT_TO_UBV,
|
||||
OP_FLOAT_TO_SBV,
|
||||
OP_FLOAT_TO_REAL,
|
||||
|
@ -134,9 +132,7 @@ class float_decl_plugin : public decl_plugin {
|
|||
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_float_to_ieee_bv(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_from3bv(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,
|
||||
|
@ -210,11 +206,11 @@ public:
|
|||
unsigned get_ebits(sort * s);
|
||||
unsigned get_sbits(sort * s);
|
||||
|
||||
app * mk_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_RM_NEAREST_TIES_TO_EVEN); }
|
||||
app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_RM_NEAREST_TIES_TO_AWAY); }
|
||||
app * mk_round_toward_positive() { return m().mk_const(m_fid, OP_RM_TOWARD_POSITIVE); }
|
||||
app * mk_round_toward_negative() { return m().mk_const(m_fid, OP_RM_TOWARD_NEGATIVE); }
|
||||
app * mk_round_toward_zero() { return m().mk_const(m_fid, OP_RM_TOWARD_ZERO); }
|
||||
app * mk_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_FLOAT_RM_NEAREST_TIES_TO_EVEN); }
|
||||
app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_FLOAT_RM_NEAREST_TIES_TO_AWAY); }
|
||||
app * mk_round_toward_positive() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_POSITIVE); }
|
||||
app * mk_round_toward_negative() { return m().mk_const(m_fid, OP_FLOAT_RM_TOWARD_NEGATIVE); }
|
||||
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);
|
||||
|
@ -240,9 +236,9 @@ public:
|
|||
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); }
|
||||
|
||||
bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); }
|
||||
bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_FLOAT_TO_FP); }
|
||||
|
||||
app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); }
|
||||
app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_TO_FP, arg1, arg2); }
|
||||
app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); }
|
||||
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); }
|
||||
|
@ -277,8 +273,6 @@ public:
|
|||
app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
|
||||
|
||||
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); }
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -53,8 +53,8 @@ fpa2bv_converter::~fpa2bv_converter() {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
|
||||
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
|
||||
expr_ref sgn(m), s(m), e(m);
|
||||
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn);
|
||||
|
@ -73,8 +73,8 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
|
||||
SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
|
||||
expr_ref sgn(m), s(m), e(m);
|
||||
m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), sgn);
|
||||
|
@ -2203,7 +2203,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
}
|
||||
|
||||
void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
|
||||
sgn = to_app(e)->get_arg(0);
|
||||
|
@ -2252,7 +2252,7 @@ void fpa2bv_converter::mk_is_ninf(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
expr * a0 = to_app(e)->get_arg(0);
|
||||
expr_ref zero(m);
|
||||
|
@ -2261,7 +2261,7 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
expr * a0 = to_app(e)->get_arg(0);
|
||||
expr_ref one(m);
|
||||
|
@ -2424,7 +2424,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) {
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
|
||||
sort * srt = to_app(e)->get_decl()->get_range();
|
||||
|
@ -2519,11 +2519,11 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
|
|||
{
|
||||
switch(f->get_decl_kind())
|
||||
{
|
||||
case OP_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break;
|
||||
case OP_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break;
|
||||
case OP_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break;
|
||||
case OP_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break;
|
||||
case OP_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break;
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break;
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break;
|
||||
case OP_FLOAT_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break;
|
||||
case OP_FLOAT_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break;
|
||||
case OP_FLOAT_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break;
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -73,7 +73,7 @@ public:
|
|||
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
|
||||
SASSERT(m_bv_util.is_bv(significand));
|
||||
SASSERT(m_bv_util.is_bv(exponent));
|
||||
result = m.mk_app(m_util.get_family_id(), OP_TO_FLOAT, sign, significand, exponent);
|
||||
result = m.mk_app(m_util.get_family_id(), OP_FLOAT_FP, sign, significand, exponent);
|
||||
}
|
||||
|
||||
void mk_eq(expr * a, expr * b, expr_ref & result);
|
||||
|
|
|
@ -107,11 +107,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
|
||||
if (m_conv.is_float_family(f)) {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_RM_TOWARD_NEGATIVE:
|
||||
case OP_RM_TOWARD_POSITIVE:
|
||||
case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_AWAY:
|
||||
case OP_FLOAT_RM_NEAREST_TIES_TO_EVEN:
|
||||
case OP_FLOAT_RM_TOWARD_NEGATIVE:
|
||||
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;
|
||||
|
@ -144,8 +144,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(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_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
|
||||
case OP_FLOAT_TO_FP: m_conv.mk_to_float(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;
|
||||
|
|
|
@ -36,7 +36,7 @@ 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_fp(f, num_args, args, result); break;
|
||||
case OP_FLOAT_TO_FP: 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_NEG: SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
|
||||
|
@ -63,8 +63,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
|
|||
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_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_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(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;
|
||||
|
|
|
@ -135,13 +135,7 @@ namespace smt {
|
|||
simp(a->get_arg(2), exp, pr_exp);
|
||||
|
||||
m_converter.mk_triple(sgn, sig, exp, bv_term);
|
||||
}
|
||||
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);
|
||||
simp(t, bv_term, bv_pr);
|
||||
}
|
||||
}
|
||||
else
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
|
@ -420,17 +414,6 @@ namespace smt {
|
|||
ctx.mark_as_relevant(bv_sig);
|
||||
ctx.mark_as_relevant(bv_exp);
|
||||
}
|
||||
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())
|
||||
std::swap(n, ex_a);
|
||||
eq = m.mk_eq(n, ex_a);
|
||||
ctx.internalize(eq, false);
|
||||
literal l = ctx.get_literal(eq);
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
ctx.mark_as_relevant(l);
|
||||
}
|
||||
else
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
|
|
@ -81,7 +81,7 @@ namespace smt {
|
|||
|
||||
protected:
|
||||
void split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
|
||||
SASSERT(is_app_of(e, get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(is_app_of(e, get_family_id(), OP_FLOAT_TO_FP));
|
||||
SASSERT(to_app(e)->get_num_args() == 3);
|
||||
sgn = to_app(e)->get_arg(0);
|
||||
sig = to_app(e)->get_arg(1);
|
||||
|
|
|
@ -116,7 +116,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
bv_mdl->eval(a->get_arg(1), sig, true);
|
||||
bv_mdl->eval(a->get_arg(2), exp, true);
|
||||
|
||||
SASSERT(a->is_app_of(fu.get_family_id(), OP_TO_FLOAT));
|
||||
SASSERT(a->is_app_of(fu.get_family_id(), OP_FLOAT_TO_FP));
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0);
|
||||
|
|
Loading…
Reference in a new issue