Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

src/api/dotnet/ASTMap.cs

@@ -98,11 +98,12 @@ namespace Microsoft.Z3
         /// <summary>
         /// The keys stored in the map.
         /// </summary>
-        public ASTVector Keys
+        public AST[] Keys
         {
             get
             {
-                return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                return res.ToArray();
             }
         }
 

src/api/dotnet/ASTVector.cs

@@ -99,6 +99,30 @@ namespace Microsoft.Z3
             return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Translates an AST vector into an AST[]
+        /// </summary>    
+        public AST[] ToArray()
+        {
+            uint n = Size;
+            AST[] res = new AST[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = AST.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an AST vector into an Expr[]
+        /// </summary>    
+        public Expr[] ToExprArray()
+        {
+            uint n = Size;
+            Expr[] res = new Expr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
         #region Internal
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }

src/api/dotnet/Fixedpoint.cs

@@ -269,14 +269,6 @@ 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>                
@@ -286,7 +278,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
+                return (BoolExpr[])av.ToExprArray();
             }
         }
 
@@ -299,7 +292,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
+                return (BoolExpr[])av.ToExprArray();
             }
         }
 
@@ -316,21 +310,24 @@ namespace Microsoft.Z3
             }
         }
 
-	/// <summary>
+        /// <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) {
+        public BoolExpr[] ParseFile(string file)
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        {
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
+            return (BoolExpr[])av.ToExprArray();
         }
 
         /// <summary>
         /// Similar to ParseFile. Instead it takes as argument a string.
-        /// </summary>                
+        /// </summary>
-
+        public BoolExpr[] ParseString(string s)
-	public BoolExpr[] ParseString(string s) {
+        {
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
+            return (BoolExpr[])av.ToExprArray();
         }
 
 

src/api/dotnet/InterpolationContext.cs

@@ -59,11 +59,7 @@ namespace Microsoft.Z3
             CheckContextMatch(p);
 
             ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
-            uint n = seq.Size;
+            return seq.ToExprArray();
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(this, seq[i].NativeObject);
-            return res;
         }
 
         /// <summary> 
@@ -72,7 +68,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out Expr[] interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
@@ -84,7 +80,7 @@ namespace Microsoft.Z3
 
             IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
             int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
-            interp = new ASTVector(this, i);
+            interp = new ASTVector(this, i).ToExprArray();
             model = new Model(this, m);
             return (Z3_lbool)r;
         }

src/api/dotnet/Model.cs

@@ -265,12 +265,8 @@ namespace Microsoft.Z3
             Contract.Requires(s != null);
             Contract.Ensures(Contract.Result<Expr[]>() != null);
 
-            ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
+            ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));            
-            uint n = nUniv.Size;
+            return av.ToExprArray();
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
-            return res;
         }
 
         /// <summary>

src/api/dotnet/Solver.cs

@@ -178,8 +178,8 @@ namespace Microsoft.Z3
         {
             get
             {
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                return ass.Size;
+                return assertions.Size;
             }
         }
 
@@ -192,12 +192,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                uint n = ass.Size;
+                return (BoolExpr[])assertions.ToExprArray();
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, ass[i].NativeObject);
-                return res;
             }
         }
 
@@ -270,18 +266,14 @@ namespace Microsoft.Z3
         /// The result is empty if <c>Check</c> was not invoked before,
         /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
         /// </remarks>
-        public Expr[] UnsatCore
+        public BoolExpr[] UnsatCore
         {
             get
             {
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
 
-                ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
+                ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
-                uint n = core.Size;
+                return (BoolExpr[])core.ToExprArray();
-                Expr[] res = new Expr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = Expr.Create(Context, core[i].NativeObject);
-                return res;
             }
         }
 

src/api/java/ASTMap.java

@@ -92,10 +92,10 @@ class ASTMap extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ASTVector getKeys()
+    public AST[] getKeys()
     {
-        return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
+        ASTVector av = new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(), getNativeObject()));
-                getNativeObject()));
+        return av.ToArray();
     }
 
     /**

src/api/java/ASTVector.java

@@ -119,12 +119,27 @@ public class ASTVector extends Z3Object
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
-
+    
-    BoolExpr[] ToBoolArray() {
+    /**
+     * Translates the AST vector into an AST[]
+     * */
+    public AST[] ToArray()
+    {
         int n = size();
-        BoolExpr[] res = new BoolExpr[n];
+        AST[] res = new AST[n];
         for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), get(i).getNativeObject());
+            res[i] = AST.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+    
+    /**
+     * Translates the AST vector into an Expr[]
+     * */
+    public Expr[] ToExprArray() {
+        int n = size();
+        Expr[] res = new Expr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Expr.create(getContext(), get(i).getNativeObject());
         return res;	
     }
 }

src/api/java/Fixedpoint.java

