Z3
DatatypeSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public class DatatypeSort extends Sort
24{
30 public int getNumConstructors()
31 {
32 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33 getNativeObject());
34 }
35
43 {
44 int n = getNumConstructors();
45 FuncDecl[] res = new FuncDecl[n];
46 for (int i = 0; i < n; i++)
47 res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
48 getContext().nCtx(), getNativeObject(), i));
49 return res;
50 }
51
59 {
60 int n = getNumConstructors();
61 FuncDecl[] res = new FuncDecl[n];
62 for (int i = 0; i < n; i++)
63 res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
64 getContext().nCtx(), getNativeObject(), i));
65 return res;
66 }
67
75 {
76
77 int n = getNumConstructors();
78 FuncDecl[][] res = new FuncDecl[n][];
79 for (int i = 0; i < n; i++)
80 {
81 FuncDecl fd = new FuncDecl(getContext(),
82 Native.getDatatypeSortConstructor(getContext().nCtx(),
83 getNativeObject(), i));
84 int ds = fd.getDomainSize();
85 FuncDecl[] tmp = new FuncDecl[ds];
86 for (int j = 0; j < ds; j++)
87 tmp[j] = new FuncDecl(getContext(),
89 .nCtx(), getNativeObject(), i, j));
90 res[i] = tmp;
91 }
92 return res;
93 }
94
95 DatatypeSort(Context ctx, long obj)
96 {
97 super(ctx, obj);
98 }
99
100 DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
101
102 {
103 super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
104 constructors.length, arrayToNative(constructors)));
105
106 }
107};
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
Definition: Native.java:2792
static int getDatatypeSortNumConstructors(long a0, long a1)
Definition: Native.java:2765
static long getDatatypeSortConstructor(long a0, long a1, int a2)
Definition: Native.java:2774
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
Definition: Native.java:2783