From abcb6040d4593545a7019a4f4431444bc4d03dad Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Oct 2016 17:39:31 +0100 Subject: [PATCH] Refactored FPA numeral accessors. --- src/api/api_fpa.cpp | 102 +++++++++++++++++---------------- src/api/dotnet/FPNum.cs | 71 ++++++++++------------- src/api/java/FPNum.java | 66 ++++++++++----------- src/api/python/z3/z3.py | 60 +++++++++---------- src/api/python/z3/z3printer.py | 4 +- src/api/z3_fpa.h | 44 ++++++++------ 6 files changed, 175 insertions(+), 172 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index ce0cf1ae6..669df8666 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -946,7 +946,7 @@ extern "C" { fpa_util & fu = mk_c(c)->fpautil(); api::context * ctx = mk_c(c); expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } @@ -956,6 +956,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } + std::cout << "val=" << mpfm.to_string(val) << std::endl; app * a; if (mpfm.is_pos(val)) a = ctx->bvutil().mk_numeral(0, 1); @@ -966,44 +967,6 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t) { - Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_bv(c, t); - RESET_ERROR_CODE(); - CHECK_NON_NULL(t, 0); - CHECK_VALID_AST(t, 0); - ast_manager & m = mk_c(c)->m(); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); - family_id fid = mk_c(c)->get_fpa_fid(); - fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); - fpa_util & fu = mk_c(c)->fpautil(); - expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - scoped_mpf val(mpfm); - bool r = plugin->is_numeral(e, val); - if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - unsigned ebits = val.get().get_ebits(); - mpf_exp_t q = mpfm.exp(val); - mpf_exp_t q_biassed = mpfm.bias_exp(ebits, q); - app * a; - if (mpfm.is_inf(val)) - a = mk_c(c)->bvutil().mk_numeral(-1, ebits); - else if (mpfm.is_zero(val) || mpfm.is_denormal(val)) - a = mk_c(c)->bvutil().mk_numeral(0, ebits); - else - a = mk_c(c)->bvutil().mk_numeral(q_biassed, ebits); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_expr(a)); - Z3_CATCH_RETURN(0); - } - Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_bv(c, t); @@ -1018,7 +981,7 @@ extern "C" { SASSERT(plugin != 0); fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } @@ -1106,9 +1069,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) { + Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased) { Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_string(c, t); + LOG_Z3_fpa_get_numeral_exponent_string(c, t, biased); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1127,19 +1090,21 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } + unsigned ebits = val.get().get_ebits(); mpf_exp_t exp = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : - mpfm.exp(val); + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) mpfm.unbias_exp(ebits, exp); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); Z3_CATCH_RETURN(""); } - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) { + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased) { Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n); + LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1160,14 +1125,51 @@ extern "C" { *n = 0; return 0; } + unsigned ebits = val.get().get_ebits(); *n = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : - mpfm.exp(val); + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) *n = mpfm.unbias_exp(ebits, *n); return 1; Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased) { + Z3_TRY; + LOG_Z3_fpa_get_numeral_exponent_bv(c, t, biased); + RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); + ast_manager & m = mk_c(c)->m(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); + fpa_util & fu = mk_c(c)->fpautil(); + expr * e = to_expr(t); + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + scoped_mpf val(mpfm); + bool r = plugin->is_numeral(e, val); + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + unsigned ebits = val.get().get_ebits(); + mpf_exp_t exp = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) exp = mpfm.unbias_exp(ebits, exp); + app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_expr(a)); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_to_ieee_bv(c, t); diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index ed0367481..705e7304e 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// /// NaN's do not have a bit-vector sign, so they are invalid arguments. /// - public BitVecExpr BVSign + public BitVecExpr SignBV { get { @@ -41,34 +41,6 @@ namespace Microsoft.Z3 } } - /// - /// The exponent of a floating-point numeral as a bit-vector expression - /// - /// - /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. - /// - public BitVecExpr BVExponent - { - get - { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject)); - } - } - - /// - /// The significand of a floating-point numeral as a bit-vector expression - /// - /// - /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. - /// - public BitVecExpr BVSignificand - { - get - { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); - } - } - /// /// Retrieves the sign of a floating-point literal /// @@ -121,28 +93,47 @@ namespace Microsoft.Z3 } /// - /// Return the exponent value of a floating-point numeral as a string + /// The significand of a floating-point numeral as a bit-vector expression /// - public string Exponent + /// + /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. + /// + public BitVecExpr SignificandBV { get { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); } } + /// + /// Return the (biased) exponent value of a floating-point numeral as a string + /// + public string Exponent(bool biased = true) + { + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0); + } + /// /// Return the exponent value of a floating-point numeral as a signed 64-bit integer /// - public Int64 ExponentInt64 + public Int64 ExponentInt64(bool biased = true) { - get - { - Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0) - throw new Z3Exception("Exponent is not a 64 bit integer"); - return result; - } + Int64 result = 0; + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0) + throw new Z3Exception("Exponent is not a 64 bit integer"); + return result; + } + + /// + /// The exponent of a floating-point numeral as a bit-vector expression + /// + /// + /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. + /// + public BitVecExpr ExponentBV(bool biased = true) + { + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); } #region Internal diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 7bfca0f86..252d9e012 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -20,34 +20,7 @@ package com.microsoft.z3; * FloatingPoint Numerals */ public class FPNum extends FPExpr -{ - /** - * The sign of a floating-point numeral as a bit-vector expression - * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVSign() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject())); - } - - /** - * The exponent of a floating-point numeral as a bit-vector expression - * Remarks: +oo, -oo, and NaN's do not have a bit-vector exponent, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVExponent() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject())); - } - - /** - * The significand of a floating-point numeral as a bit-vector expression - * Remarks: +oo, -oo, and NaN's do not have a bit-vector significand, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVSignificand() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject())); - } - +{ /** * Retrieves the sign of a floating-point literal * Remarks: returns true if the numeral is negative @@ -60,6 +33,15 @@ public class FPNum extends FPExpr return res.value != 0; } + /** + * The sign of a floating-point numeral as a bit-vector expression + * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments. + * @throws Z3Exception + */ + public BitVecExpr getSignBV() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject())); + } + /** * The significand value of a floating-point numeral as a string * Remarks: The significand s is always 0 < s < 2.0; the resulting string is long @@ -84,25 +66,45 @@ public class FPNum extends FPExpr throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return res.value; } + + /** + * The significand of a floating-point numeral as a bit-vector expression + * Remarks: NaN is an invalid argument. + * @throws Z3Exception + */ + public BitVecExpr getSignificandBV() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject())); + } /** * Return the exponent value of a floating-point numeral as a string + * Remarks: NaN is an invalid argument. * @throws Z3Exception */ - public String getExponent() { - return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject()); + public String getExponent(boolean biased) { + return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased); } /** * Return the exponent value of a floating-point numeral as a signed 64-bit integer + * Remarks: NaN is an invalid argument. * @throws Z3Exception */ - public long getExponentInt64() { + public long getExponentInt64(boolean biased) { Native.LongPtr res = new Native.LongPtr(); - if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res)) + if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased)) throw new Z3Exception("Exponent is not a 64 bit integer"); return res.value; } + + /** + * The exponent of a floating-point numeral as a bit-vector expression + * Remarks: NaN is an invalid argument. + * @throws Z3Exception + */ + public BitVecExpr getExponentBV(boolean biased) { + return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased)); + } public FPNum(Context ctx, long obj) { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index fc9ef6d62..e651fc04f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8445,31 +8445,7 @@ class FPNumRef(FPRef): def isNegative(self): k = self.decl().kind() return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True) - - """ - The sign of a floating-point numeral as a bit-vector expression - - Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. - """ - def BVSign(self): - return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), ctx) - """ - The exponent of a floating-point numeral as a bit-vector expression - - Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. - """ - def BVExponent(self): - return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast()), ctx) - - """ - The sign of a floating-point numeral as a bit-vector expression - - Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. - """ - def BVSignificand(self): - return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), ctx) - """ The sign of the numeral. @@ -8486,6 +8462,15 @@ class FPNumRef(FPRef): raise Z3Exception("error retrieving the sign of a numeral.") return l.value != 0 + """ + The sign of a floating-point numeral as a bit-vector expression + + Remark: NaN's are invalid arguments. + """ + def sign_as_bv(self): + return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) + + """ The significand of the numeral. @@ -8495,6 +8480,14 @@ class FPNumRef(FPRef): """ def significand(self): return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) + + """ + The significand of a floating-point numeral as a bit-vector expression + + Remark: NaN are invalid arguments. + """ + def significand_as_bv(self): + return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) """ The exponent of the numeral. @@ -8503,8 +8496,8 @@ class FPNumRef(FPRef): >>> x.exponent() 1 """ - def exponent(self): - return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast()) + def exponent(self, biased=True): + return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) """ The exponent of the numeral as a long. @@ -8513,12 +8506,21 @@ class FPNumRef(FPRef): >>> x.exponent_as_long() 1 """ - def exponent_as_long(self): + def exponent_as_long(self, biased=True): ptr = (ctypes.c_longlong * 1)() - if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr): + if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): raise Z3Exception("error retrieving the exponent of a numeral.") return ptr[0] + """ + The exponent of a floating-point numeral as a bit-vector expression + + Remark: NaNs are invalid arguments. + """ + def exponent_as_bv(self, biased=True): + return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) + + """ The string representation of the numeral. @@ -8527,7 +8529,7 @@ class FPNumRef(FPRef): 1.25*(2**4) """ def as_string(self): - s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast()) + s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) return ("FPVal(%s, %s)" % (s, self.sort())) def is_fp(a): diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 2e3a528bf..8a67fa911 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -620,8 +620,8 @@ class Formatter: r = [] sgn = c_int(0) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) + exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) - exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast) r.append(to_format('FPVal(')) if sgnb and sgn.value != 0: r.append(to_format('-')) @@ -650,8 +650,8 @@ class Formatter: r = [] sgn = (ctypes.c_int)(0) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) + exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) - exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast) if sgnb and sgn.value != 0: r.append(to_format('-')) r.append(to_format(sig)) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 5544099d6..420106838 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -900,24 +900,12 @@ extern "C" { \param c logical context \param t a floating-point numeral - Remarks: +oo, -oo and NaN are invalid arguments. + Remarks: NaN is an invalid argument. def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t); - /** - \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. - - \param c logical context - \param t a floating-point numeral - - Remarks: +oo, -oo and NaN are invalid arguments. - - def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t); - /** \brief Retrieves the sign of a floating-point literal. @@ -954,23 +942,25 @@ extern "C" { Remarks: This function extracts the significand bits in `t`, without the hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the - significand does not fit into a uint64. + significand does not fit into a uint64. NaN is an invalid argument. def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64))) */ Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __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. \param c logical context \param t a floating-point numeral + \param biased flag to indicate whether the result is in biased representation Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid argument. - def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL))) */ - Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t); + Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased); /** \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer @@ -978,12 +968,28 @@ extern "C" { \param c logical context \param t a floating-point numeral \param n exponent + \param biased flag to indicate whether the result is in biased representation Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid argument. - def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) + def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL))) */ - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n); + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased); + + /** + \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. + + \param c logical context + \param t a floating-point numeral + \param biased flag to indicate whether the result is in biased representation + + Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid arguments. + + def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL))) + */ + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased); /** \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.