ML/Java: Proper use of Datatype API for List/Enum/Constructor

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

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<FuncDecl>() != null);
-                init();
+                IntPtr constructor = IntPtr.Zero;
-                return m_constructorDecl;
+                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<FuncDecl>() != null);
-                init();
+                IntPtr constructor = IntPtr.Zero;
-                return m_testerDecl;
+                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<FuncDecl[]>() != null);
-                init(); 
+                IntPtr constructor = IntPtr.Zero;
-                return m_accessorDecls;
+                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 uint n = 0;
-        private FuncDecl m_testerDecl = null;
+        
-        private FuncDecl m_constructorDecl = null;
-        private FuncDecl[] m_accessorDecls = null;
-
         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
     }
 }

src/api/dotnet/EnumSort.cs

@@ -36,8 +36,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
+                uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
-                return _constdecls;
+                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<Expr[]>() != null);
-
+                FuncDecl[] cds = ConstDecls;
-                return _consts;
+                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<FuncDecl[]>() != null);
-
+                uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
-                return _testerdecls;
+                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
     };

src/api/dotnet/ListSort.cs

@@ -36,7 +36,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != 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<Expr>() != null);
-                return nilConst;
+                return Context.MkApp(NilDecl);
             }
         }
 
@@ -60,7 +60,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != null);
-                return tailDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
             }
         }
 
-        #region Object Invariant
+        #region Internal        
-
-        [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;
-
         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,
+            IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero, 
-                   iisnil = IntPtr.Zero,
+                   icons = IntPtr.Zero, iiscons = IntPtr.Zero,
-                   icons = IntPtr.Zero,
+                   ihead = IntPtr.Zero, itail = 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);
+                                                  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);
         }
         #endregion
     };

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();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_constructorDecl;
+	    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();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_testerDecl;
+        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();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_accessorDecls;
+        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]);
-	}
-
 }

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()
+	public Expr[] getConsts() throws Z3Exception
-	{
+	{	    
-		return _consts;
+	    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));
+				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);
 	}
 };

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