diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index e85687ccf..ac1fae5f5 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -59,6 +59,25 @@ namespace Microsoft.Z3
}
}
+ ///
+ /// The significand value of a floating-point numeral as a UInt64
+ ///
+ ///
+ /// This function extracts the significand bits, without the
+ /// hidden bit or normalization. Throws an exception if the
+ /// significand does not fit into a UInt64.
+ ///
+ public UInt64 SignificandUInt64
+ {
+ get
+ {
+ UInt64 result = 0;
+ if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+ throw new Z3Exception("Significand is not a 64 bit unsigned integer");
+ return result;
+ }
+ }
+
///
/// Return the exponent value of a floating-point numeral as a string
///
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
index 9a147778a..69a44c559 100644
--- a/src/api/java/FPNum.java
+++ b/src/api/java/FPNum.java
@@ -43,6 +43,21 @@ public class FPNum extends FPExpr
return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
}
+ /**
+ * The significand value of a floating-point numeral as a UInt64
+ * Remarks: This function extracts the significand bits, without the
+ * hidden bit or normalization. Throws an exception if the
+ * significand does not fit into a UInt64.
+ * @throws Z3Exception
+ **/
+ public long getSignificandUInt64()
+ {
+ Native.LongPtr res = new Native.LongPtr();
+ if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true)
+ throw new Z3Exception("Significand is not a 64 bit unsigned integer");
+ return res.value;
+ }
+
/**
* Return the exponent value of a floating-point numeral as a string
* @throws Z3Exception
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index fa6ce6c81..a776eacd3 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2059,6 +2059,8 @@ struct
(Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t))
let get_numeral_significand_string ( ctx : context ) ( t : expr ) =
(Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t))
+ let get_numeral_significand_uint ( ctx : context ) ( t : expr ) =
+ (Z3native.fpa_get_numeral_significand_uint64 (context_gno ctx) (Expr.gno t))
let get_numeral_exponent_string ( ctx : context ) ( t : expr ) =
(Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t))
let get_numeral_exponent_int ( ctx : context ) ( t : expr ) =
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 2099359fa..ce937d4e0 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2161,6 +2161,12 @@ sig
(** Return the significand value of a floating-point numeral as a string. *)
val get_numeral_significand_string : context -> Expr.expr -> string
+ (** Return the significand value of a floating-point numeral as a uint64.
+ Remark: This function extracts the significand bits, without the
+ hidden bit or normalization. Throws an exception if the
+ significand does not fit into a uint64. *)
+ val get_numeral_significand_uint : context -> Expr.expr -> bool * int
+
(** Return the exponent value of a floating-point numeral as a string *)
val get_numeral_exponent_string : context -> Expr.expr -> string
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 6bd752f0a..7813142a3 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -866,7 +866,7 @@ 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
- signicand does not fit into a uint64.
+ significand does not fit into a uint64.
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
*/