18package com.microsoft.z3;
32 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
42 @SuppressWarnings(
"unchecked")
47 for (
int i = 0; i < n; i++)
48 res[i] =
new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
49 getContext().nCtx(), getNativeObject(), i));
59 @SuppressWarnings(
"unchecked")
64 for (
int i = 0; i < n; i++)
65 res[i] =
new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(
66 getContext().nCtx(), getNativeObject(), i));
81 for (
int i = 0; i < n; i++)
84 Native.getDatatypeSortConstructor(getContext().nCtx(),
85 getNativeObject(), i));
88 for (
int j = 0; j < ds; j++)
90 Native.getDatatypeSortConstructorAccessor(getContext()
91 .nCtx(), getNativeObject(), i, j));
102 DatatypeSort(Context ctx, Symbol name, Constructor<R>[] constructors)
105 super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
FuncDecl< BoolSort >[] getRecognizers()
FuncDecl< DatatypeSort< R > >[] getConstructors()
FuncDecl<?>[][] getAccessors()
static long[] arrayToNative(Z3Object[] a)