18package com.microsoft.z3;
23@SuppressWarnings(
"unchecked")
32 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
34 for (
int i = 0; i < n; i++)
35 t[i] =
new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
45 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
57 for (
int i = 0; i < t.length; i++)
58 t[i] = getContext().mkApp(cds[i]);
69 return getContext().mkApp(getConstDecl(inx));
76 @SuppressWarnings(
"unchecked")
79 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
81 for (
int i = 0; i < n; i++)
82 t[i] =
new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
92 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
97 super(ctx, Native.mkEnumerationSort(ctx.
nCtx(),
98 name.getNativeObject(), enumNames.length,
100 new long[enumNames.length],
new long[enumNames.length]));
Expr< EnumSort< R > > getConst(int inx)
FuncDecl< EnumSort< R > > getConstDecl(int inx)
FuncDecl< BoolSort > getTesterDecl(int inx)
Expr< EnumSort< R > >[] getConsts()
FuncDecl< EnumSort< R > >[] getConstDecls()
static long[] arrayToNative(Z3Object[] a)
def EnumSort(name, values, ctx=None)