Z3
DatatypeSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class DatatypeSort<R> extends Sort
24{
30 public int getNumConstructors()
31 {
32 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33 getNativeObject());
34 }
35
42 @SuppressWarnings("unchecked")
44 {
45 int n = getNumConstructors();
46 FuncDecl<DatatypeSort<R>>[] res = new FuncDecl[n];
47 for (int i = 0; i < n; i++)
48 res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
49 getContext().nCtx(), getNativeObject(), i));
50 return res;
51 }
52
59 @SuppressWarnings("unchecked")
61 {
62 int n = getNumConstructors();
63 FuncDecl<BoolSort>[] res = new FuncDecl[n];
64 for (int i = 0; i < n; i++)
65 res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(
66 getContext().nCtx(), getNativeObject(), i));
67 return res;
68 }
69
77 {
78
79 int n = getNumConstructors();
80 FuncDecl<?>[][] res = new FuncDecl[n][];
81 for (int i = 0; i < n; i++)
82 {
83 FuncDecl<?> fd = new FuncDecl<>(getContext(),
84 Native.getDatatypeSortConstructor(getContext().nCtx(),
85 getNativeObject(), i));
86 int ds = fd.getDomainSize();
87 FuncDecl<?>[] tmp = new FuncDecl[ds];
88 for (int j = 0; j < ds; j++)
89 tmp[j] = new FuncDecl<>(getContext(),
90 Native.getDatatypeSortConstructorAccessor(getContext()
91 .nCtx(), getNativeObject(), i, j));
92 res[i] = tmp;
93 }
94 return res;
95 }
96
97 DatatypeSort(Context ctx, long obj)
98 {
99 super(ctx, obj);
100 }
101
102 DatatypeSort(Context ctx, Symbol name, Constructor<R>[] constructors)
103
104 {
105 super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
106 constructors.length, arrayToNative(constructors)));
107
108 }
109};
FuncDecl< BoolSort >[] getRecognizers()
FuncDecl< DatatypeSort< R > >[] getConstructors()
FuncDecl<?>[][] getAccessors()
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73