Added accessors to enumeration sorts. Thanks to codeplex user steimann for suggesting this.

(http://z3.codeplex.com/workitem/195)

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

RELEASE_NOTES

@@ -11,7 +11,7 @@ Version 4.4
 
 - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one.
 
-- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886.
+- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, steimann, and Stackoverflow users user297886.
 
 
 Version 4.3.2

src/api/dotnet/EnumSort.cs

@@ -44,6 +44,16 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the inx'th constant declaration in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public FuncDecl ConstDecl(uint inx)
+        {
+            return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
+        }
+
         /// <summary>
         /// The constants in the enumeration.
         /// </summary>
@@ -61,7 +71,17 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// The test predicates for the constants in the enumeration.
+        /// Retrieves the inx'th constant in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public Expr Const(uint inx)
+        {
+            return Context.MkApp(ConstDecl(inx));
+        }
+
+        /// <summary>
+        /// The test predicates (recognizers) for the constants in the enumeration.
         /// </summary>
         public FuncDecl[] TesterDecls
         {
@@ -76,6 +96,16 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the inx'th tester/recognizer declaration in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public FuncDecl TesterDecl(uint inx)
+        {
+            return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
+        }
+
         #region Internal
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
             : base(ctx, IntPtr.Zero)

src/api/java/EnumSort.java

@@ -34,11 +34,20 @@ public class EnumSort extends Sort
             t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
         return t;
     }
+    
+    /**
+     * Retrieves the inx'th constant declaration in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl getConstDecl(int inx) throws Z3Exception
+    {
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
+    }
 
     /**
      * The constants in the enumeration.
      * @throws Z3Exception on error
-     * @return an Expr
+     * @return an Expr[]
      **/
     public Expr[] getConsts() throws Z3Exception
     {        
@@ -48,6 +57,16 @@ public class EnumSort extends Sort
             t[i] = getContext().mkApp(cds[i]);
         return t;
     }
+    
+    /**
+     * Retrieves the inx'th constant in the enumeration.
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr getConst(int inx) throws Z3Exception
+    {        
+    	return getContext().mkApp(getConstDecl(inx));
+    }
 
     /**
      * The test predicates for the constants in the enumeration.
@@ -61,6 +80,15 @@ public class EnumSort extends Sort
             t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
         return t;
     }
+    
+    /**
+     * Retrieves the inx'th tester/recognizer declaration in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl getTesterDecl(int inx) throws Z3Exception
+    {
+        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
+    }
 
     EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
     {

src/api/ml/z3.ml

@@ -1390,11 +1390,24 @@ struct
     let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x)  i)) in
     mk_list f n
 
+  let get_const_decl ( x : sort ) ( inx : int ) =
+    func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) inx)
+
+  let get_consts ( x : sort ) =
+    let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
+    let f i = (Expr.mk_const_f (Sort.gc x) (get_const_decl x i)) in
+    mk_list f n
+
+  let get_const ( x : sort ) ( inx : int ) =
+    Expr.mk_const_f (Sort.gc x) (get_const_decl x inx)
+
   let get_tester_decls ( x : sort ) = 
     let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
-    let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x)  i)) in
+    let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in
     mk_list f n
       
+  let get_tester_decl ( x : sort ) ( inx : int ) = 
+    func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) inx)
 end
 
 

src/api/ml/z3.mli

@@ -1091,8 +1091,20 @@ sig
   (** The function declarations of the constants in the enumeration. *)
   val get_const_decls : Sort.sort -> FuncDecl.func_decl list
 
+  (** Retrieves the inx'th constant declaration in the enumeration. *)
+  val get_const_decl : Sort.sort -> int -> FuncDecl.func_decl
+
+  (** The constants in the enumeration. *)
+  val get_consts : Sort.sort -> Expr.expr list
+
+  (** Retrieves the inx'th constant in the enumeration. *)
+  val get_const : Sort.sort -> int -> Expr.expr
+
   (** The test predicates for the constants in the enumeration. *)
   val get_tester_decls : Sort.sort -> FuncDecl.func_decl list
+
+  (** Retrieves the inx'th tester/recognizer declaration in the enumeration. *)
+  val get_tester_decl : Sort.sort -> int -> FuncDecl.func_decl
 end
 
 (** Functions to manipulate List expressions *)