From 004bf1471f057d70b3860d36588ac236248da9fc Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 10 Jun 2015 13:17:34 +0100
Subject: [PATCH] Added conversion function for Goal to Expr conversion in
 .NET, Java, ML

---
 src/api/dotnet/Goal.cs | 15 +++++++++++++++
 src/api/java/Goal.java | 16 ++++++++++++++++
 src/api/ml/z3.ml       |  9 +++++++++
 src/api/ml/z3.mli      |  3 +++
 4 files changed, 43 insertions(+)

diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 46d519d35..5ee44f34b 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -208,6 +208,21 @@ namespace Microsoft.Z3
             return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Goal to BoolExpr conversion.
+        /// </summary>
+        /// <returns>A string representation of the Goal.</returns>
+        public BoolExpr AsBoolExpr() {
+            uint n = Size;
+            if (n == 0) 
+                return Context.MkTrue();
+            else if (n == 1)                
+                return Formulas[0];
+            else {
+                return Context.MkAnd(Formulas);
+            }
+        }
+
         #region Internal
         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index 18aecb557..41d4e27ac 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -221,6 +221,22 @@ public class Goal extends Z3Object
             return "Z3Exception: " + e.getMessage();
         }
     }
+    
+    /** 
+     * Goal to BoolExpr conversion.
+     *  
+     * Returns a string representation of the Goal.
+     **/
+    public BoolExpr AsBoolExpr() {
+        int n = size();
+        if (n == 0) 
+            return getContext().mkTrue();
+        else if (n == 1)                
+            return getFormulas()[0];
+        else {
+            return getContext().mkAnd(getFormulas());
+        }
+    }
 
     Goal(Context ctx, long obj)
     {
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index a776eacd3..51eb35e29 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -2199,6 +2199,15 @@ struct
     create ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs)
 
   let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x)
+
+  let as_expr ( x : goal ) = 
+	let n = get_size x in
+	if n = 0 then 
+	  (Boolean.mk_true (z3obj_gc x)) 
+	else if n = 1 then
+	  (List.hd (get_formulas x))
+	else
+	  (Boolean.mk_and (z3obj_gc x) (get_formulas x))
 end  
 
 
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index ce937d4e0..e0f89565d 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2653,6 +2653,9 @@ sig
 
   (**  A string representation of the Goal. *)
   val to_string : goal -> string
+
+  (** Goal to BoolExpr conversion. *)
+  val as_expr : goal -> Expr.expr
 end
 
 (** Models