.NET FPA API overhaul

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

examples/dotnet/Program.cs

@@ -2084,25 +2084,26 @@ namespace test_mapi
 
             FPRMExpr rm = (FPRMExpr)ctx.MkConst(ctx.MkSymbol("rm"), rm_sort);
             BitVecExpr x = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkBitVecSort(64));
-            FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);
+            FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);            
-            RealExpr real_val = ctx.MkReal(42);
-            BitVecExpr bv_val = ctx.MkBV(42, 64);
             FPExpr fp_val = ctx.MkFP(42, double_sort);
 
-            BoolExpr c1 = ctx.MkEq(x, ctx.MkFPToIEEEBV(fp_val));
+            BoolExpr c1 = ctx.MkEq(y, fp_val);
-            BoolExpr c2 = ctx.MkEq(x, ctx.MkBV(42, 64));
+            BoolExpr c2 = ctx.MkEq(x, ctx.MkFPToBV(rm, y, 64, false));
-            BoolExpr c3 = ctx.MkEq(fp_val, ctx.MkFPToFP(rm, real_val, double_sort));
+            BoolExpr c3 = ctx.MkEq(x, ctx.MkBV(42, 64));
-            BoolExpr c4 = ctx.MkAnd(c1, c2);
+            BoolExpr c4 = ctx.MkEq(ctx.MkNumeral(42, ctx.RealSort), ctx.MkFPToReal(fp_val));
-            Console.WriteLine("c3 = " + c3);
+            BoolExpr c5 = ctx.MkAnd(c1, c2, c3, c4);
+            Console.WriteLine("c5 = " + c5);
 
             /* Generic solver */
             Solver s = ctx.MkSolver();
-            s.Assert(c3);
+            s.Assert(c5);
+            
+            Console.WriteLine(s);
 
             if (s.Check() != Status.SATISFIABLE)
                 throw new TestFailedException();
 
-            Console.WriteLine("OK, model: ", s.Model.ToString());
+            Console.WriteLine("OK, model: {0}", s.Model.ToString());
         }
 
         static void Main(string[] args)

src/api/dotnet/AST.cs

@@ -227,10 +227,8 @@ namespace Microsoft.Z3
         internal override void IncRef(IntPtr o)
         {            
             // Console.WriteLine("AST IncRef()");
-            if (Context == null)
+            if (Context == null || o == IntPtr.Zero)
-                throw new Z3Exception("inc() called on null context");
+                return;
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("inc() called on null AST");
             Context.AST_DRQ.IncAndClear(Context, o);
             base.IncRef(o);
         }
@@ -238,10 +236,8 @@ namespace Microsoft.Z3
         internal override void DecRef(IntPtr o)
         {
             // Console.WriteLine("AST DecRef()");
-            if (Context == null)
+            if (Context == null || o == IntPtr.Zero)
-                throw new Z3Exception("dec() called on null context");
+                return;
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("dec() called on null AST");
             Context.AST_DRQ.Add(o);
             base.DecRef(o);
         }

src/api/dotnet/ArithExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArithExpr </summary>
-        internal protected ArithExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArithExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/ArrayExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArrayExpr </summary>
-        internal protected ArrayExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArrayExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/BitVecExpr.cs

@@ -41,7 +41,6 @@ namespace Microsoft.Z3
 
         #region Internal
         /// <summary> Constructor for BitVecExpr </summary>
-        internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }

src/api/dotnet/BoolExpr.cs

@@ -32,8 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for BoolExpr </summary>
-        internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> Constructor for BoolExpr </summary>
         internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }

src/api/dotnet/DatatypeExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for DatatypeExpr </summary>
-        internal protected DatatypeExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal DatatypeExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/EnumSort.cs

@@ -78,7 +78,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);

src/api/dotnet/Expr.cs

@@ -1759,10 +1759,6 @@ namespace Microsoft.Z3
         /// <summary> 
         /// Constructor for Expr 
         /// </summary>
-        internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> 
-        /// Constructor for Expr 
-        /// </summary>
         internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG

src/api/dotnet/FPExpr.cs

@@ -42,11 +42,6 @@ namespace Microsoft.Z3
 
         #region Internal
         /// <summary> Constructor for FPExpr </summary>
-        internal protected FPExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal FPExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/FPRMExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for FPRMExpr </summary>
-        internal protected FPRMExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal FPRMExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/IntExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for IntExpr </summary>
-        internal protected IntExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal IntExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/ListSort.cs

@@ -113,9 +113,9 @@ namespace Microsoft.Z3
             }
         }
 
-        #region Internal        
+        #region Internal
         internal ListSort(Context ctx, Symbol name, Sort elemSort)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);

src/api/dotnet/Quantifier.cs

@@ -160,7 +160,7 @@ namespace Microsoft.Z3
         #region Internal
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(sorts != null);
@@ -203,7 +203,7 @@ namespace Microsoft.Z3
 
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(body != null);

src/api/dotnet/RealExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for RealExpr </summary>
-        internal protected RealExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal RealExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/Sort.cs

@@ -116,8 +116,7 @@ namespace Microsoft.Z3
         #region Internal
         /// <summary>
         /// Sort constructor
-        /// </summary>
+        /// </summary>        
-        internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG
@@ -146,6 +145,8 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
                 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
                 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
+                case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
+                case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
                 default:
                     throw new Z3Exception("Unknown sort kind");
             }

src/api/dotnet/TupleSort.cs

@@ -68,7 +68,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);