Added accessors to extract sign/exponent/significand BV numerals from FP numerals.

src/api/api_fpa.cpp

@@ -909,6 +909,8 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
         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();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
@@ -929,6 +931,101 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_sign_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_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)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        if (is_app_of(e, fid, OP_FPA_PLUS_INF)) {
+            expr * r = ctx->bvutil().mk_numeral(0, 1);
+            ctx->save_ast_trail(r);
+            RETURN_Z3(of_expr(r));
+        }
+        if (is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+            expr * r = ctx->bvutil().mk_numeral(1, 1);
+            ctx->save_ast_trail(r);
+            RETURN_Z3(of_expr(r));
+        }
+        if (!fu.is_fp(e)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        app * a = to_app(e);
+        RETURN_Z3(of_expr(a->get_arg(0)));
+        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_util & fu = mk_c(c)->fpautil();
+        expr * e = to_expr(t);
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        if (!fu.is_fp(e)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        api::context * ctx = mk_c(c);
+        app * a = to_app(e);
+        RETURN_Z3(of_expr(a->get_arg(1)));
+        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);
+        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_util & fu = mk_c(c)->fpautil();
+        expr * e = to_expr(t);
+        if (!is_app(e) ||
+            is_app_of(e, fid, OP_FPA_NAN) ||
+            is_app_of(e, fid, OP_FPA_PLUS_INF) ||
+            is_app_of(e, fid, OP_FPA_MINUS_INF)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        if (!fu.is_fp(e)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            RETURN_Z3(0);
+        }
+        api::context * ctx = mk_c(c);
+        app * a = to_app(e);
+        RETURN_Z3(of_expr(a->get_arg(2)));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_significand_string(c, t);

src/api/dotnet/FPNum.cs

@@ -14,7 +14,7 @@ Author:
     Christoph Wintersteiger (cwinter) 2013-06-10
 
 Notes:
-    
+
 --*/
 using System;
 using System.Diagnostics.Contracts;
@@ -27,6 +27,48 @@ namespace Microsoft.Z3
     [ContractVerification(true)]
     public class FPNum : FPExpr
     {
+        /// <summary>
+        /// The sign of a floating-point numeral as a bit-vector expression
+        /// </summary>
+        /// <remarks>
+        /// NaN's do not have a bit-vector sign, so they are invalid arguments.
+        /// </remarks>
+        public BitVecExpr BVSign
+        {
+            get
+            {
+                return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The exponent of a floating-point numeral as a bit-vector expression
+        /// </summary>
+        /// <remarks>
+        /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments.
+        /// </remarks>
+        public BitVecExpr BVExponent
+        {
+            get
+            {
+                return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The significand of a floating-point numeral as a bit-vector expression
+        /// </summary>
+        /// <remarks>
+        /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments.
+        /// </remarks>
+        public BitVecExpr BVSignificand
+        {
+            get
+            {
+                return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject));
+            }
+        }
+
         /// <summary>
         /// Retrieves the sign of a floating-point literal
         /// </summary>
@@ -38,7 +80,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)                
+                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
                     throw new Z3Exception("Sign is not a Boolean value");
                 return res != 0;
             }
@@ -63,7 +105,7 @@ namespace Microsoft.Z3
         /// The significand value of a floating-point numeral as a UInt64
         /// </summary>
         /// <remarks>
-        /// This function extracts the significand bits, without the 
+        /// 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>
@@ -73,7 +115,7 @@ namespace Microsoft.Z3
             {
                 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");                
+                    throw new Z3Exception("Significand is not a 64 bit unsigned integer");
                 return result;
             }
         }
@@ -113,7 +155,7 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Returns a string representation of the numeral.
-        /// </summary>        
+        /// </summary>
         public override string ToString()
         {
             return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);

src/api/java/FPNum.java

@@ -21,6 +21,33 @@ package com.microsoft.z3;
  */
 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 

src/api/ml/z3.ml

@@ -1324,6 +1324,9 @@ struct
   let mk_to_real = Z3native.mk_fpa_to_real
   let get_ebits = Z3native.fpa_get_ebits
   let get_sbits = Z3native.fpa_get_sbits
+  let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv
+  let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv
+  let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv
   let get_numeral_sign = Z3native.fpa_get_numeral_sign
   let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
   let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64

src/api/ml/z3.mli

@@ -2138,6 +2138,18 @@ sig
   (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *)
   val get_sbits : context -> Sort.sort -> int
 
+  (** Return 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. *)
+  val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr
+
+  (** Return 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. *)
+  val get_numeral_exponent_bv : context -> Expr.expr -> Expr.expr
+
+  (** Return the significand value 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. *)
+  val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr
+
   (** Retrieves the sign of a floating-point literal. *)
   val get_numeral_sign : context -> Expr.expr -> bool * int
 

src/api/python/z3/z3.py

@@ -8446,6 +8446,30 @@ class FPNumRef(FPRef):
         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.
 

src/api/z3_fpa.h

@@ -822,6 +822,42 @@ extern "C" {
     */
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
 
+    /**
+        \brief Retrieves the sign of a floating-point literal as a bit-vector expression.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        Remarks: NaN is an invalid argument.
+
+        def_API('Z3_fpa_get_numeral_sign_bv', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Retrieves the significand 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_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.