3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java, and ML APIs.

This commit is contained in:
Christoph M. Wintersteiger 2015-06-09 12:57:19 +01:00
parent da3243fb07
commit 98f2de3216
5 changed files with 43 additions and 1 deletions

View file

@ -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>

View file

@ -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

View file

@ -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 ) =

View file

@ -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

View file

@ -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)))
*/