mirror of
https://github.com/Z3Prover/z3
synced 2025-06-03 21:01:22 +00:00
Added extraction of uint64 significand bits from FP numerals.
This commit is contained in:
parent
624cc8a874
commit
d39969f0a0
2 changed files with 37 additions and 0 deletions
|
@ -765,7 +765,30 @@ extern "C" {
|
||||||
mpqm.display_decimal(ss, q, sbits);
|
mpqm.display_decimal(ss, q, sbits);
|
||||||
return mk_c(c)->mk_external_string(ss.str());
|
return mk_c(c)->mk_external_string(ss.str());
|
||||||
Z3_CATCH_RETURN("");
|
Z3_CATCH_RETURN("");
|
||||||
|
}
|
||||||
|
|
||||||
|
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
|
||||||
|
Z3_TRY;
|
||||||
|
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
|
||||||
|
RESET_ERROR_CODE();
|
||||||
|
ast_manager & m = mk_c(c)->m();
|
||||||
|
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||||
|
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||||
|
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||||
|
scoped_mpf val(mpfm);
|
||||||
|
bool r = plugin->is_numeral(to_expr(t), val);
|
||||||
|
if (!r) {
|
||||||
|
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
const mpz & z = mpfm.sig(val);
|
||||||
|
if (!mpzm.is_uint64(z)) {
|
||||||
|
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
*n = mpzm.get_uint64(z);
|
||||||
|
return 1;
|
||||||
|
Z3_CATCH_RETURN(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
|
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
|
||||||
|
|
|
@ -858,6 +858,20 @@ extern "C" {
|
||||||
*/
|
*/
|
||||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
|
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
|
||||||
|
|
||||||
|
/**
|
||||||
|
\brief Return the significand value of a floating-point numeral as a uint64.
|
||||||
|
|
||||||
|
\param c logical context
|
||||||
|
\param t a floating-point numeral
|
||||||
|
|
||||||
|
Remarks: This function extracts the significand bits in `t`, without the
|
||||||
|
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
|
||||||
|
signicand does not fit into a uint64.
|
||||||
|
|
||||||
|
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST)))
|
||||||
|
*/
|
||||||
|
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
\brief Return the exponent value of a floating-point numeral as a string
|
\brief Return the exponent value of a floating-point numeral as a string
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue