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