diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 5d423c725..048113eca 100644
--- a/src/api/api_fpa.cpp
+++ b/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);
diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index ac1fae5f5..ed0367481 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/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
{
+ ///
+ /// The sign of a floating-point numeral as a bit-vector expression
+ ///
+ ///
+ /// NaN's do not have a bit-vector sign, so they are invalid arguments.
+ ///
+ public BitVecExpr BVSign
+ {
+ get
+ {
+ return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject));
+ }
+ }
+
+ ///
+ /// 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
///
@@ -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
///
///
- /// 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.
///
@@ -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
///
/// Returns a string representation of the numeral.
- ///
+ ///
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
index 402d25ebe..7bfca0f86 100644
--- a/src/api/java/FPNum.java
+++ b/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
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index b7016c4c8..613db591e 100644
--- a/src/api/ml/z3.ml
+++ b/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
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 1c91b28aa..e08028c61 100644
--- a/src/api/ml/z3.mli
+++ b/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
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a037bbc5d..fc9ef6d62 100644
--- a/src/api/python/z3/z3.py
+++ b/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.
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 510fa0473..9abbb7b60 100644
--- a/src/api/z3_fpa.h
+++ b/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.