From 6b474adc8adb3e8a01a04b76055fa2a59674c48f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 16 Sep 2016 16:48:22 +0100 Subject: [PATCH] Added accessors to extract sign/exponent/significand BV numerals from FP numerals. --- src/api/api_fpa.cpp | 97 +++++++++++++++++++++++++++++++++++++++++ src/api/dotnet/FPNum.cs | 52 +++++++++++++++++++--- src/api/java/FPNum.java | 27 ++++++++++++ src/api/ml/z3.ml | 3 ++ src/api/ml/z3.mli | 12 +++++ src/api/python/z3/z3.py | 24 ++++++++++ src/api/z3_fpa.h | 36 +++++++++++++++ 7 files changed, 246 insertions(+), 5 deletions(-) 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.