From 6075ae28fcdf8ce1b1bf13ad1925711aa2adb445 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 20 Feb 2013 19:40:48 +0000 Subject: [PATCH] ML/Java: Proper use of Datatype API for List/Enum/Constructor Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Constructor.cs | 65 ++++++++++++----------------------- src/api/dotnet/EnumSort.cs | 46 ++++++++----------------- src/api/dotnet/ListSort.cs | 54 +++++++---------------------- src/api/java/Constructor.java | 47 ++++++++++--------------- src/api/java/EnumSort.java | 40 ++++++++++----------- src/api/java/ListSort.java | 46 +++++++++++-------------- 6 files changed, 109 insertions(+), 189 deletions(-) diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs index 043eb3a1e..527b8bc13 100644 --- a/src/api/dotnet/Constructor.cs +++ b/src/api/dotnet/Constructor.cs @@ -34,8 +34,7 @@ namespace Microsoft.Z3 public uint NumFields { get - { - init(); + { return n; } } @@ -48,8 +47,11 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - init(); - return m_constructorDecl; + IntPtr constructor = IntPtr.Zero; + IntPtr tester = IntPtr.Zero; + IntPtr[] accessors = new IntPtr[n]; + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + return new FuncDecl(Context, constructor); } } @@ -61,8 +63,11 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - init(); - return m_testerDecl; + IntPtr constructor = IntPtr.Zero; + IntPtr tester = IntPtr.Zero; + IntPtr[] accessors = new IntPtr[n]; + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + return new FuncDecl(Context, tester); } } @@ -74,8 +79,14 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - init(); - return m_accessorDecls; + IntPtr constructor = IntPtr.Zero; + IntPtr tester = IntPtr.Zero; + IntPtr[] accessors = new IntPtr[n]; + Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); + FuncDecl[] t = new FuncDecl[n]; + for (uint i = 0; i < n; i++) + t[i] = new FuncDecl(Context, accessors[i]); + return t; } } @@ -85,25 +96,11 @@ namespace Microsoft.Z3 ~Constructor() { Native.Z3_del_constructor(Context.nCtx, NativeObject); - } - - #region Object invariant - - [ContractInvariantMethod] - private void ObjectInvariant() - { - Contract.Invariant(m_testerDecl == null || m_constructorDecl != null); - Contract.Invariant(m_testerDecl == null || m_accessorDecls != null); - } - - #endregion + } #region Internal - readonly private uint n = 0; - private FuncDecl m_testerDecl = null; - private FuncDecl m_constructorDecl = null; - private FuncDecl[] m_accessorDecls = null; - + private uint n = 0; + internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, uint[] sortRefs) : base(ctx) @@ -129,24 +126,6 @@ namespace Microsoft.Z3 } - private void init() - { - Contract.Ensures(m_constructorDecl != null); - Contract.Ensures(m_testerDecl != null); - Contract.Ensures(m_accessorDecls != null); - - if (m_testerDecl != null) return; - IntPtr constructor = IntPtr.Zero; - IntPtr tester = IntPtr.Zero; - IntPtr[] accessors = new IntPtr[n]; - Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors); - m_constructorDecl = new FuncDecl(Context, constructor); - m_testerDecl = new FuncDecl(Context, tester); - m_accessorDecls = new FuncDecl[n]; - for (uint i = 0; i < n; i++) - m_accessorDecls[i] = new FuncDecl(Context, accessors[i]); - } - #endregion } } diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index 1a9b0536c..e62043078 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -36,8 +36,11 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - - return _constdecls; + uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); + FuncDecl[] t = new FuncDecl[n]; + for (uint i = 0; i < n; i++) + t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i)); + return t; } } @@ -49,8 +52,11 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - - return _consts; + FuncDecl[] cds = ConstDecls; + Expr[] t = new Expr[cds.Length]; + for (uint i = 0; i < t.Length; i++) + t[i] = Context.MkApp(cds[i]); + return t; } } @@ -62,28 +68,15 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - - return _testerdecls; + uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); + FuncDecl[] t = new FuncDecl[n]; + for (uint i = 0; i < n; i++) + t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i)); + return t; } } - #region Object Invariant - - [ContractInvariantMethod] - private void ObjectInvariant() - { - Contract.Invariant(this._constdecls != null); - Contract.Invariant(this._testerdecls != null); - Contract.Invariant(this._consts != null); - } - - - #endregion - #region Internal - readonly private FuncDecl[] _constdecls = null, _testerdecls = null; - readonly private Expr[] _consts = null; - internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames) : base(ctx) { @@ -96,15 +89,6 @@ namespace Microsoft.Z3 IntPtr[] n_testers = new IntPtr[n]; NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n, Symbol.ArrayToNative(enumNames), n_constdecls, n_testers); - _constdecls = new FuncDecl[n]; - for (uint i = 0; i < n; i++) - _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); - _testerdecls = new FuncDecl[n]; - for (uint i = 0; i < n; i++) - _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); - _consts = new Expr[n]; - for (uint i = 0; i < n; i++) - _consts[i] = ctx.MkApp(_constdecls[i]); } #endregion }; diff --git a/src/api/dotnet/ListSort.cs b/src/api/dotnet/ListSort.cs index c099259a2..7dbafb385 100644 --- a/src/api/dotnet/ListSort.cs +++ b/src/api/dotnet/ListSort.cs @@ -36,7 +36,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return nilDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0)); } } @@ -48,7 +48,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return nilConst; + return Context.MkApp(NilDecl); } } @@ -60,7 +60,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return isNilDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0)); } } @@ -72,7 +72,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return consDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1)); } } @@ -85,7 +85,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return isConsDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1)); } } @@ -97,7 +97,7 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return headDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0)); } } @@ -109,31 +109,11 @@ namespace Microsoft.Z3 get { Contract.Ensures(Contract.Result() != null); - return tailDecl; + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1)); } } - #region Object Invariant - - [ContractInvariantMethod] - private void ObjectInvariant() - { - Contract.Invariant(nilConst != null); - Contract.Invariant(nilDecl != null); - Contract.Invariant(isNilDecl != null); - Contract.Invariant(consDecl != null); - Contract.Invariant(isConsDecl != null); - Contract.Invariant(headDecl != null); - Contract.Invariant(tailDecl != null); - } - - - #endregion - - #region Internal - readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl; - readonly private Expr nilConst; - + #region Internal internal ListSort(Context ctx, Symbol name, Sort elemSort) : base(ctx) { @@ -141,22 +121,12 @@ namespace Microsoft.Z3 Contract.Requires(name != null); Contract.Requires(elemSort != null); - IntPtr inil = IntPtr.Zero, - iisnil = IntPtr.Zero, - icons = IntPtr.Zero, - iiscons = IntPtr.Zero, - ihead = IntPtr.Zero, - itail = IntPtr.Zero; + IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero, + icons = IntPtr.Zero, iiscons = IntPtr.Zero, + ihead = IntPtr.Zero, itail = IntPtr.Zero; NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject, - ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail); - nilDecl = new FuncDecl(ctx, inil); - isNilDecl = new FuncDecl(ctx, iisnil); - consDecl = new FuncDecl(ctx, icons); - isConsDecl = new FuncDecl(ctx, iiscons); - headDecl = new FuncDecl(ctx, ihead); - tailDecl = new FuncDecl(ctx, itail); - nilConst = ctx.MkConst(nilDecl); + ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail); } #endregion }; diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index c12521bc5..0c53da73c 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -16,8 +16,7 @@ public class Constructor extends Z3Object * @throws Z3Exception **/ public int getNumFields() throws Z3Exception - { - init(); + { return n; } @@ -27,8 +26,11 @@ public class Constructor extends Z3Object **/ public FuncDecl ConstructorDecl() throws Z3Exception { - init(); - return m_constructorDecl; + Native.LongPtr constructor = new Native.LongPtr(); + Native.LongPtr tester = new Native.LongPtr(); + long[] accessors = new long[n]; + Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); + return new FuncDecl(getContext(), constructor.value); } /** @@ -37,8 +39,11 @@ public class Constructor extends Z3Object **/ public FuncDecl getTesterDecl() throws Z3Exception { - init(); - return m_testerDecl; + Native.LongPtr constructor = new Native.LongPtr(); + Native.LongPtr tester = new Native.LongPtr(); + long[] accessors = new long[n]; + Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); + return new FuncDecl(getContext(), tester.value); } /** @@ -47,8 +52,14 @@ public class Constructor extends Z3Object **/ public FuncDecl[] getAccessorDecls() throws Z3Exception { - init(); - return m_accessorDecls; + Native.LongPtr constructor = new Native.LongPtr(); + Native.LongPtr tester = new Native.LongPtr(); + long[] accessors = new long[n]; + Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors); + FuncDecl[] t = new FuncDecl[n]; + for (int i = 0; i < n; i++) + t[i] = new FuncDecl(getContext(), accessors[i]); + return t; } /** @@ -60,9 +71,6 @@ public class Constructor extends Z3Object } private int n = 0; - private FuncDecl m_testerDecl = null; - private FuncDecl m_constructorDecl = null; - private FuncDecl[] m_accessorDecls = null; Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) @@ -87,21 +95,4 @@ public class Constructor extends Z3Object Sort.arrayToNative(sorts), sortRefs)); } - - private void init() throws Z3Exception - { - if (m_testerDecl != null) - return; - Native.LongPtr constructor = new Native.LongPtr(); - Native.LongPtr tester = new Native.LongPtr(); - long[] accessors = new long[n]; - Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, - constructor, tester, accessors); - m_constructorDecl = new FuncDecl(getContext(), constructor.value); - m_testerDecl = new FuncDecl(getContext(), tester.value); - m_accessorDecls = new FuncDecl[n]; - for (int i = 0; i < n; i++) - m_accessorDecls[i] = new FuncDecl(getContext(), accessors[i]); - } - } diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index f3cbda954..c0fb6d1d6 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -14,30 +14,39 @@ public class EnumSort extends Sort /** * The function declarations of the constants in the enumeration. **/ - public FuncDecl[] getConstDecls() + public FuncDecl[] getConstDecls() throws Z3Exception { - return _constdecls; + int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); + FuncDecl[] t = new FuncDecl[n]; + for (int i = 0; i < n; i++) + t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); + return t; } /** * The constants in the enumeration. **/ - public Expr[] getConsts() - { - return _consts; + public Expr[] getConsts() throws Z3Exception + { + FuncDecl[] cds = getConstDecls(); + Expr[] t = new Expr[cds.length]; + for (int i = 0; i < t.length; i++) + t[i] = getContext().mkApp(cds[i]); + return t; } /** * The test predicates for the constants in the enumeration. **/ - public FuncDecl[] getTesterDecls() + public FuncDecl[] getTesterDecls() throws Z3Exception { - return _testerdecls; + int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); + FuncDecl[] t = new FuncDecl[n]; + for (int i = 0; i < n; i++) + t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i)); + return t; } - private FuncDecl[] _constdecls = null, _testerdecls = null; - private Expr[] _consts = null; - EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception { super(ctx); @@ -47,15 +56,6 @@ public class EnumSort extends Sort long[] n_testers = new long[n]; setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames), - n_constdecls, n_testers)); - _constdecls = new FuncDecl[n]; - for (int i = 0; i < n; i++) - _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); - _testerdecls = new FuncDecl[n]; - for (int i = 0; i < n; i++) - _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); - _consts = new Expr[n]; - for (int i = 0; i < n; i++) - _consts[i] = ctx.mkApp(_constdecls[i], (Expr[])null); + n_constdecls, n_testers)); } }; diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index df1c51a95..af1645187 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -13,65 +13,68 @@ public class ListSort extends Sort { /** * The declaration of the nil function of this list sort. + * @throws Z3Exception **/ - public FuncDecl getNilDecl() + public FuncDecl getNilDecl() throws Z3Exception { - return nilDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0)); } /** * The empty list. + * @throws Z3Exception **/ - public Expr getNil() + public Expr getNil() throws Z3Exception { - return nilConst; + return getContext().mkApp(getNilDecl()); } /** * The declaration of the isNil function of this list sort. + * @throws Z3Exception **/ - public FuncDecl getIsNilDecl() + public FuncDecl getIsNilDecl() throws Z3Exception { - return isNilDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0)); } /** * The declaration of the cons function of this list sort. + * @throws Z3Exception **/ - public FuncDecl getConsDecl() + public FuncDecl getConsDecl() throws Z3Exception { - return consDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1)); } /** * The declaration of the isCons function of this list sort. + * @throws Z3Exception * **/ - public FuncDecl getIsConsDecl() + public FuncDecl getIsConsDecl() throws Z3Exception { - return isConsDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1)); } /** * The declaration of the head function of this list sort. + * @throws Z3Exception **/ - public FuncDecl getHeadDecl() + public FuncDecl getHeadDecl() throws Z3Exception { - return headDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0)); } /** * The declaration of the tail function of this list sort. + * @throws Z3Exception **/ - public FuncDecl getTailDecl() + public FuncDecl getTailDecl() throws Z3Exception { - return tailDecl; + return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1)); } - private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, - tailDecl; - private Expr nilConst; - ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception { super(ctx); @@ -83,12 +86,5 @@ public class ListSort extends Sort setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(), elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead, itail)); - nilDecl = new FuncDecl(ctx, inil.value); - isNilDecl = new FuncDecl(ctx, iisnil.value); - consDecl = new FuncDecl(ctx, icons.value); - isConsDecl = new FuncDecl(ctx, iiscons.value); - headDecl = new FuncDecl(ctx, ihead.value); - tailDecl = new FuncDecl(ctx, itail.value); - nilConst = ctx.mkConst(nilDecl); } };