Added conversion function for Goal to Expr conversion in .NET, Java, ML

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); }
 

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)
     {

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  
 
 

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