Z3
EnumSort.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23@SuppressWarnings("unchecked")
24public class EnumSort<R> extends Sort
25{
31 {
32 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
33 FuncDecl<?>[] t = new FuncDecl[n];
34 for (int i = 0; i < n; i++)
35 t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
36 return (FuncDecl<EnumSort<R>>[]) t;
37 }
38
44 {
45 return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
46 }
47
54 {
55 FuncDecl<?>[] cds = getConstDecls();
56 Expr<?>[] t = new Expr[cds.length];
57 for (int i = 0; i < t.length; i++)
58 t[i] = getContext().mkApp(cds[i]);
59 return (Expr<EnumSort<R>>[]) t;
60 }
61
67 public Expr<EnumSort<R>> getConst(int inx)
68 {
69 return getContext().mkApp(getConstDecl(inx));
70 }
71
76 @SuppressWarnings("unchecked")
77 public FuncDecl<BoolSort>[] getTesterDecls()
78 {
79 int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
80 FuncDecl<BoolSort>[] t = new FuncDecl[n];
81 for (int i = 0; i < n; i++)
82 t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
83 return t;
84 }
85
91 {
92 return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
93 }
94
95 EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
96 {
97 super(ctx, Native.mkEnumerationSort(ctx.nCtx(),
98 name.getNativeObject(), enumNames.length,
99 Symbol.arrayToNative(enumNames),
100 new long[enumNames.length], new long[enumNames.length]));
101 }
102};
Expr< EnumSort< R > > getConst(int inx)
Definition: EnumSort.java:67
FuncDecl< EnumSort< R > > getConstDecl(int inx)
Definition: EnumSort.java:43
FuncDecl< BoolSort > getTesterDecl(int inx)
Definition: EnumSort.java:90
Expr< EnumSort< R > >[] getConsts()
Definition: EnumSort.java:53
FuncDecl< EnumSort< R > >[] getConstDecls()
Definition: EnumSort.java:30
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
def EnumSort(name, values, ctx=None)
Definition: z3py.py:5317