From 1c77ad00c30cb308864bbb2a099932a4110ed96b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Mar 2015 21:42:05 +0000 Subject: [PATCH] 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 --- RELEASE_NOTES | 2 +- src/api/dotnet/EnumSort.cs | 32 +++++++++++++++++++++++++++++++- src/api/java/EnumSort.java | 30 +++++++++++++++++++++++++++++- src/api/ml/z3.ml | 15 ++++++++++++++- src/api/ml/z3.mli | 12 ++++++++++++ 5 files changed, 87 insertions(+), 4 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 01f9e687e..afa613f57 100644 --- a/RELEASE_NOTES +++ b/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 diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index f7ba98222..62be48a2c 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -44,6 +44,16 @@ namespace Microsoft.Z3 } } + /// + /// Retrieves the inx'th constant declaration in the enumeration. + /// + /// + /// + public FuncDecl ConstDecl(uint inx) + { + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx)); + } + /// /// The constants in the enumeration. /// @@ -61,7 +71,17 @@ namespace Microsoft.Z3 } /// - /// The test predicates for the constants in the enumeration. + /// Retrieves the inx'th constant in the enumeration. + /// + /// + /// + public Expr Const(uint inx) + { + return Context.MkApp(ConstDecl(inx)); + } + + /// + /// The test predicates (recognizers) for the constants in the enumeration. /// public FuncDecl[] TesterDecls { @@ -76,6 +96,16 @@ namespace Microsoft.Z3 } } + /// + /// Retrieves the inx'th tester/recognizer declaration in the enumeration. + /// + /// + /// + 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) diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index e33b9b348..bfe0c50b8 100644 --- a/src/api/java/EnumSort.java +++ b/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 { diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d8cf21cda..a7cafbc29 100644 --- a/src/api/ml/z3.ml +++ b/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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e223008bb..db0c3f130 100644 --- a/src/api/ml/z3.mli +++ b/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 *)