Z3 |

DatatypeSort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public class DatatypeSort<R> extends Sort
24{
30 public int getNumConstructors()
31 {
32 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33 getNativeObject());
34 }
35
42 @SuppressWarnings("unchecked")
43 public FuncDecl<DatatypeSort<R>>[] getConstructors()
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")
60 public FuncDecl<BoolSort>[] getRecognizers()
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
76 public FuncDecl<?>[][] getAccessors()
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};
com.microsoft.z3.BoolSort
Definition: BoolSort.java:24
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.DatatypeSort
Definition: DatatypeSort.java:24
com.microsoft.z3.DatatypeSort.getNumConstructors
int getNumConstructors()
Definition: DatatypeSort.java:30
com.microsoft.z3.DatatypeSort.getRecognizers
FuncDecl< BoolSort >[] getRecognizers()
Definition: DatatypeSort.java:60
com.microsoft.z3.DatatypeSort.getConstructors
FuncDecl< DatatypeSort< R > >[] getConstructors()
Definition: DatatypeSort.java:43
com.microsoft.z3.DatatypeSort.getAccessors
FuncDecl<?>[][] getAccessors()
Definition: DatatypeSort.java:76
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:87
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73