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.