@@ -295,10 +295,8 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getRules()
     {
-
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
+        return (BoolExpr[]) v.ToExprArray();
-                getContext().nCtx(), getNativeObject()));
-	return v.ToBoolArray();
     }
 
     /**
@@ -308,10 +306,8 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
+        return (BoolExpr[]) v.ToExprArray();
-                getContext().nCtx(), getNativeObject()));
-	return v.ToBoolArray();
     }
 
     /**
@@ -319,12 +315,34 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Statistics getStatistics() throws Z3Exception
+    public Statistics getStatistics()
     {
         return new Statistics(getContext(), Native.fixedpointGetStatistics(
                 getContext().nCtx(), getNativeObject()));
     }
 
+    /** 
+     * Parse an SMT-LIB2 file with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/        
+    public BoolExpr[] ParseFile(String file)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
+        return (BoolExpr[])av.ToExprArray();
+    }
+
+    /** 
+     * Parse an SMT-LIB2 string with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/ 
+    public BoolExpr[] ParseString(String s)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
+        return (BoolExpr[])av.ToExprArray();
+    }
+    
 
     Fixedpoint(Context ctx, long obj) throws Z3Exception
     {

src/api/java/InterpolationContext.java

@@ -80,11 +80,7 @@ public class InterpolationContext extends Context
         checkContextMatch(p);
 
         ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
-        int n = seq.size();
+        return seq.ToExprArray();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(this, seq.get(i).getNativeObject());
-        return res;
     }
 
     public class ComputeInterpolantResult 
@@ -110,9 +106,8 @@ public class InterpolationContext extends Context
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
         res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
-        if (res.status == Z3_lbool.Z3_L_FALSE) {
+        if (res.status == Z3_lbool.Z3_L_FALSE)
-	    res.interp = (new ASTVector(this, n_i.value)).ToBoolArray();
+            res.interp = (BoolExpr[]) (new ASTVector(this, n_i.value)).ToExprArray();
-	}
         if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }

src/api/java/Model.java

@@ -273,11 +273,7 @@ public class Model extends Z3Object
 
         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
-        int n = nUniv.size();
+        return nUniv.ToExprArray();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
-        return res;
     }
 
     /**

src/api/java/Solver.java

@@ -176,8 +176,7 @@ public class Solver extends Z3Object
      **/
     public int getNumAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
-                getContext().nCtx(), getNativeObject()));
         return assrts.size();
     }
 
