From 44751c0ef8212bc78400aac42432e4fc7db3fa15 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Jul 2014 15:27:24 -0700
Subject: [PATCH] Add missing .NET API functions for parsing rules into
 fixedpoint object

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Fixedpoint.cs | 39 +++++++++++++++++++++++++-----------
 1 file changed, 27 insertions(+), 12 deletions(-)

diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 8c6e6c4c6..3f40b220b 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -269,6 +269,14 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
+        BoolExpr[] ToBoolExprs(ASTVector v) {
+            uint n = v.Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = new BoolExpr(Context, v[i].NativeObject);
+            return res;
+        }
+
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
@@ -278,12 +286,7 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
             }
         }
 
@@ -296,15 +299,27 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
             }
         }
 
+        /// <summary>
+        /// Parse an SMT-LIB2 file with fixedpoint rules. 
+        /// Add the rules to the current fixedpoint context. 
+        /// Return the set of queries in the file.
+        /// </summary>                
+	public BoolExpr[] ParseFile(string file) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        }
+
+        /// <summary>
+        /// Similar to ParseFile. Instead it takes as argument a string.
+        /// </summary>                
+
+	public BoolExpr[] ParseString(string s) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+        }
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)