Z3
src/api/java/DatatypeSort.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00023 public class DatatypeSort extends Sort
00024 {
00028         public int getNumConstructors() throws Z3Exception
00029         {
00030                 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
00031                                 getNativeObject());
00032         }
00033 
00039         public FuncDecl[] getConstructors() throws Z3Exception
00040         {
00041                 int n = getNumConstructors();
00042                 FuncDecl[] res = new FuncDecl[n];
00043                 for (int i = 0; i < n; i++)
00044                         res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
00045                                         getContext().nCtx(), getNativeObject(), i));
00046                 return res;
00047         }
00048 
00054         public FuncDecl[] getRecognizers() throws Z3Exception
00055         {
00056                 int n = getNumConstructors();
00057                 FuncDecl[] res = new FuncDecl[n];
00058                 for (int i = 0; i < n; i++)
00059                         res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
00060                                         getContext().nCtx(), getNativeObject(), i));
00061                 return res;
00062         }
00063 
00069         public FuncDecl[][] getAccessors() throws Z3Exception
00070         {
00071 
00072                 int n = getNumConstructors();
00073                 FuncDecl[][] res = new FuncDecl[n][];
00074                 for (int i = 0; i < n; i++)
00075                 {
00076                         FuncDecl fd = new FuncDecl(getContext(),
00077                                         Native.getDatatypeSortConstructor(getContext().nCtx(),
00078                                                         getNativeObject(), i));
00079                         int ds = fd.getDomainSize();
00080                         FuncDecl[] tmp = new FuncDecl[ds];
00081                         for (int j = 0; j < ds; j++)
00082                                 tmp[j] = new FuncDecl(getContext(),
00083                                                 Native.getDatatypeSortConstructorAccessor(getContext()
00084                                                                 .nCtx(), getNativeObject(), i, j));
00085                         res[i] = tmp;
00086                 }
00087                 return res;
00088         }
00089 
00090         DatatypeSort(Context ctx, long obj) throws Z3Exception
00091         {
00092                 super(ctx, obj);
00093         }
00094 
00095         DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
00096                         throws Z3Exception
00097         {
00098                 super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
00099                                 (int) constructors.length, arrayToNative(constructors)));
00100 
00101         }
00102 };
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines