From c573a7446bfe8038d0692a0cfd738fbdb557c339 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 26 Oct 2016 18:44:25 +0100
Subject: [PATCH] Added FPA numeral predicates to .NET API

---
 src/api/dotnet/FPNum.cs | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index 705e7304e..05eda00b3 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -136,6 +136,36 @@ namespace Microsoft.Z3
             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
         internal FPNum(Context ctx, IntPtr obj)
             : base(ctx, obj)