@@ -188,9 +187,8 @@ public class Solver extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
-                getContext().nCtx(), getNativeObject()));
+        return (BoolExpr[]) assrts.ToExprArray();
-	return assrts.ToBoolArray();
     }
 
     /**
@@ -278,16 +276,11 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getUnsatCore()
+    public BoolExpr[] getUnsatCore()
     {
 
-        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
+        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
-                getContext().nCtx(), getNativeObject()));
+        return (BoolExpr[])core.ToExprArray();
-        int n = core.size();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
-        return res;
     }
 
     /**

src/api/ml/z3.mli

@@ -123,7 +123,7 @@ sig
 end
 
 (** The abstract syntax tree (AST) module *)
-module AST :
+module rec AST :
 sig
   type ast 
 
@@ -156,6 +156,12 @@ sig
 		@return A new ASTVector *)
     val translate : ast_vector -> context -> ast_vector
 
+    (** Translates the ASTVector into an (Ast.ast list) *)
+    val to_list : ast_vector -> ast list
+
+    (** Translates the ASTVector into an (Expr.expr list) *)
+    val to_expr_list : ast_vector -> Expr.expr list
+
     (** Retrieves a string representation of the vector. *)
     val to_string : ast_vector -> string
   end
@@ -189,7 +195,7 @@ sig
     val get_size : ast_map -> int
 
     (** The keys stored in the map. *)
-    val get_keys : ast_map -> ast list
+    val get_keys : ast_map -> Expr.expr list
 
     (** Retrieves a string representation of the map.*)
     val to_string : ast_map -> string
@@ -260,7 +266,7 @@ sig
 end
 
 (** The Sort module implements type information for ASTs *)
-module Sort :
+and Sort :
 sig
   type sort = Sort of AST.ast
 
@@ -291,7 +297,7 @@ sig
 end
 
 (** Function declarations *)
-module rec FuncDecl :
+and FuncDecl :
 sig
   type func_decl = FuncDecl of AST.ast
 
@@ -2751,7 +2757,7 @@ sig
   (** The finite set of distinct values that represent the interpretation of a sort. 
       {!get_sorts}
       @return A list of expressions, where each is an element of the universe of the sort *)
-  val sort_universe : model -> Sort.sort -> AST.ast list
+  val sort_universe : model -> Sort.sort -> Expr.expr list
     
   (** Conversion of models to strings. 
       @return A string representation of the model. *)
@@ -2938,6 +2944,55 @@ sig
   val interrupt : context -> unit
 end
 
+(** Objects that track statistical information. *)
+module Statistics :
+sig
+  type statistics 
+	
+  (** Statistical data is organized into pairs of \[Key, Entry\], where every
+	  Entry is either a floating point or integer value. *)
+  module Entry :
+  sig
+    type statistics_entry
+	  
+    (** The key of the entry. *)
+    val get_key : statistics_entry -> string
+	  
+    (** The int-value of the entry. *)
+    val get_int : statistics_entry -> int
+	  
+    (** The float-value of the entry. *)
+    val get_float : statistics_entry -> float
+	  
+    (** True if the entry is uint-valued. *)
+    val is_int : statistics_entry -> bool
+	  
+    (** True if the entry is float-valued. *)
+    val is_float : statistics_entry -> bool
+	  
+    (** The string representation of the the entry's value. *)
+    val to_string_value : statistics_entry -> string
+	  
+    (** The string representation of the entry (key and value) *)
+    val to_string : statistics_entry -> string
+  end
+
+  (** A string representation of the statistical data. *)    
+  val to_string : statistics -> string
+
+  (** The number of statistical data. *)
+  val get_size : statistics -> int
+
+  (** The data entries. *)
+  val get_entries : statistics -> Entry.statistics_entry list
+
+  (**   The statistical counters. *)
+  val get_keys : statistics -> string list
+
+  (** The value of a particular statistical counter. *)        
+  val get : statistics -> string -> Entry.statistics_entry option
+end
+
 (** Solvers *)
 module Solver :
 sig
@@ -2946,56 +3001,6 @@ sig
       
   val string_of_status : status -> string
 
-  (** Objects that track statistical information about solvers. *)
-  module Statistics :
-  sig
-    type statistics 
-
-    (**   Statistical data is organized into pairs of \[Key, Entry\], where every
-		  Entry is either a floating point or integer value.
-    *)
-    module Entry :
-    sig
-      type statistics_entry
-
-      (** The key of the entry. *)
-      val get_key : statistics_entry -> string
-
-      (** The int-value of the entry. *)
-      val get_int : statistics_entry -> int
-
-      (** The float-value of the entry. *)
-      val get_float : statistics_entry -> float
-		
-      (** True if the entry is uint-valued. *)
-      val is_int : statistics_entry -> bool
-		
-      (** True if the entry is float-valued. *)
-      val is_float : statistics_entry -> bool
-		
-      (** The string representation of the the entry's value. *)
-      val to_string_value : statistics_entry -> string
-		
-      (** The string representation of the entry (key and value) *)
-      val to_string : statistics_entry -> string
-    end
-
-    (** A string representation of the statistical data. *)    
-    val to_string : statistics -> string
-
-    (** The number of statistical data. *)
-    val get_size : statistics -> int
-
-    (** The data entries. *)
-    val get_entries : statistics -> Entry.statistics_entry list
-
-    (**   The statistical counters. *)
-    val get_keys : statistics -> string list
-
-    (** The value of a particular statistical counter. *)        
-    val get : statistics -> string -> Entry.statistics_entry option
-  end
-
   (** A string that describes all available solver parameters. *)
   val get_help : solver -> string
 
@@ -3081,7 +3086,7 @@ sig
       The unsat core is a subset of [Assertions]
       The result is empty if [Check] was not invoked before,
       if its results was not [UNSATISFIABLE], or if core production is disabled. *)
-  val get_unsat_core : solver -> AST.ast list
+  val get_unsat_core : solver -> Expr.expr list
 
   (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *)
   val get_reason_unknown : solver -> string
@@ -3198,6 +3203,19 @@ sig
 
   (** Create a Fixedpoint context. *)
   val mk_fixedpoint : context -> fixedpoint
+
+  (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *)
+  val get_statistics : fixedpoint -> Statistics.statistics
+
+  (** Parse an SMT-LIB2 string with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the string. *)
+  val parse_string : fixedpoint -> string -> Expr.expr list
+
+  (** Parse an SMT-LIB2 file with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the file. *)
+  val parse_file : fixedpoint -> string -> Expr.expr list
 end
 
 (** Functions for handling SMT and SMT2 expressions and files *)
@@ -3272,12 +3290,12 @@ sig
   (** Gets an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector
+  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list
 
   (** Computes an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model)
+  val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option)
 
   (** Retrieves an interpolation profile.
       For more information on interpolation please refer

src/api/z3_api.h

@@ -6022,7 +6022,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Parse an SMT-LIB2 string with fixedpoint rules. 
        Add the rules to the current fixedpoint context. 
-       Return the set of queries in the file.
+       Return the set of queries in the string.
 
        \param c - context.
        \param f - fixedpoint context.