mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Added FPA numeral predicates to .NET API

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-26 18:44:25 +01:00
parent 963dfad10e
commit c573a7446b
1 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/api/dotnet/FPNum.cs
View file

@ -136,6 +136,36 @@ namespace Microsoft.Z3
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0));
} }
/// <summary>
/// Indicates whether the numeral is a NaN.
/// </summary>
public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is a +oo or -oo.
/// </summary>
public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is +zero or -zero.
/// </summary>
public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is normal.
/// </summary>
public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is subnormal.
/// </summary>
public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is positive.
/// </summary>
public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
#region Internal #region Internal
internal FPNum(Context ctx, IntPtr obj) internal FPNum(Context ctx, IntPtr obj)
: base(ctx, obj) : base(ctx, obj)