From 98f2de32160f13e495d1269a63d84f2e05978658 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 9 Jun 2015 12:57:19 +0100
Subject: [PATCH] Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java,
 and ML APIs.

---
 src/api/dotnet/FPNum.cs | 19 +++++++++++++++++++
 src/api/java/FPNum.java | 15 +++++++++++++++
 src/api/ml/z3.ml        |  2 ++
 src/api/ml/z3.mli       |  6 ++++++
 src/api/z3_fpa.h        |  2 +-
 5 files changed, 43 insertions(+), 1 deletion(-)

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
             }
         }
 
+        /// <summary>
+        /// The significand value of a floating-point numeral as a UInt64
+        /// </summary>
+        /// <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.
+        /// </remarks>
+        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;
+            }
+        }
+
         /// <summary>
         /// Return the exponent value of a floating-point numeral as a string
         /// </summary>
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)))
     */